---

Step * 1 of Lemma decidable__equal-es-base-E


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

---

Latex:



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


By

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

---

Home Index