---

Step * 3 of Lemma FormSafe1'-iff-FormSafe1''


1. C : Type
2. left : Form(C)
3. right : Form(C)
4. ∀vs:Atom List. (FormSafe1'(left) vs ⇐⇒ FormSafe1''(left) vs)
5. ∀vs:Atom List. (FormSafe1'(right) vs ⇐⇒ FormSafe1''(right) vs)
6. vs : Atom List
7. let theta = vs-FormFvs(right) in
       (FormSafe1''(left) theta) ∧ (FormSafe1''(right) vs-theta)
⊢ ∃theta:Atom List. (l_subset(Atom;theta;vs-FormFvs(right)) ∧ (FormSafe1'(left) theta) ∧ (FormSafe1'(right) vs-theta))
BY
{ (RepUR ``let`` -1 THEN D 0 With ⌜vs-FormFvs(right)⌝  THEN Auto) }

---

Latex:

---

Latex:

1.  C  :  Type
2.  left  :  Form(C)
3.  right  :  Form(C)
4.  \mforall{}vs:Atom  List.  (FormSafe1'(left)  vs  \mLeftarrow{}{}\mRightarrow{}  FormSafe1''(left)  vs)
5.  \mforall{}vs:Atom  List.  (FormSafe1'(right)  vs  \mLeftarrow{}{}\mRightarrow{}  FormSafe1''(right)  vs)
6.  vs  :  Atom  List
7.  let  theta  =  vs-FormFvs(right)  in
              (FormSafe1''(left)  theta)  \mwedge{}  (FormSafe1''(right)  vs-theta)
\mvdash{}  \mexists{}theta:Atom  List
      (l\_subset(Atom;theta;vs-FormFvs(right))
      \mwedge{}  (FormSafe1'(left)  theta)
      \mwedge{}  (FormSafe1'(right)  vs-theta))


By

---

Latex:
(RepUR  ``let``  -1  THEN  D  0  With  \mkleeneopen{}vs-FormFvs(right)\mkleeneclose{}    THEN  Auto)

---

Home Index