---

Step * of Lemma FOL-sequent-abstract_wf

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

---

Latex:

---

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


By

---

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

---

Home Index