---

Step * of Lemma lifting-isaxiom-spread

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

---

Latex:

---

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


By

---

Latex:
ProveLiftingLemma

---

Home Index