---

Step * 1 1 of Lemma void-function-equipollent


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

---

Latex:

---

Latex:

1.  F  :  Top@i
2.  b  :  Top@i
\mvdash{}  \mexists{}a:i:\mBbbN{}0  {}\mrightarrow{}  F[i].  (((\mlambda{}x.x)  a)  =  b)


By

---

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

---

Home Index