Nuprl Lemma : single-bag-append-nil

[a:Top]. ([a] [] [a])


Proof




Definitions occuring in Statement :  bag-append: as bs cons: [a b] nil: [] uall: [x:A]. B[x] top: Top sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T empty-bag: {}
Lemmas referenced :  bag-append-empty cons_wf top_wf nil_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule hypothesis lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality sqequalAxiom

Latex:
\mforall{}[a:Top].  ([a]  +  []  \msim{}  [a])



Date html generated: 2016_05_15-PM-03_09_09
Last ObjectModification: 2015_12_27-AM-09_26_06

Theory : bags


Home Index