---

Step * 1 2 of Lemma eo-forward-forward

.....wf..... 
1. Info : Type
2. eo : EO+(Info)
3. e1 : E
4. e2 : E
5. e1 ≤loc e2 
⊢ es-base-E(eo) = es-base-E(eo) ∈ Type
BY
{ Auto }

---

Latex:


.....wf..... 
1.  Info  :  Type
2.  eo  :  EO+(Info)
3.  e1  :  E
4.  e2  :  E
5.  e1  \mleq{}loc  e2 
\mvdash{}  es-base-E(eo)  =  es-base-E(eo)


By

Auto

---

Home Index