---

Step * 1 1 of Lemma es-before_wf


1. the_es : EO@i'
2. e : E@i
3. ∀x:E. ((x <loc e) ⇒ (before(x) ∈ E List))
⊢ before(e) ∈ E List
BY
{ (RecUnfold `es-before` 0 THEN SplitOnConclITE THEN Auto THEN BHyp 3 THEN Auto THEN BLemma `es-pred-locl` THEN Auto) }

---

Latex:



1.  the$_{es}$  :  EO@i'
2.  e  :  E@i
3.  \mforall{}x:E.  ((x  <loc  e)  {}\mRightarrow{}  (before(x)  \mmember{}  E  List))
\mvdash{}  before(e)  \mmember{}  E  List


By

(RecUnfold  `es-before`  0
  THEN  SplitOnConclITE
  THEN  Auto
  THEN  BHyp  3
  THEN  Auto
  THEN  BLemma  `es-pred-locl`
  THEN  Auto)

---

Home Index