---

Step * of Lemma lifting-decide-int_eq

∀[n,m,a,b,A,B:Top].
  (case if n=m  then a  else b of inl(x) => A[x] | inr(x) => B[x] ~ if n=m
                                                                       then case a of inl(x) => A[x] | inr(x) => B[x]
                                                                       else case b of inl(x) => A[x] | inr(x) => B[x])
BY
{ ProveLiftingLemma }

---

Latex:

---

Latex:
\mforall{}[n,m,a,b,A,B:Top].
    (case  if  n=m    then  a    else  b  of  inl(x)  =>  A[x]  |  inr(x)  =>  B[x]  \msim{}  if  n=m
                                                                                                                                              then  case  a
                                                                                                                                                          of  inl(x)  =>
                                                                                                                                                          A[x]
                                                                                                                                                          |  inr(x)  =>
                                                                                                                                                          B[x]
                                                                                                                                              else  case  b
                                                                                                                                                          of  inl(x)  =>
                                                                                                                                                          A[x]
                                                                                                                                                          |  inr(x)  =>
                                                                                                                                                          B[x])


By

---

Latex:
ProveLiftingLemma

---

Home Index