---

Step * of Lemma lifting-decide-spread

∀[a,F,A,B:Top].
  (case let u,v = a in F[u;v] of inl(x) => A[x] | inr(x) => B[x] ~ let u,v = a 
                                                                   in case F[u;v] of inl(x) => A[x] | inr(x) => B[x])
BY
{ ProveLiftingLemma }

---

Latex:

---

Latex:
\mforall{}[a,F,A,B:Top].
    (case  let  u,v  =  a  in  F[u;v]  of  inl(x)  =>  A[x]  |  inr(x)  =>  B[x]  \msim{}  let  u,v  =  a 
                                                                                                                                      in  case  F[u;v]
                                                                                                                                              of  inl(x)  =>
                                                                                                                                              A[x]
                                                                                                                                              |  inr(x)  =>
                                                                                                                                              B[x])


By

---

Latex:
ProveLiftingLemma

---

Home Index