---

Step * 1 of Lemma equipollent-void-domain


1. [A] : Type
⊢ singleton-type(ℕ0 ⟶ A)
BY
{ (BLemma `singleton-type-void-domain` THEN Auto) }

---

Latex:

---

Latex:

1.  [A]  :  Type
\mvdash{}  singleton-type(\mBbbN{}0  {}\mrightarrow{}  A)


By

---

Latex:
(BLemma  `singleton-type-void-domain`  THEN  Auto)

---

Home Index