Step
*
of Lemma
mFOL-abstract_wf
∀[fmla:mFOL()]. (mFOL-abstract(fmla) ∈ AbstractFOFormula)
BY
{ ProveWfLemma }
Latex:
\mforall{}[fmla:mFOL()].  (mFOL-abstract(fmla)  \mmember{}  AbstractFOFormula)
By
ProveWfLemma
Home
Index