---

Step * 1 of Lemma decidable__es-le


1. the_es : EO@i'
2. e' : E@i
3. e : E@i
⊢ Dec(e = e' ∈ E)
BY
{ Auto }

---

Latex:



1.  the$_{es}$  :  EO@i'
2.  e'  :  E@i
3.  e  :  E@i
\mvdash{}  Dec(e  =  e')


By

Auto

---

Home Index