---

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

∀hyps:mFOL() List. ∀concl:mFOL().  mFOL-freevars(concl) ⊆ mFOL-sequent-freevars(<hyps, concl>)
BY
{ (Auto THEN BLemma `mFOL-sequent-freevars-contains-concl` THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}hyps:mFOL()  List.  \mforall{}concl:mFOL().    mFOL-freevars(concl)  \msubseteq{}  mFOL-sequent-freevars(<hyps,  concl>)


By

---

Latex:
(Auto  THEN  BLemma  `mFOL-sequent-freevars-contains-concl`  THEN  Reduce  0  THEN  Auto)

---

Home Index