---

Step * of Lemma single-bag-not-null

∀T:Type. ∀x:T.  (↑bag-null({x}) ~ False)
BY
{ RepeatFor 2 ((D 0 THENA Auto)) }

1
1. T : Type@i'
2. x : T@i
⊢ ↑bag-null({x}) ~ False

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}x:T.    (\muparrow{}bag-null(\{x\})  \msim{}  False)


By

---

Latex:
RepeatFor  2  ((D  0  THENA  Auto))

---

Home Index