---

Step * of Lemma levelsup_wf

No Annotations
∀[x,y:ℕ4].  (levelsup(x;y) ∈ ℕ4)
BY
{ RepeatFor 2 (ProveWfLemma) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[x,y:\mBbbN{}4].    (levelsup(x;y)  \mmember{}  \mBbbN{}4)


By

---

Latex:
RepeatFor  2  (ProveWfLemma)

---

Home Index