---

Step * of Lemma lifting-callbyvalue-spread

∀[a,F,H:Top].  (eval x = let u,v = a in F[u;v] in H[x] ~ let u,v = a in eval x = F[u;v] in H[x])
BY
{ ProveLiftingLemma }

---

Latex:

---

Latex:
\mforall{}[a,F,H:Top].    (eval  x  =  let  u,v  =  a  in  F[u;v]  in  H[x]  \msim{}  let  u,v  =  a  in  eval  x  =  F[u;v]  in  H[x])


By

---

Latex:
ProveLiftingLemma

---

Home Index