### Nuprl Lemma : cons_sublist_cons

`∀[T:Type]. ∀x1,x2:T. ∀L1,L2:T List.  ([x1 / L1] ⊆ [x2 / L2] `⇐⇒` ((x1 = x2 ∈ T) ∧ L1 ⊆ L2) ∨ [x1 / L1] ⊆ L2)`

Proof

Definitions occuring in Statement :  sublist: `L1 ⊆ L2` cons: `[a / b]` list: `T List` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` or: `P ∨ Q` and: `P ∧ Q` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` implies: `P `` Q` sublist: `L1 ⊆ L2` member: `t ∈ T` exists: `∃x:A. B[x]` prop: `ℙ` rev_implies: `P `` Q` or: `P ∨ Q` int_seg: `{i..j-}` lelt: `i ≤ j < k` le: `A ≤ B` less_than': `less_than'(a;b)` false: `False` not: `¬A` nat_plus: `ℕ+` decidable: `Dec(P)` uimplies: `b supposing a` satisfiable_int_formula: `satisfiable_int_formula(fmla)` guard: `{T}` uiff: `uiff(P;Q)` subtype_rel: `A ⊆r B` cand: `A c∧ B` nat: `ℕ` ge: `i ≥ j ` less_than: `a < b` squash: `↓T` sq_type: `SQType(T)` true: `True` increasing: `increasing(f;k)` nequal: `a ≠ b ∈ T ` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` ifthenelse: `if b then t else f fi ` bfalse: `ff` bnot: `¬bb` assert: `↑b` subtract: `n - m` select: `L[n]` cons: `[a / b]`
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt lambdaFormation_alt independent_pairFormation sqequalHypSubstitution sqequalRule cut introduction extract_by_obid dependent_functionElimination thin Error :memTop,  hypothesis productElimination universeIsType isectElimination hypothesisEquality unionIsType productIsType equalityIstype inhabitedIsType instantiate universeEquality dependent_set_memberEquality_alt natural_numberEquality unionElimination independent_isectElimination approximateComputation independent_functionElimination dependent_pairFormation_alt lambdaEquality_alt voidElimination equalityTransitivity equalitySymmetry applyLambdaEquality setElimination rename pointwiseFunctionality promote_hyp baseApply closedConclusion baseClosed int_eqEquality because_Cache addEquality applyEquality inlFormation_alt functionIsType functionExtensionality imageElimination cumulativity intEquality imageMemberEquality productEquality hyp_replacement inrFormation_alt equalityElimination minusEquality multiplyEquality

Latex:
\mforall{}[T:Type]
\mforall{}x1,x2:T.  \mforall{}L1,L2:T  List.    ([x1  /  L1]  \msubseteq{}  [x2  /  L2]  \mLeftarrow{}{}\mRightarrow{}  ((x1  =  x2)  \mwedge{}  L1  \msubseteq{}  L2)  \mvee{}  [x1  /  L1]  \msubseteq{}  L2)

Date html generated: 2020_05_19-PM-09_42_01
Last ObjectModification: 2019_12_31-PM-00_15_48

Theory : list_1

Home Index