---

Step * of Lemma null-bag-size

∀[T:Type]. ∀[x:bag(T)].  (bag-null(x) ~ (#(x) =z 0))
BY
{ Auto }

1
1. T : Type
2. x : bag(T)
⊢ bag-null(x) = (#(x) =z 0)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[x:bag(T)].    (bag-null(x)  \msim{}  (\#(x)  =\msubz{}  0))


By

---

Latex:
Auto

---

Home Index