---

Step * of Lemma eo-strict-forward-first

∀[Info:Type]. ∀[eo:EO+(Info)]. ∀[e:E]. ∀[e':E].
  (first(e') ~ if loc(e') = loc(e) then es-eq(eo) pred(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 es-eq(eo) pred(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  es-eq(eo)  pred(e')  e  else  first(e')  fi  )


By

---

Latex:
Auto

---

Home Index