---

Step * of Lemma evalall-sqequal2

∀[x:Base]. evalall(x) ~ x supposing (evalall(x))↓
BY
{ % this used to be a different proof of evalall-sqequal, but now we only
     have one proof (since we have exceptions) %
     InstLemma `evalall-sqequal` [] THEN Hypothesis⋅ }

---

Latex:

---

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


By

---

Latex:
\%  this  used  to  be  a  different  proof  of  evalall-sqequal,  but  now  we  only
          have  one  proof  (since  we  have  exceptions)  \%
          InstLemma  `evalall-sqequal`  []  THEN  Hypothesis\mcdot{}

---

Home Index