---

Step * of Lemma mFOL-freevars-connect-right-contained

∀fmla:mFOL(). mFOL-freevars(mFOconnect-right(fmla)) ⊆ mFOL-freevars(fmla) supposing ↑mFOconnect?(fmla)
BY
{ (BLemma `mFOL-induction` THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}fmla:mFOL()
    mFOL-freevars(mFOconnect-right(fmla))  \msubseteq{}  mFOL-freevars(fmla)  supposing  \muparrow{}mFOconnect?(fmla)


By

---

Latex:
(BLemma  `mFOL-induction`  THEN  Reduce  0  THEN  Auto)

---

Home Index