---

Step * of Lemma mFOL_size_wf

∀[p:mFOL()]. (mFOL_size(p) ∈ ℕ)
BY
{ ProveCoSizeWf2 `mFOLco_size` }

---

Latex:


\mforall{}[p:mFOL()].  (mFOL\_size(p)  \mmember{}  \mBbbN{})


By

ProveCoSizeWf2  `mFOLco\_size`

---

Home Index