---

Step * 2 of Lemma last-es-hist


1. Info : Type
2. es : EO+(Info)
3. e1 : E
4. e2 : E
5. e1 ≤loc e2 
⊢ info(last([e1, e2])) ~ info(e2)
BY
{ (EqCD THEN Try (Trivial) THEN BLemma `es-interval-last` THEN Auto) }

---

Latex:



1.  Info  :  Type
2.  es  :  EO+(Info)
3.  e1  :  E
4.  e2  :  E
5.  e1  \mleq{}loc  e2 
\mvdash{}  info(last([e1,  e2]))  \msim{}  info(e2)


By

(EqCD  THEN  Try  (Trivial)  THEN  BLemma  `es-interval-last`  THEN  Auto)

---

Home Index