---

Step * of Lemma evalall-sqle

∀[x:Base]. evalall(x) ≤ x supposing (evalall(x))↓
BY
{ ((UnivCD THENA Auto) THEN RWO "evalall-sqequal" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[x:Base].  evalall(x)  \mleq{}  x  supposing  (evalall(x))\mdownarrow{}


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RWO  "evalall-sqequal"  0  THEN  Auto)

---

Home Index