---

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


1. C : Type
2. left : Form(C)
3. right : Form(C)
4. vs : Atom List
5. phi : Atom List
6. l_subset(Atom;phi;vs-FormFvs(left))
7. FormSafe1(left) vs-phi
8. FormSafe1(right) phi
9. set-equal(Atom;vs;vs-phi @ phi)
10. FormSafe1(left) vs-phi
11. FormSafe1(right) phi
12. x : Atom
13. (x ∈ phi) ∧ (x ∈ FormFvs(left))
⊢ False
BY
{ ((D 6 With ⌜x⌝  THEN Auto) THEN RWO "member-list-diff" (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  C  :  Type
2.  left  :  Form(C)
3.  right  :  Form(C)
4.  vs  :  Atom  List
5.  phi  :  Atom  List
6.  l\_subset(Atom;phi;vs-FormFvs(left))
7.  FormSafe1(left)  vs-phi
8.  FormSafe1(right)  phi
9.  set-equal(Atom;vs;vs-phi  @  phi)
10.  FormSafe1(left)  vs-phi
11.  FormSafe1(right)  phi
12.  x  :  Atom
13.  (x  \mmember{}  phi)  \mwedge{}  (x  \mmember{}  FormFvs(left))
\mvdash{}  False


By

---

Latex:
((D  6  With  \mkleeneopen{}x\mkleeneclose{}    THEN  Auto)  THEN  RWO  "member-list-diff"  (-1)  THEN  Auto)

---

Home Index