---

Step * of Lemma es-before_wf2

∀[the_es:EO]. ∀[e:E].  (before(e) ∈ {e':E| loc(e') = loc(e) ∈ Id}  List)
BY
{ (UniformUnivCD Auto THEN Repeat (MoveToConcl (-1))) }

1
∀the_es:EO. ∀e:E.  (before(e) ∈ {e':E| loc(e') = loc(e) ∈ Id}  List)

---

Latex:


\mforall{}[the$_{es}$:EO].  \mforall{}[e:E].    (before(e)  \mmember{}  \{e':E|  loc(e')  =  loc(e)\}    List)


By

(UniformUnivCD  Auto  THEN  Repeat  (MoveToConcl  (-1)))

---

Home Index