Nuprl Lemma : bag_size_single_lemma

x:Top. (#({x}) 1)


Proof




Definitions occuring in Statement :  bag-size: #(bs) single-bag: {x} top: Top all: x:A. B[x] natural_number: $n sqequal: t
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T single-bag: {x} bag-size: #(bs) top: Top
Lemmas referenced :  top_wf length_of_cons_lemma length_of_nil_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{}x:Top.  (\#(\{x\})  \msim{}  1)



Date html generated: 2016_05_15-PM-02_24_54
Last ObjectModification: 2015_12_27-AM-09_53_27

Theory : bags


Home Index