---

Step * of Lemma null-bag-empty

∀T:Type. ∀x:bag(T).  (↑bag-null(x) ⇐⇒ x = {} ∈ bag(T))
BY
{ (((UnivCD THENA Auto) THEN Unfold `bag-null` 0 THEN RWO "null-bag" 0) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}x:bag(T).    (\muparrow{}bag-null(x)  \mLeftarrow{}{}\mRightarrow{}  x  =  \{\})


By

---

Latex:
(((UnivCD  THENA  Auto)  THEN  Unfold  `bag-null`  0  THEN  RWO  "null-bag"  0)  THEN  Auto)

---

Home Index