---

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


1. C : Type
2. left : Form(C)
3. right : Form(C)
4. vs : Atom List
5. as : Atom List
6. bs : Atom List
7. FormSafe1(left) as
8. FormSafe1(right) bs
9. x : Atom
10. ¬((x ∈ as) ∧ (x ∈ FormFvs(right)))
11. (x ∈ vs) ⇐⇒ (x ∈ as @ bs)
⊢ (x ∈ as) ⇒ ((x ∈ vs) ∧ (¬(x ∈ FormFvs(right))))
BY
{ (RWO "member_append" (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  C  :  Type
2.  left  :  Form(C)
3.  right  :  Form(C)
4.  vs  :  Atom  List
5.  as  :  Atom  List
6.  bs  :  Atom  List
7.  FormSafe1(left)  as
8.  FormSafe1(right)  bs
9.  x  :  Atom
10.  \mneg{}((x  \mmember{}  as)  \mwedge{}  (x  \mmember{}  FormFvs(right)))
11.  (x  \mmember{}  vs)  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  as  @  bs)
\mvdash{}  (x  \mmember{}  as)  {}\mRightarrow{}  ((x  \mmember{}  vs)  \mwedge{}  (\mneg{}(x  \mmember{}  FormFvs(right))))


By

---

Latex:
(RWO  "member\_append"  (-1)  THEN  Auto)

---

Home Index