---

Step * of Lemma decidable__equal-es-E

∀es:EO. ∀e,e':E.  Dec(e = e' ∈ E)
BY
{ (Auto THEN (InstLemma `deq_property` [⌈E⌉; ⌈es-eq(es)⌉]⋅ THENA Auto)) }

1
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)

---

Latex:


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


By

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

---

Home Index