---

Step * of Lemma mFOL-sequent-abstract_wf

∀[s:mFOL-sequent()]. (mFOL-sequent-abstract(s) ∈ AbstractFOFormula(mFOL-sequent-freevars(s)))
BY
{ ((Intro THEN Unhide) THEN D 1 THEN RepUR ``mFOL-sequent-abstract AbstractFOFormula`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[s:mFOL-sequent()].  (mFOL-sequent-abstract(s)  \mmember{}  AbstractFOFormula(mFOL-sequent-freevars(s)))


By

---

Latex:
((Intro  THEN  Unhide)  THEN  D  1  THEN  RepUR  ``mFOL-sequent-abstract  AbstractFOFormula``  0  THEN  Auto)

---

Home Index