---

Step * of Lemma finite-unit

finite(Unit)
BY
{ (D 0 With ⌜1⌝  THEN Auto) }

1
Unit ~ ℕ1

---

Latex:

---

Latex:
finite(Unit)


By

---

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

---

Home Index