---

Step * of Lemma mFOL-sequent-freevars-contains-concl

∀s:mFOL-sequent(). ∀L:ℤ List.  (L ⊆ mFOL-freevars(snd(s)) ⇒ L ⊆ mFOL-sequent-freevars(s))
BY
{ ((UnivCD THENA Auto)
   THEN D 1
   THEN RepUR ``mFOL-sequent-freevars`` 0
   THEN Reduce (-1)
   THEN MoveToConcl (-1)
   THEN (GenConclTerm ⌜mFOL-freevars(s2)⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN MoveToConcl (-1)
   THEN Thin (-2)
   THEN ListInd 1
   THEN Reduce 0
   THEN Auto
   THEN BLemma `l-union-right-contains`
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  D  1
  THEN  RepUR  ``mFOL-sequent-freevars``  0
  THEN  Reduce  (-1)
  THEN  MoveToConcl  (-1)
  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  Auto
  THEN  BLemma  `l-union-right-contains`
  THEN  Auto)

---

Home Index