---

Step * of Lemma singleton-type-one

singleton-type(ℕ1)
BY
{ (With ⌜0⌝ (D 0)⋅ THEN Auto) }

---

Latex:

---

Latex:
singleton-type(\mBbbN{}1)


By

---

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

---

Home Index