---

Step * 1 1 1 of Lemma es-hist-iseg


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
8. e1 ≤loc e 
9. [e1, e] ≤ [e1, e2] ⇐⇒ e ≤loc e2 
⊢ [e1, e] ≤ [e1, e2]
BY
{ ((D (-1)) THEN (D (-1)) THEN Auto) }

---

Latex:



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)
7.  e  \mleq{}loc  e2  @i
8.  e1  \mleq{}loc  e 
9.  [e1,  e]  \mleq{}  [e1,  e2]  \mLeftarrow{}{}\mRightarrow{}  e  \mleq{}loc  e2 
\mvdash{}  [e1,  e]  \mleq{}  [e1,  e2]


By

((D  (-1))  THEN  (D  (-1))  THEN  Auto)

---

Home Index