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