Nuprl Lemma : bag_null_cons_lemma

v,u:Top.  (bag-null(u.v) ff)


Proof




Definitions occuring in Statement :  bag-null: bag-null(bs) cons-bag: x.b bfalse: ff top: Top all: x:A. B[x] sqequal: t
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T cons-bag: x.b bag-null: bag-null(bs) top: Top
Lemmas referenced :  top_wf null_cons_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut hypothesis lemma_by_obid sqequalRule sqequalHypSubstitution dependent_functionElimination thin isect_memberEquality voidElimination voidEquality

Latex:
\mforall{}v,u:Top.    (bag-null(u.v)  \msim{}  ff)



Date html generated: 2016_05_15-PM-02_23_58
Last ObjectModification: 2015_12_27-AM-09_53_35

Theory : bags


Home Index