---

Step * of Lemma lifting-ispair-spread

∀[a,b,c,F:Top].
  (if let x,y = a 
      in F[x;y] is a pair then b otherwise c ~ let x,y = a 
                                               in if F[x;y] is a pair then b otherwise c)
BY
{ ProveLiftingLemma }

---

Latex:

---

Latex:
\mforall{}[a,b,c,F:Top].
    (if  let  x,y  =  a 
            in  F[x;y]  is  a  pair  then  b  otherwise  c  \msim{}  let  x,y  =  a 
                                                                                              in  if  F[x;y]  is  a  pair  then  b  otherwise  c)


By

---

Latex:
ProveLiftingLemma

---

Home Index