---

Step * of Lemma mFOL-sequent-freevars-contained

∀s:mFOL-sequent(). ∀L:ℤ List.
  (mFOL-sequent-freevars(s) ⊆ L ⇐⇒ mFOL-freevars(snd(s)) ⊆ L ∧ (∀h:mFOL(). ((h ∈ fst(s)) ⇒ mFOL-freevars(h) ⊆ L)))
BY
{ ((UnivCD THENA Auto)
   THEN D 1
   THEN RepUR ``mFOL-sequent-freevars`` 0
   THEN (GenConclTerm ⌜mFOL-freevars(s2)⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN MoveToConcl (-1)
   THEN Thin (-2)
   THEN ListInd 1
   THEN Reduce 0
   THEN (RWO "nil_member cons_member l-union-contained" 0 THENA Auto)
   THEN RWW "-1" 0
   THEN Auto
   THEN D -1
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}s:mFOL-sequent().  \mforall{}L:\mBbbZ{}  List.
    (mFOL-sequent-freevars(s)  \msubseteq{}  L
    \mLeftarrow{}{}\mRightarrow{}  mFOL-freevars(snd(s))  \msubseteq{}  L  \mwedge{}  (\mforall{}h:mFOL().  ((h  \mmember{}  fst(s))  {}\mRightarrow{}  mFOL-freevars(h)  \msubseteq{}  L)))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  D  1
  THEN  RepUR  ``mFOL-sequent-freevars``  0
  THEN  (GenConclTerm  \mkleeneopen{}mFOL-freevars(s2)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  MoveToConcl  (-1)
  THEN  Thin  (-2)
  THEN  ListInd  1
  THEN  Reduce  0
  THEN  (RWO  "nil\_member  cons\_member  l-union-contained"  0  THENA  Auto)
  THEN  RWW  "-1"  0
  THEN  Auto
  THEN  D  -1
  THEN  Auto)

---

Home Index