Nuprl Lemma : length-one-member

[T:Type]. ∀[L:T List].  ∀[x,y:T].  (x y ∈ T) supposing ((y ∈ L) and (x ∈ L)) supposing ||L|| 1 ∈ ℤ


Definitions occuring in Statement :  l_member: (x ∈ l) length: ||as|| list: List uimplies: supposing a uall: [x:A]. B[x] natural_number: $n int: universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T all: x:A. B[x] or: P ∨ Q uimplies: supposing a sq_type: SQType(T) implies:  Q guard: {T} true: True false: False prop: cons: [a b] top: Top ge: i ≥  le: A ≤ B and: P ∧ Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] not: ¬A iff: ⇐⇒ Q
Lemmas referenced :  member_singleton list_wf length_wf cons_wf l_member_wf int_formula_prop_wf int_term_value_add_lemma int_formula_prop_eq_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_and_lemma itermAdd_wf intformeq_wf itermVar_wf itermConstant_wf intformle_wf intformand_wf satisfiable-full-omega-tt non_neg_length length_of_cons_lemma product_subtype_list equal_wf int_subtype_base subtype_base_sq length_of_nil_lemma list-cases
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut hypothesisEquality lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesis dependent_functionElimination unionElimination sqequalRule instantiate cumulativity intEquality independent_isectElimination equalityTransitivity equalitySymmetry independent_functionElimination natural_numberEquality voidElimination promote_hyp isect_memberEquality axiomEquality because_Cache hypothesis_subsumption productElimination voidEquality rename dependent_pairFormation lambdaEquality int_eqEquality independent_pairFormation computeAll addEquality universeEquality

\mforall{}[T:Type].  \mforall{}[L:T  List].    \mforall{}[x,y:T].    (x  =  y)  supposing  ((y  \mmember{}  L)  and  (x  \mmember{}  L))  supposing  ||L||  =  1

Date html generated: 2016_05_14-PM-01_27_50
Last ObjectModification: 2016_01_15-AM-08_28_54

Theory : list_1

Home Index