Nuprl Lemma : list_extensionality

[T:Type]. ∀[a,b:T List].
  (a b ∈ (T List)) supposing ((∀i:ℕ(i < ||a||  (a[i] b[i] ∈ T))) and (||a|| ||b|| ∈ ℤ))


Definitions occuring in Statement :  select: L[n] length: ||as|| list: List nat: less_than: a < b uimplies: supposing a uall: [x:A]. B[x] all: x:A. B[x] implies:  Q int: universe: Type equal: t ∈ T
Definitions unfolded in proof :  so_apply: x[s] all: x:A. B[x] guard: {T} squash: T sq_stable: SqStable(P) uimplies: supposing a nat: prop: implies:  Q so_lambda: λ2x.t[x] uall: [x:A]. B[x] member: t ∈ T select: L[n] nil: [] it: so_lambda: λ2y.t[x; y] top: Top so_apply: x[s1;s2] exists: x:A. B[x] subtype_rel: A ⊆B false: False subtract: m sq_type: SQType(T) ge: i ≥  le: A ≤ B and: P ∧ Q less_than': less_than'(a;b) true: True not: ¬A cons: [a b] less_than: a < b nat_plus: + uiff: uiff(P;Q) rev_implies:  Q iff: ⇐⇒ Q or: P ∨ Q decidable: Dec(P)
Lemmas referenced :  list_wf le_weakening length_wf less_than_transitivity1 sq_stable__le select_wf equal_wf less_than_wf nat_wf all_wf list_induction equal-wf-base-T nil_wf length_of_nil_lemma stuck-spread base_wf equal-wf-base length_of_cons_lemma non_neg_length length_wf_nat set_subtype_base le_wf int_subtype_base cons_wf less_than_irreflexivity equal-wf-T-base add-commutes subtract_wf minus-add add-associates minus-one-mul zero-add add-swap add-mul-special two-mul mul-distributes-right zero-mul add-zero one-mul subtype_base_sq minus-zero nat_properties and_wf true_wf squash_wf nat_plus_wf add_nat_plus false_wf le-add-cancel2 add_functionality_wrt_le minus-one-mul-top condition-implies-le le_antisymmetry_iff not-equal-2 decidable__int_equal less-iff-le not-lt-2 decidable__lt le-add-cancel not-le-2 decidable__le iff_weakening_equal select_cons_tl
Rules used in proof :  axiomEquality isect_memberEquality isect_memberFormation universeEquality intEquality dependent_functionElimination imageElimination baseClosed imageMemberEquality independent_functionElimination natural_numberEquality independent_isectElimination hypothesisEquality cumulativity equalitySymmetry equalityTransitivity because_Cache rename setElimination functionEquality lambdaEquality sqequalRule hypothesis thin isectElimination sqequalHypSubstitution extract_by_obid introduction cut sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution lambdaFormation voidEquality voidElimination dependent_pairFormation sqequalIntensionalEquality applyEquality productElimination promote_hyp addEquality minusEquality multiplyEquality instantiate hyp_replacement dependent_set_memberEquality independent_pairFormation applyLambdaEquality unionElimination

\mforall{}[T:Type].  \mforall{}[a,b:T  List].
    (a  =  b)  supposing  ((\mforall{}i:\mBbbN{}.  (i  <  ||a||  {}\mRightarrow{}  (a[i]  =  b[i])))  and  (||a||  =  ||b||))

Date html generated: 2019_06_20-PM-00_41_09
Last ObjectModification: 2018_08_06-PM-02_09_12

Theory : list_0

Home Index