Nuprl Lemma : bag-val-empty

[+,zero:Top].  (bag-val(zero;+) {} zero)


Proof




Definitions occuring in Statement :  bag-val: bag-val(zero;+) empty-bag: {} uall: [x:A]. B[x] top: Top apply: a sqequal: t
Definitions unfolded in proof :  empty-bag: {} bag-val: bag-val(zero;+) all: x:A. B[x] member: t ∈ T top: Top so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] uall: [x:A]. B[x]
Lemmas referenced :  list_accum_nil_lemma top_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity sqequalRule cut lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin isect_memberEquality voidElimination voidEquality hypothesis isect_memberFormation introduction sqequalAxiom isectElimination hypothesisEquality because_Cache

Latex:
\mforall{}[+,zero:Top].    (bag-val(zero;+)  \{\}  \msim{}  zero)



Date html generated: 2016_05_15-PM-02_26_34
Last ObjectModification: 2015_12_27-AM-09_52_02

Theory : bags


Home Index