---

Step * of Lemma bag-append-empty

∀[as:Top List]. (as + {} ~ as)
BY
{ ((UnivCD THENA Auto) THEN Unfolds ``bag-append empty-bag`` 0 THEN RWO "append-nil" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[as:Top  List].  (as  +  \{\}  \msim{}  as)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Unfolds  ``bag-append  empty-bag``  0  THEN  RWO  "append-nil"  0  THEN  Auto)

---

Home Index