Nuprl Lemma : l-last-nil

l-last([]) ~ ⊥


Proof




Definitions occuring in Statement :  l-last: l-last(l) nil: [] bottom: sqequal: t
Definitions unfolded in proof :  l-last: l-last(l) l-last-default: l-last-default(l;d) all: x:A. B[x] so_lambda: so_lambda(x,y,z.t[x; y; z]) member: t ∈ T top: Top so_apply: x[s1;s2;s3]
Lemmas referenced :  list_ind_nil_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity sqequalRule cut lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin isect_memberEquality voidElimination voidEquality hypothesis

Latex:
l-last([])  \msim{}  \mbot{}



Date html generated: 2016_05_14-AM-07_41_52
Last ObjectModification: 2015_12_26-PM-02_51_44

Theory : list_1


Home Index