---

Step * of Lemma single-valued-bag-single

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

---

Latex:

---

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


By

---

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

---

Home Index