---

Step * 1 of Lemma es-causl-total


1. es : EO@i'
2. e : E@i
3. e' : E@i
4. loc(e) = loc(e') ∈ Id
5. e = e' ∈ es-base-E(es)
⊢ e = e' ∈ E
BY
{ (DVar `e' THEN Unfold `es-E` 0 THEN All (Folds ``es-base-E es-dom``) THEN EqTypeCD THEN Auto)⋅ }

---

Latex:



1.  es  :  EO@i'
2.  e  :  E@i
3.  e'  :  E@i
4.  loc(e)  =  loc(e')
5.  e  =  e'
\mvdash{}  e  =  e'


By

(DVar  `e'  THEN  Unfold  `es-E`  0  THEN  All  (Folds  ``es-base-E  es-dom``)  THEN  EqTypeCD  THEN  Auto)\mcdot{}

---

Home Index