---

Step * of Lemma decidable__equal_es-E-interface

∀[Info:Type]. ∀es:EO+(Info). ∀X:EClass(Top). ∀e,e':E(X).  Dec(e = e' ∈ E(X))
BY
{ Auto }

1
.....decidable?..... 
1. [Info] : Type
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. e : E(X)@i
5. e' : E(X)@i
⊢ Dec(e = e' ∈ E(X))

---

Latex:


\mforall{}[Info:Type].  \mforall{}es:EO+(Info).  \mforall{}X:EClass(Top).  \mforall{}e,e':E(X).    Dec(e  =  e')


By

Auto

---

Home Index