---

Step * 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
⊢ [e1, e] ≤ [e1, e2]
BY
{ (Decide ⌈e1 ≤loc e ⌉⋅ 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
8. e1 ≤loc e 
⊢ [e1, e] ≤ [e1, e2]

2
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, e] ≤ [e1, e2]

---

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
\mvdash{}  [e1,  e]  \mleq{}  [e1,  e2]


By

(Decide  \mkleeneopen{}e1  \mleq{}loc  e  \mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index