---

Step * 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 / v])
⊢ mFOL-freevars(h) ⊆ mFOL-freevars(u) ⋃ reduce(λh,vs. mFOL-freevars(h) ⋃ vs;mFOL-freevars(concl);v)
BY
{ ((RWO "cons_member" (-1) THENM D -1) THENA 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 ∈ mFOL()
⊢ mFOL-freevars(h) ⊆ mFOL-freevars(u) ⋃ reduce(λh,vs. mFOL-freevars(h) ⋃ vs;mFOL-freevars(concl);v)

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)

---

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{}  [u  /  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:
((RWO  "cons\_member"  (-1)  THENM  D  -1)  THENA  Auto)

---

Home Index