---

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

∀hyps:mFOL() List. ∀concl,h:mFOL().  ((h ∈ hyps) ⇒ mFOL-freevars(h) ⊆ mFOL-sequent-freevars(<hyps, concl>))
BY
{ (RepUR ``mFOL-sequent-freevars`` 0 THEN InductionOnList THEN Reduce 0 ⋅ THEN Auto) }

1
1. u : mFOL()
2. v : mFOL() List
3. ∀concl,h:mFOL().  ((h ∈ v) ⇒ mFOL-freevars(h) ⊆ reduce(λh,vs. mFOL-freevars(h) ⋃ vs;mFOL-freevars(concl);v))
4. concl : mFOL()
5. h : mFOL()
6. (h ∈ [u / v])
⊢ mFOL-freevars(h) ⊆ mFOL-freevars(u) ⋃ reduce(λh,vs. mFOL-freevars(h) ⋃ vs;mFOL-freevars(concl);v)

---

Latex:

---

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


By

---

Latex:
(RepUR  ``mFOL-sequent-freevars``  0  THEN  InductionOnList  THEN  Reduce  0  \mcdot{}  THEN  Auto)

---

Home Index