---

Step * of Lemma es-init-eq

∀[es:EO]. ∀[e,e':E].  es-init(es;e) = es-init(es;e') ∈ E supposing loc(e) = loc(e') ∈ Id
BY
{ (UniformUnivCD Auto THEN Repeat (MoveToConcl (-1))) }

1
∀es:EO. ∀e,e':E.  ((loc(e) = loc(e') ∈ Id) ⇒ (es-init(es;e) = es-init(es;e') ∈ E))

---

Latex:


\mforall{}[es:EO].  \mforall{}[e,e':E].    es-init(es;e)  =  es-init(es;e')  supposing  loc(e)  =  loc(e')


By

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

---

Home Index