---

Step * of Lemma single-valued-bag-empty

∀[T:Type]. single-valued-bag({};T)
BY
{ (Auto THEN BLemma `single-valued-bag-if-le1` THEN Auto THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  single-valued-bag(\{\};T)


By

---

Latex:
(Auto  THEN  BLemma  `single-valued-bag-if-le1`  THEN  Auto  THEN  Reduce  0  THEN  Auto)

---

Home Index