---

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

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

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  BLemma  `mFOL-sequent-freevars-subset-4`  THEN  Auto)

---

Home Index