---

Step * of Lemma lifting-callbyvalueall-decide

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

---

Latex:

---

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


By

---

Latex:
ProveLiftingLemma

---

Home Index