∀[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:
\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 )