---

Step * of Lemma es-hist-one-one

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[e1,e2,e3:E].
  (e2 = e3 ∈ E) supposing ((es-hist(es;e1;e2) = es-hist(es;e1;e3) ∈ (Info List)) and e1 ≤loc e3  and e1 ≤loc e2 )
BY
{ Auto⋅ }

1
1. Info : Type
2. es : EO+(Info)
3. e1 : E
4. e2 : E
5. e3 : E
6. e1 ≤loc e2 
7. e1 ≤loc e3 
8. es-hist(es;e1;e2) = es-hist(es;e1;e3) ∈ (Info List)
⊢ e2 = e3 ∈ E

---

Latex:


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


By

Auto\mcdot{}

---

Home Index