---

Step * of Lemma bag-union-single

∀x:Top List. (bag-union({x}) ~ x)
BY
{ (RepUR ``bag-union single-bag concat`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}x:Top  List.  (bag-union(\{x\})  \msim{}  x)


By

---

Latex:
(RepUR  ``bag-union  single-bag  concat``  0  THEN  Auto)

---

Home Index