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