---

Step * of Lemma empty-bag-iff-size

∀[T:Type]. ∀[bs:bag(T)].  uiff(bs = {} ∈ bag(T);#(bs) ≤ 0)
BY
{ RepeatFor 2 ((D 0 THENA Auto)) }

1
1. T : Type
2. bs : bag(T)
⊢ uiff(bs = {} ∈ bag(T);#(bs) ≤ 0)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[bs:bag(T)].    uiff(bs  =  \{\};\#(bs)  \mleq{}  0)


By

---

Latex:
RepeatFor  2  ((D  0  THENA  Auto))

---

Home Index