---

Step * 1 of Lemma es-before_wf


∀the_es:EO. ∀e:E.  (before(e) ∈ E List)
BY
{ StrongLocLessInd⋅ }

1
1. the_es : EO@i'
2. e : E@i
3. ∀x:E. ((x <loc e) ⇒ (before(x) ∈ E List))
⊢ before(e) ∈ E List

---

Latex:



\mforall{}the$_{es}$:EO.  \mforall{}e:E.    (before(e)  \mmember{}  E  List)


By

StrongLocLessInd\mcdot{}

---

Home Index