---

Step * 4 1 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;[])
7. vs = [] ∈ (Atom List)
8. FormSafe1(body) []
⊢ ws = [] ∈ (Atom List)
BY
{ (FLemma `l_subset_nil_right` [-3] THEN Auto) }

---

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;[])
7.  vs  =  []
8.  FormSafe1(body)  []
\mvdash{}  ws  =  []


By

---

Latex:
(FLemma  `l\_subset\_nil\_right`  [-3]  THEN  Auto)

---

Home Index