---

Step * of Lemma eo-forward-forward2

∀[Info:Type]. ∀[eo:EO+(Info)]. ∀[e1:E]. ∀[e2:E].  eo.e1.e2 = eo.e2 ∈ EO+(Info) supposing loc(e2) = loc(e1) ∈ Id
BY
{ (Auto THEN BLemma `eo-forward-forward` THEN Auto) }

---

Latex:


\mforall{}[Info:Type].  \mforall{}[eo:EO+(Info)].  \mforall{}[e1:E].  \mforall{}[e2:E].    eo.e1.e2  =  eo.e2  supposing  loc(e2)  =  loc(e1)


By

(Auto  THEN  BLemma  `eo-forward-forward`  THEN  Auto)

---

Home Index