Nuprl Lemma : last_append_singleton_sq

dumplicate needes to be removed and references replaced by last_append_singleton

[T:Type]. ∀L:T List. ∀a:T.  (last(L [a]) a)


Proof




Definitions occuring in Statement :  last: last(L) append: as bs cons: [a b] nil: [] list: List uall: [x:A]. B[x] all: x:A. B[x] universe: Type sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T all: x:A. B[x] top: Top subtype_rel: A ⊆B uimplies: supposing a
Lemmas referenced :  last_singleton_append subtype_rel_list top_wf list_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation lemma_by_obid sqequalHypSubstitution isectElimination thin isect_memberEquality voidElimination voidEquality dependent_functionElimination hypothesisEquality applyEquality hypothesis independent_isectElimination lambdaEquality because_Cache sqequalRule sqequalAxiom universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}L:T  List.  \mforall{}a:T.    (last(L  @  [a])  \msim{}  a)



Date html generated: 2016_07_08-PM-04_49_15
Last ObjectModification: 2015_12_26-PM-05_06_06

Theory : list_1


Home Index