---

Step * of Lemma partial-void

∀z:partial(Void). (z ~ ⊥)
BY
{ (Auto THEN BLemma `no-value-bottom` THEN Auto) }

1
1. z : partial(Void)@i
⊢ ¬(z)↓

---

Latex:

---

Latex:
\mforall{}z:partial(Void).  (z  \msim{}  \mbot{})


By

---

Latex:
(Auto  THEN  BLemma  `no-value-bottom`  THEN  Auto)

---

Home Index