---

Step * of Lemma es-loc-pred

∀[the_es:EO]. ∀[e:E].  loc(pred(e)) = loc(e) ∈ Id supposing ¬↑first(e)
BY
{ (Auto THEN FLemma `es-pred_property` [-1] THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[the$_{es}$:EO].  \mforall{}[e:E].    loc(pred(e))  =  loc(e)  supposing  \mneg{}\muparrow{}first(e)


By

---

Latex:
(Auto  THEN  FLemma  `es-pred\_property`  [-1]  THEN  Auto)

---

Home Index