---

Step * of Lemma cbv-sqequal0

∀[a:Base]. eval x = a in 0 ~ 0 supposing (a)↓
BY
{ (SqReasoning THEN Try ((RW (AddrC [1] CallByValue2C) 0 THEN Complete (Auto)))) }

---

Latex:

---

Latex:
\mforall{}[a:Base].  eval  x  =  a  in  0  \msim{}  0  supposing  (a)\mdownarrow{}


By

---

Latex:
(SqReasoning  THEN  Try  ((RW  (AddrC  [1]  CallByValue2C)  0  THEN  Complete  (Auto))))

---

Home Index