---

Step * of Lemma lifting-decide-callbyvalue

∀[a,H,F,G:Top].
  (case eval z = a in H[z] of inl(x) => F[x] | inr(x) => G[x] ~ eval z = a in
                                                                case H[z] of inl(x) => F[x] | inr(x) => G[x])
BY
{ ProveLiftingLemma }

---

Latex:

---

Latex:
\mforall{}[a,H,F,G:Top].
    (case  eval  z  =  a  in  H[z]  of  inl(x)  =>  F[x]  |  inr(x)  =>  G[x]  \msim{}  eval  z  =  a  in
                                                                                                                                case  H[z]
                                                                                                                                  of  inl(x)  =>
                                                                                                                                  F[x]
                                                                                                                                  |  inr(x)  =>
                                                                                                                                  G[x])


By

---

Latex:
ProveLiftingLemma

---

Home Index