---

Step * of Lemma mFOL-sequent-freevars-subset-4

∀hyps:mFOL() List. ∀x,y:mFOL().  (mFOL-freevars(x) ⊆ mFOL-sequent-freevars(<hyps, y>) ⇒ mFOL-sequent-freevars(<hyps, x>\000C) ⊆ mFOL-sequent-freevars(<hyps, y>))
BY
{ (Auto THEN BLemma `mFOL-sequent-freevars-contained` THEN Auto THEN All Reduce THEN EAuto 1) }

---

Latex:

---

Latex:
\mforall{}hyps:mFOL()  List.  \mforall{}x,y:mFOL().    (mFOL-freevars(x)  \msubseteq{}  mFOL-sequent-freevars(<hyps,  y>)  {}\mRightarrow{}  mFOL-sequen\000Ct-freevars(<hyps,  x>)  \msubseteq{}  mFOL-sequent-freevars(<hyps,  y>))


By

---

Latex:
(Auto  THEN  BLemma  `mFOL-sequent-freevars-contained`  THEN  Auto  THEN  All  Reduce  THEN  EAuto  1)

---

Home Index