---

Step * of Lemma decidable__es-E-equal

∀the_es:EO. ∀e,e':E.  Dec(e = e' ∈ E)
BY
{ (Auto THEN RWO "assert-es-eq-E" 0 THEN Auto) }

---

Latex:


\mforall{}the$_{es}$:EO.  \mforall{}e,e':E.    Dec(e  =  e')


By

(Auto  THEN  RWO  "assert-es-eq-E"  0  THEN  Auto)

---

Home Index