---

Step * of Lemma es-before_wf

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

1
∀the_es:EO. ∀e:E.  (before(e) ∈ E List)

---

Latex:

---

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


By

---

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

---

Home Index