---

Step * 1 of Lemma null-es-hist


1. Info : Type
2. es : EO+(Info)@i'
3. e1 : E@i
4. e2 : E@i
5. loc(e2) = loc(e1) ∈ Id
6. (e2 <loc e1)
⊢ ↑null(es-hist(es;e1;e2)) ⇐⇒ (e2 <loc e1)
BY
{ (Unfold `es-hist` 0 THEN RWO "es-interval-is-nil" 0 THEN Reduce 0 THEN Auto) }

---

Latex:



1.  Info  :  Type
2.  es  :  EO+(Info)@i'
3.  e1  :  E@i
4.  e2  :  E@i
5.  loc(e2)  =  loc(e1)
6.  (e2  <loc  e1)
\mvdash{}  \muparrow{}null(es-hist(es;e1;e2))  \mLeftarrow{}{}\mRightarrow{}  (e2  <loc  e1)


By

(Unfold  `es-hist`  0  THEN  RWO  "es-interval-is-nil"  0  THEN  Reduce  0  THEN  Auto)

---

Home Index