Nuprl Lemma : single-bag-not-null
∀T:Type. ∀x:T. (↑bag-null({x}) ~ False)
Proof
Definitions occuring in Statement :
assert: ↑b,
all: ∀x:A. B[x],
false: False,
universe: Type,
sqequal: s ~ t,
bag-null: bag-null(bs),
single-bag: {x}
Lemmas :
null-bag-size,
single-bag_wf,
length_of_cons_lemma,
length_of_nil_lemma
Latex:
\mforall{}T:Type. \mforall{}x:T. (\muparrow{}bag-null(\{x\}) \msim{} False)
Date html generated:
2015_07_23-AM-11_25_24
Last ObjectModification:
2015_01_28-PM-11_16_14
Home
Index