---

Step * of Lemma nat-to-incomparable_wf

∀[n:ℕ]. (nat-to-incomparable(n) ∈ Name)
BY
{ Unfold `name` 0
THEN ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  (nat-to-incomparable(n)  \mmember{}  Name)


By

---

Latex:
Unfold  `name`  0
THEN  ProveWfLemma

---

Home Index