---

Step * of Lemma prank_wf

∀[x:formula()]. (prank(x) ∈ ℕ)
BY
{ (ProveWfLemma THEN (RWO "imax_unfold" 0 THENA Auto) THEN AutoSplit) }

---

Latex:

---

Latex:
\mforall{}[x:formula()].  (prank(x)  \mmember{}  \mBbbN{})


By

---

Latex:
(ProveWfLemma  THEN  (RWO  "imax\_unfold"  0  THENA  Auto)  THEN  AutoSplit)

---

Home Index