---

Step * of Lemma mFOquant_wf

∀[isall:𝔹]. ∀[var:ℤ]. ∀[body:mFOL()].  (mFOquant(isall;var;body) ∈ mFOL())
BY
{ DepprodCoDatatypeConstructorWf `mFOL_size` }

---

Latex:


\mforall{}[isall:\mBbbB{}].  \mforall{}[var:\mBbbZ{}].  \mforall{}[body:mFOL()].    (mFOquant(isall;var;body)  \mmember{}  mFOL())


By

DepprodCoDatatypeConstructorWf  `mFOL\_size`

---

Home Index