Nuprl Lemma : before_last

[T:Type]. ∀L:T List. ∀x:T.  ((x ∈ L)  before last(L) ∈ supposing ¬(x last(L) ∈ T))


Proof




Definitions occuring in Statement :  l_before: before y ∈ l last: last(L) l_member: (x ∈ l) list: List uimplies: supposing a uall: [x:A]. B[x] all: x:A. B[x] not: ¬A implies:  Q universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] member: t ∈ T so_lambda: λ2x.t[x] implies:  Q prop: uimplies: supposing a not: ¬A false: False so_apply: x[s] iff: ⇐⇒ Q and: P ∧ Q top: Top or: P ∨ Q l_before: before y ∈ l rev_implies:  Q uiff: uiff(P;Q) last: last(L) select: L[n] cons: [a b] subtract: m length: ||as|| list_ind: list_ind nil: [] it: assert: b ifthenelse: if then else fi  btrue: tt bfalse: ff true: True squash: T subtype_rel: A ⊆B guard: {T}
Lemmas referenced :  list_induction all_wf l_member_wf not_wf equal_wf last_wf assert_elim null_wf member-implies-null-eq-bfalse btrue_neq_bfalse assert_wf l_before_wf list_wf nil_member nil_wf cons_wf null_cons_lemma istype-void bfalse_wf cons_member cons_sublist_cons assert_of_null list-cases null_nil_lemma btrue_wf product_subtype_list false_wf squash_wf true_wf last_cons iff_weakening_equal sublist_wf subtype_rel_self member_iff_sublist last_member
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  Error :lambdaFormation_alt,  cut thin introduction extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality sqequalRule Error :lambdaEquality_alt,  cumulativity functionEquality because_Cache hypothesis isectEquality independent_isectElimination equalityTransitivity equalitySymmetry independent_functionElimination voidElimination Error :universeIsType,  rename Error :functionIsType,  Error :inhabitedIsType,  Error :isectIsType,  dependent_functionElimination universeEquality productElimination Error :equalityIsType1,  Error :isect_memberEquality_alt,  Error :unionIsType,  unionElimination hyp_replacement applyLambdaEquality promote_hyp hypothesis_subsumption natural_numberEquality applyEquality imageElimination imageMemberEquality baseClosed Error :inlFormation_alt,  instantiate independent_pairFormation Error :inrFormation_alt,  Error :productIsType

Latex:
\mforall{}[T:Type].  \mforall{}L:T  List.  \mforall{}x:T.    ((x  \mmember{}  L)  {}\mRightarrow{}  x  before  last(L)  \mmember{}  L  supposing  \mneg{}(x  =  last(L)))



Date html generated: 2019_06_20-PM-01_23_37
Last ObjectModification: 2018_09_29-PM-00_04_11

Theory : list_1


Home Index