---

Step * 1 of Lemma void-function-equipollent


1. F : Top@i
⊢ i:ℕ0 ⟶ F[i] ~ Top
BY
{ ((With ⌜λx.x⌝ (D 0)⋅ THEN Auto) THEN RepeatFor 2 ((D 0 THEN Auto))) }

1
1. F : Top@i
2. b : Top@i
⊢ ∃a:i:ℕ0 ⟶ F[i]. (((λx.x) a) = b ∈ Top)

---

Latex:

---

Latex:

1.  F  :  Top@i
\mvdash{}  i:\mBbbN{}0  {}\mrightarrow{}  F[i]  \msim{}  Top


By

---

Latex:
((With  \mkleeneopen{}\mlambda{}x.x\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)  THEN  RepeatFor  2  ((D  0  THEN  Auto)))

---

Home Index