---

Step * 2 1 of Lemma FormSafe1'-iff-FormSafe1''

.....assertion..... 
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. phi : Atom List
8. l_subset(Atom;phi;vs-FormFvs(left))
9. FormSafe1'(left) vs-phi
10. FormSafe1'(right) phi
⊢ set-equal(Atom;vs-FormFvs(left);phi)
BY
{ ((RWO "FormSafe-iff-FormSafe1'<" (-1)⋅ THENA Auto)
   THEN (RWO "FormSafe-iff-FormSafe1'<" (-2)⋅ THENA Auto)
   THEN (FLemma `FormSafe1-Fvs-subset` [-2] THENA Auto)) }

1
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. phi : Atom List
8. l_subset(Atom;phi;vs-FormFvs(left))
9. FormSafe1(left) vs-phi
10. FormSafe1(right) phi
11. l_subset(Atom;vs-phi;FormFvs(left))
⊢ set-equal(Atom;vs-FormFvs(left);phi)

---

Latex:

---

Latex:
.....assertion..... 
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.  phi  :  Atom  List
8.  l\_subset(Atom;phi;vs-FormFvs(left))
9.  FormSafe1'(left)  vs-phi
10.  FormSafe1'(right)  phi
\mvdash{}  set-equal(Atom;vs-FormFvs(left);phi)


By

---

Latex:
((RWO  "FormSafe-iff-FormSafe1'<"  (-1)\mcdot{}  THENA  Auto)
  THEN  (RWO  "FormSafe-iff-FormSafe1'<"  (-2)\mcdot{}  THENA  Auto)
  THEN  (FLemma  `FormSafe1-Fvs-subset`  [-2]  THENA  Auto))

---

Home Index