---

Step * of Lemma lifting-callbyvalue-callbyvalue

∀[a,F,G:Top].  (eval x = eval y = a in F[y] in G[x] ~ eval y = a in eval x = F[y] in   G[x])
BY
{ ProveLiftingLemma }

---

Latex:

---

Latex:
\mforall{}[a,F,G:Top].    (eval  x  =  eval  y  =  a  in  F[y]  in  G[x]  \msim{}  eval  y  =  a  in  eval  x  =  F[y]  in      G[x])


By

---

Latex:
ProveLiftingLemma

---

Home Index