Step
*
of Lemma
mFOL-freevars_wf
∀[fmla:mFOL()]. (mFOL-freevars(fmla) ∈ ℤ List)
BY
{ ProveWfLemma }
Latex:
\mforall{}[fmla:mFOL()].  (mFOL-freevars(fmla)  \mmember{}  \mBbbZ{}  List)
By
ProveWfLemma
Home
Index