---

Step * of Lemma es-hist-iseg

∀[Info:Type]
  ∀es:EO+(Info). ∀e1,e2,e:E.  e ≤loc e2  ⇒ es-hist(es;e1;e) ≤ es-hist(es;e1;e2) supposing loc(e2) = loc(e1) ∈ Id
BY
{ ((Auto THEN Unfold `es-hist` 0 THEN (BLemma `iseg_map` )⋅) THENA Auto) }

1
1. [Info] : Type
2. es : EO+(Info)@i'
3. e1 : E@i
4. e2 : E@i
5. e : E@i
6. loc(e2) = loc(e1) ∈ Id
7. e ≤loc e2 @i
⊢ [e1, e] ≤ [e1, e2]

---

Latex:


\mforall{}[Info:Type]
    \mforall{}es:EO+(Info).  \mforall{}e1,e2,e:E.
        e  \mleq{}loc  e2    {}\mRightarrow{}  es-hist(es;e1;e)  \mleq{}  es-hist(es;e1;e2)  supposing  loc(e2)  =  loc(e1)


By

((Auto  THEN  Unfold  `es-hist`  0  THEN  (BLemma  `iseg\_map`  )\mcdot{})  THENA  Auto)

---

Home Index