---

Step * 1 of Lemma mFOL-freevars-connect-contained


1. x : mFOL()@i
2. y : mFOL()@i
3. knd : Atom@i
4. vs : ℤ List@i
5. mFOL-freevars(x) ⊆ vs@i
6. mFOL-freevars(y) ⊆ vs@i
⊢ mFOL-freevars(x) ⋃ mFOL-freevars(y) ⊆ vs
BY
{ (BLemma `l-union-contained` THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  mFOL()@i
2.  y  :  mFOL()@i
3.  knd  :  Atom@i
4.  vs  :  \mBbbZ{}  List@i
5.  mFOL-freevars(x)  \msubseteq{}  vs@i
6.  mFOL-freevars(y)  \msubseteq{}  vs@i
\mvdash{}  mFOL-freevars(x)  \mcup{}  mFOL-freevars(y)  \msubseteq{}  vs


By

---

Latex:
(BLemma  `l-union-contained`  THEN  Auto)

---

Home Index