---

Step * 4 1 of Lemma FormSafe1_functionality


1. C : Type
2. body : Form(C)
3. ∀vs,ws:Atom List.  (l_subset(Atom;ws;vs) ⇒ (FormSafe1(body) vs) ⇒ (FormSafe1(body) ws))
4. vs : Atom List
5. ws : Atom List
6. l_subset(Atom;ws;vs)
7. ↑null(vs)
8. FormSafe1(body) []
⊢ ws = [] ∈ (Atom List)
BY
{ ((RW assert_pushdownC (-2) THENA Auto) THEN HypSubst' (-2) (-3)) }

1
1. C : Type
2. body : Form(C)
3. ∀vs,ws:Atom List.  (l_subset(Atom;ws;vs) ⇒ (FormSafe1(body) vs) ⇒ (FormSafe1(body) ws))
4. vs : Atom List
5. ws : Atom List
6. l_subset(Atom;ws;[])
7. vs = [] ∈ (Atom List)
8. FormSafe1(body) []
⊢ ws = [] ∈ (Atom List)

---

Latex:

---

Latex:

1.  C  :  Type
2.  body  :  Form(C)
3.  \mforall{}vs,ws:Atom  List.    (l\_subset(Atom;ws;vs)  {}\mRightarrow{}  (FormSafe1(body)  vs)  {}\mRightarrow{}  (FormSafe1(body)  ws))
4.  vs  :  Atom  List
5.  ws  :  Atom  List
6.  l\_subset(Atom;ws;vs)
7.  \muparrow{}null(vs)
8.  FormSafe1(body)  []
\mvdash{}  ws  =  []


By

---

Latex:
((RW  assert\_pushdownC  (-2)  THENA  Auto)  THEN  HypSubst'  (-2)  (-3))

---

Home Index