---

Step * of Lemma decidable__equal-es-base-E

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

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

---

Latex:

---

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


By

---

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

---

Home Index