---

Step * 1 2 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 
⊢ [] ≤ [e1, e2]
BY
{ (BLemma `nil_iseg` 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.  \mneg{}e1  \mleq{}loc  e 
\mvdash{}  []  \mleq{}  [e1,  e2]


By

(BLemma  `nil\_iseg`  THEN  Auto)

---

Home Index