---

Step * 1 of Lemma es-pred-loc-base


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

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

---

Latex:



1.  es  :  EO@i'
2.  e  :  es-base-E(es)@i
\mvdash{}  loc(pred(e))  =  loc(e)


By

MoveToConcl  (-1)

---

Home Index