---

Step * 1 1 1 of Lemma equipollent-product


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

---

Latex:

---

Latex:

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


By

---

Latex:
(BLemma  `singleton-type-void-domain`  THEN  Auto)\mcdot{}

---

Home Index