---

Step * of Lemma mFOL-freevars-connect-contained

∀x,y:mFOL(). ∀knd:Atom. ∀vs:ℤ List.
  ((mFOL-freevars(x) ⊆ vs ∧ mFOL-freevars(y) ⊆ vs) ⇒ mFOL-freevars(mFOconnect(knd;x;y)) ⊆ vs)
BY
{ (Auto THEN RepUR ``mFOL-freevars`` 0 THEN Fold `mFOL-freevars` 0 THEN RWO "val-union-l-union" 0 THEN Auto) }

1
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

---

Latex:

---

Latex:
\mforall{}x,y:mFOL().  \mforall{}knd:Atom.  \mforall{}vs:\mBbbZ{}  List.
    ((mFOL-freevars(x)  \msubseteq{}  vs  \mwedge{}  mFOL-freevars(y)  \msubseteq{}  vs)  {}\mRightarrow{}  mFOL-freevars(mFOconnect(knd;x;y))  \msubseteq{}  vs)


By

---

Latex:
(Auto
  THEN  RepUR  ``mFOL-freevars``  0
  THEN  Fold  `mFOL-freevars`  0
  THEN  RWO  "val-union-l-union"  0
  THEN  Auto)

---

Home Index