---

Step * 1 of Lemma decidable__equal-es-E


1. es : EO@i'
2. e : E@i
3. e' : E@i
4. ∀[x,y:E].  uiff(x = y ∈ E;↑(es-eq(es) x y))
⊢ Dec(e = e' ∈ E)
BY
{ (RWO "-1" 0 THEN Auto)⋅ }

---

Latex:



1.  es  :  EO@i'
2.  e  :  E@i
3.  e'  :  E@i
4.  \mforall{}[x,y:E].    uiff(x  =  y;\muparrow{}(es-eq(es)  x  y))
\mvdash{}  Dec(e  =  e')


By

(RWO  "-1"  0  THEN  Auto)\mcdot{}

---

Home Index