---

Step * of Lemma decidable__es-le

∀the_es:EO. ∀e',e:E.  Dec(e ≤loc e' )
BY
{ (Auto
   THEN Unfold `es-le` 0
   THEN (BLemma `decidable__or` THENA Auto)
   THEN Try ((BLemma `decidable__es-locl` THENA Auto))) }

1
1. the_es : EO@i'
2. e' : E@i
3. e : E@i
⊢ Dec(e = e' ∈ E)

---

Latex:


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


By

(Auto
  THEN  Unfold  `es-le`  0
  THEN  (BLemma  `decidable\_\_or`  THENA  Auto)
  THEN  Try  ((BLemma  `decidable\_\_es-locl`  THENA  Auto)))

---

Home Index