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