---

Step * 1 2 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 ∈ v)
⊢ mFOL-freevars(h) ⊆ mFOL-freevars(u) ⋃ reduce(λh,vs. mFOL-freevars(h) ⋃ vs;mFOL-freevars(concl);v)
BY
{ (InstHyp [⌜concl⌝;⌜h⌝] 3⋅ 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 ∈ v)
7. mFOL-freevars(h) ⊆ reduce(λh,vs. mFOL-freevars(h) ⋃ vs;mFOL-freevars(concl);v)
⊢ mFOL-freevars(h) ⊆ mFOL-freevars(u) ⋃ reduce(λh,vs. mFOL-freevars(h) ⋃ vs;mFOL-freevars(concl);v)

---

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  \mmember{}  v)
\mvdash{}  mFOL-freevars(h)  \msubseteq{}  mFOL-freevars(u)  \mcup{}  reduce(\mlambda{}h,vs.  mFOL-freevars(h)  \mcup{}  vs;mFOL-freevars(concl);v)


By

---

Latex:
(InstHyp  [\mkleeneopen{}concl\mkleeneclose{};\mkleeneopen{}h\mkleeneclose{}]  3\mcdot{}  THEN  Auto)

---

Home Index