---

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


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 ∈ mFOL()
⊢ mFOL-freevars(h) ⊆ mFOL-freevars(u) ⋃ reduce(λh,vs. mFOL-freevars(h) ⋃ vs;mFOL-freevars(concl);v)
BY
{ (HypSubst' (-1) 0 THEN Auto) }

---

Latex:

---

Latex:

1.  u  :  mFOL()
2.  v  :  mFOL()  List
3.  \mforall{}concl,h:mFOL().
          ((h  \mmember{}  v)  {}\mRightarrow{}  mFOL-freevars(h)  \msubseteq{}  reduce(\mlambda{}h,vs.  mFOL-freevars(h)  \mcup{}  vs;mFOL-freevars(concl);v))
4.  concl  :  mFOL()
5.  h  :  mFOL()
6.  h  =  u
\mvdash{}  mFOL-freevars(h)  \msubseteq{}  mFOL-freevars(u)  \mcup{}  reduce(\mlambda{}h,vs.  mFOL-freevars(h)  \mcup{}  vs;mFOL-freevars(concl);v)


By

---

Latex:
(HypSubst'  (-1)  0  THEN  Auto)

---

Home Index