---

Step * of Lemma lifting-callbyvalue-decide

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

---

Latex:

---

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


By

---

Latex:
ProveLiftingLemma

---

Home Index