Nuprl Lemma : last-not-before

[T:Type]. ∀L:T List. (∀x:T. (last(L) before x ∈ ⇐⇒ False)) supposing (no_repeats(T;L) and (¬↑null(L)))


Definitions occuring in Statement :  l_before: before y ∈ l last: last(L) no_repeats: no_repeats(T;l) null: null(as) list: List assert: b uimplies: supposing a uall: [x:A]. B[x] all: x:A. B[x] iff: ⇐⇒ Q not: ¬A false: False universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] uimplies: supposing a member: t ∈ T not: ¬A implies:  Q false: False iff: ⇐⇒ Q and: P ∧ Q uiff: uiff(P;Q) prop: rev_implies:  Q
Lemmas referenced :  no_repeats_witness no_repeats_iff last_wf before_last l_before_wf istype-void no_repeats_wf istype-assert null_wf list_wf istype-universe l_before_member l_before_transitivity
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt lambdaFormation_alt cut introduction sqequalRule sqequalHypSubstitution lambdaEquality_alt dependent_functionElimination thin hypothesisEquality voidElimination functionIsTypeImplies inhabitedIsType rename extract_by_obid isectElimination independent_functionElimination hypothesis independent_pairFormation because_Cache productElimination independent_isectElimination equalitySymmetry equalityIstype universeIsType functionIsType instantiate universeEquality

    \mforall{}L:T  List.  (\mforall{}x:T.  (last(L)  before  x  \mmember{}  L  \mLeftarrow{}{}\mRightarrow{}  False))  supposing  (no\_repeats(T;L)  and  (\mneg{}\muparrow{}null(L)))

Date html generated: 2019_10_15-AM-10_23_47
Last ObjectModification: 2019_08_05-PM-02_11_52

Theory : list_1

Home Index