---

Step * of Lemma es-pred-loc-base

∀es:EO. ∀e:es-base-E(es).  (loc(pred(e)) = loc(e) ∈ Id)
BY
{ Auto }

1
1. es : EO@i'
2. e : es-base-E(es)@i
⊢ loc(pred(e)) = loc(e) ∈ Id

---

Latex:


\mforall{}es:EO.  \mforall{}e:es-base-E(es).    (loc(pred(e))  =  loc(e))


By

Auto

---

Home Index