---

Step * of Lemma dlo-refl

∀a:dl-Obj(). (↑a ≤ a)
BY
{ (dlObjInduction THEN Try (DloLeReduce (0)) THEN Auto THEN Try ((RWO  "assert-dlo_eq" 0 THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}a:dl-Obj().  (\muparrow{}a  \mleq{}  a)


By

---

Latex:
(dlObjInduction  THEN  Try  (DloLeReduce  (0))  THEN  Auto  THEN  Try  ((RWO    "assert-dlo\_eq"  0  THEN  Auto)))

---

Home Index