---

Step * of Lemma spread-spread

∀[t:Top × Top]. ∀[P,Q:Top].  (let x,y = let a,b = t in P[a;b] in Q[x;y] ~ let a,b = t in let x,y = P[a;b] in Q[x;y])
BY
{ RepeatFor 3 ((D 0 THENA Auto))
THEN D 1
THEN Reduce 0
THEN Auto }

---

Latex:

---

Latex:
\mforall{}[t:Top  \mtimes{}  Top].  \mforall{}[P,Q:Top].
    (let  x,y  =  let  a,b  =  t 
                          in  P[a;b] 
      in  Q[x;y]  \msim{}  let  a,b  =  t 
                              in  let  x,y  =  P[a;b] 
                                    in  Q[x;y])


By

---

Latex:
RepeatFor  3  ((D  0  THENA  Auto))
THEN  D  1
THEN  Reduce  0
THEN  Auto

---

Home Index