---

Step * of Lemma bag_all-empty

∀[f:Top]. (bag_all({};f) ~ tt)
BY
{ (RepUR ``bag_all bag-accum empty-bag`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[f:Top].  (bag\_all(\{\};f)  \msim{}  tt)


By

---

Latex:
(RepUR  ``bag\_all  bag-accum  empty-bag``  0  THEN  Auto)

---

Home Index