---

Step * of Lemma lifting-decide-decide

∀[a,F,G,A,B:Top].
  (case case a of inl(x) => F[x] | inr(x) => G[x] of inl(x) => A[x] | inr(x) => B[x] ~ case a
   of inl(x) =>
   case F[x] of inl(y) => A[y] | inr(y) => B[y]
   | inr(x) =>
   case G[x] of inl(y) => A[y] | inr(y) => B[y])
BY
{ ProveLiftingLemma }

---

Latex:

---

Latex:
\mforall{}[a,F,G,A,B:Top].
    (case  case  a  of  inl(x)  =>  F[x]  |  inr(x)  =>  G[x]  of  inl(x)  =>  A[x]  |  inr(x)  =>  B[x]  \msim{}  case  a
      of  inl(x)  =>
      case  F[x]  of  inl(y)  =>  A[y]  |  inr(y)  =>  B[y]
      |  inr(x)  =>
      case  G[x]  of  inl(y)  =>  A[y]  |  inr(y)  =>  B[y])


By

---

Latex:
ProveLiftingLemma

---

Home Index