---

Step * 1 1 of Lemma es-hist-partition


1. Info : Type
2. es : EO+(Info)
3. e1 : E
4. e2 : E
5. e : E
6. (e1 <loc e)
7. e ≤loc e2 
8. [e1, e2] = ([e1, pred(e)] @ [e, e2]) ∈ (E List)
⊢ [e1, e2] = ([e1, pred(e)] @ [e, e2]) ∈ (E List)
BY
{ ((StrongRevHypSubst (-1) 0) THEN Try (Complete (Auto))) }

---

Latex:



1.  Info  :  Type
2.  es  :  EO+(Info)
3.  e1  :  E
4.  e2  :  E
5.  e  :  E
6.  (e1  <loc  e)
7.  e  \mleq{}loc  e2 
8.  [e1,  e2]  =  ([e1,  pred(e)]  @  [e,  e2])
\mvdash{}  [e1,  e2]  =  ([e1,  pred(e)]  @  [e,  e2])


By

((StrongRevHypSubst  (-1)  0)  THEN  Try  (Complete  (Auto)))

---

Home Index