Nuprl Lemma : sublist_nil

[T:Type]. ∀L:T List. (L ⊆ [] ⇐⇒ [] ∈ (T List))


Proof




Definitions occuring in Statement :  sublist: L1 ⊆ L2 nil: [] list: List uall: [x:A]. B[x] all: x:A. B[x] iff: ⇐⇒ Q universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q implies:  Q member: t ∈ T prop: rev_implies:  Q uiff: uiff(P;Q) uimplies: supposing a ge: i ≥  decidable: Dec(P) or: P ∨ Q le: A ≤ B satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False not: ¬A top: Top
Lemmas referenced :  sublist_wf nil_wf equal-wf-T-base list_wf length_zero length_sublist length_of_nil_lemma non_neg_length decidable__equal_int length_wf satisfiable-full-omega-tt intformand_wf intformnot_wf intformeq_wf itermVar_wf itermConstant_wf intformle_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_eq_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_wf nil-sublist
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation independent_pairFormation cut hypothesis introduction extract_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesisEquality baseClosed universeEquality productElimination independent_isectElimination because_Cache sqequalRule dependent_functionElimination unionElimination natural_numberEquality dependent_pairFormation lambdaEquality int_eqEquality intEquality isect_memberEquality voidElimination voidEquality computeAll hyp_replacement equalitySymmetry Error :applyLambdaEquality

Latex:
\mforall{}[T:Type].  \mforall{}L:T  List.  (L  \msubseteq{}  []  \mLeftarrow{}{}\mRightarrow{}  L  =  [])



Date html generated: 2016_10_21-AM-10_02_01
Last ObjectModification: 2016_07_12-AM-05_23_43

Theory : list_1


Home Index