---

Step * of Lemma es-le_weakening_eq

∀es:EO. ∀a,b:E.  a ≤loc b  supposing a = b ∈ E
BY
{ (Unfold `es-le` 0 THEN Auto) }

---

Latex:


\mforall{}es:EO.  \mforall{}a,b:E.    a  \mleq{}loc  b    supposing  a  =  b


By

(Unfold  `es-le`  0  THEN  Auto)

---

Home Index