---

Step * of Lemma eo-forward-first

∀[Info:Type]. ∀[eo:EO+(Info)]. ∀[e:E]. ∀[e':E].  (first(e') ~ if loc(e') = loc(e) then e' = e else first(e') fi )
BY
{ Auto }

1
1. Info : Type
2. eo : EO+(Info)
3. e : E
4. e' : E
⊢ first(e') = if loc(e') = loc(e) then e' = e else first(e') fi 

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[eo:EO+(Info)].  \mforall{}[e:E].  \mforall{}[e':E].
    (first(e')  \msim{}  if  loc(e')  =  loc(e)  then  e'  =  e  else  first(e')  fi  )


By

---

Latex:
Auto

---

Home Index