---

Step * of Lemma lifting-decide-less

∀[a,b,c,d,F,G:Top].
  (case if (a) < (b)  then c  else d of inl(x) => F[x] | inr(x) => G[x] ~ if (a) < (b)
                                                                             then case c
                                                                                   of inl(x) =>
                                                                                   F[x]
                                                                                   | inr(x) =>
                                                                                   G[x]
                                                                             else case d
                                                                                   of inl(x) =>
                                                                                   F[x]
                                                                                   | inr(x) =>
                                                                                   G[x])
BY
{ ProveLiftingLemma }

---

Latex:

---

Latex:
\mforall{}[a,b,c,d,F,G:Top].
    (case  if  (a)  <  (b)    then  c    else  d  of  inl(x)  =>  F[x]  |  inr(x)  =>  G[x]  \msim{}  if  (a)  <  (b)
                                                                                                                                                          then  case  c
                                                                                                                                                                      of  inl(x)  =>
                                                                                                                                                                      F[x]
                                                                                                                                                                      |  inr(x)  =>
                                                                                                                                                                      G[x]
                                                                                                                                                          else  case  d
                                                                                                                                                                      of  inl(x)  =>
                                                                                                                                                                      F[x]
                                                                                                                                                                      |  inr(x)  =>
                                                                                                                                                                      G[x])


By

---

Latex:
ProveLiftingLemma

---

Home Index