---

Step * of Lemma bag-combine-single-right

∀[A:Type]. ∀[bs:bag(A)].  (⋃x∈bs.{x} ~ bs)
BY
{ (InstLemma `bag-combine-unit-right` [] THEN Fold `single-bag` (-1) THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[bs:bag(A)].    (\mcup{}x\mmember{}bs.\{x\}  \msim{}  bs)


By

---

Latex:
(InstLemma  `bag-combine-unit-right`  []  THEN  Fold  `single-bag`  (-1)  THEN  Trivial)

---

Home Index