---

Step * of Lemma bag-size-is-zero

∀[C:Type]. ∀[bs:bag(C)].  bs ~ {} supposing #(bs) = 0 ∈ ℤ
BY
{ (Auto THEN BLemma `bag-size-zero` THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[C:Type].  \mforall{}[bs:bag(C)].    bs  \msim{}  \{\}  supposing  \#(bs)  =  0


By

---

Latex:
(Auto  THEN  BLemma  `bag-size-zero`  THEN  Auto')

---

Home Index