---

Step * 1 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. theta : Atom List
8. l_subset(Atom;theta;vs-FormFvs(right))
9. FormSafe1'(left) theta
10. FormSafe1'(right) vs-theta
11. set-equal(Atom;vs-FormFvs(right);theta)
12. FormSafe1''(left) vs-FormFvs(right)
⊢ FormSafe1''(right) vs-vs-FormFvs(right)
BY
{ (((RWO "4< 5<" 0 THENA Auto) THEN MoveToConcl (-3))
   THEN (RWO "FormSafe-iff-FormSafe1'<" 0⋅ THENA Auto)
   THEN (BLemma `FormSafe1_functionality`  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. theta : Atom List
8. l_subset(Atom;theta;vs-FormFvs(right))
9. FormSafe1'(left) theta
10. set-equal(Atom;vs-FormFvs(right);theta)
11. FormSafe1''(left) vs-FormFvs(right)
⊢ l_subset(Atom;vs-vs-FormFvs(right);vs-theta)

---

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


By

---

Latex:
(((RWO  "4<  5<"  0  THENA  Auto)  THEN  MoveToConcl  (-3))
  THEN  (RWO  "FormSafe-iff-FormSafe1'<"  0\mcdot{}  THENA  Auto)
  THEN  (BLemma  `FormSafe1\_functionality`    THENA  Auto))

---

Home Index