---

Step * 1 of Lemma decidable__equal_es-E-interface

.....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))
BY
{ ((InstLemma `deq_property` [⌈E(X)⌉;⌈es-eq(es)⌉]⋅ THENA Auto) THEN RWO  "-1" 0 THEN Auto) }

---

Latex:


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


By

((InstLemma  `deq\_property`  [\mkleeneopen{}E(X)\mkleeneclose{};\mkleeneopen{}es-eq(es)\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  RWO    "-1"  0  THEN  Auto)

---

Home Index