---

Step * 1 of Lemma single-bag-not-null


1. T : Type@i'
2. x : T@i
⊢ ↑bag-null({x}) ~ False
BY
{ (( RWO "null-bag-size" 0  THENA Auto) THEN RepUR ``bag-size single-bag`` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type@i'
2.  x  :  T@i
\mvdash{}  \muparrow{}bag-null(\{x\})  \msim{}  False


By

---

Latex:
((  RWO  "null-bag-size"  0    THENA  Auto)  THEN  RepUR  ``bag-size  single-bag``  0  THEN  Auto)

---

Home Index