---

Step * 1 of Lemma partial-void


1. z : partial(Void)@i
⊢ ¬(z)↓
BY
{ (D 0 THEN Auto THEN Unfold `false` 0) }

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

---

Latex:

---

Latex:

1.  z  :  partial(Void)@i
\mvdash{}  \mneg{}(z)\mdownarrow{}


By

---

Latex:
(D  0  THEN  Auto  THEN  Unfold  `false`  0)

---

Home Index