---

Step * of Lemma test-cbva-normalize

∀[a,B:Top].  (let x ⟵ a in <let y ⟵ x in B[y], let z ⟵ a in B[z] + 22, eval w = a in B[w] + 3 + 1> ~ let x ⟵ a in <B\000C[x], B[x] + 22, (B[x] + 3) + 1>)
BY
{ (NormalizeCbv 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a,B:Top].    (let  x  \mleftarrow{}{}  a  in  <let  y  \mleftarrow{}{}  x  in  B[y],  let  z  \mleftarrow{}{}  a  in  B[z]  +  22,  eval  w  =  a  in  B[w]  +  3  +  1\000C>  \msim{}  let  x  \mleftarrow{}{}  a  in  <B[x],  B[x]  +  22,  (B[x]  +  3)  +  1>)


By

---

Latex:
(NormalizeCbv  0  THEN  Auto)

---

Home Index