Nuprl Lemma : sublist_antisymmetry

[T:Type]. ∀[L1,L2:T List].  (L1 L2 ∈ (T List)) supposing (L2 ⊆ L1 and L1 ⊆ L2)


Definitions occuring in Statement :  sublist: L1 ⊆ L2 list: List uimplies: supposing a uall: [x:A]. B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a prop: all: x:A. B[x] decidable: Dec(P) or: P ∨ Q le: A ≤ B and: P ∧ Q not: ¬A implies:  Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False top: Top
Lemmas referenced :  proper_sublist_length sublist_wf list_wf length_sublist decidable__equal_int full-omega-unsat intformand_wf intformnot_wf intformeq_wf itermVar_wf intformle_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_eq_lemma int_term_value_var_lemma int_formula_prop_le_lemma int_formula_prop_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality independent_isectElimination hypothesis sqequalRule isect_memberEquality axiomEquality because_Cache equalityTransitivity equalitySymmetry universeEquality dependent_functionElimination unionElimination productElimination natural_numberEquality approximateComputation independent_functionElimination dependent_pairFormation lambdaEquality int_eqEquality intEquality voidElimination voidEquality independent_pairFormation

\mforall{}[T:Type].  \mforall{}[L1,L2:T  List].    (L1  =  L2)  supposing  (L2  \msubseteq{}  L1  and  L1  \msubseteq{}  L2)

Date html generated: 2018_05_21-PM-00_33_14
Last ObjectModification: 2018_05_19-AM-06_42_52

Theory : list_1

Home Index