---

Step * of Lemma lifting-spread-spread

∀[p,F,G:Top].  (let c,d = let a,b = p in F[a;b] in G[c;d] ~ let a,b = p in let c,d = F[a;b] in G[c;d])
BY
{ ProveLiftingLemma }

---

Latex:

---

Latex:
\mforall{}[p,F,G:Top].
    (let  c,d  =  let  a,b  =  p 
                          in  F[a;b] 
      in  G[c;d]  \msim{}  let  a,b  =  p 
                              in  let  c,d  =  F[a;b] 
                                    in  G[c;d])


By

---

Latex:
ProveLiftingLemma

---

Home Index