---

Step * of Lemma sqequal-spread-cbva-weak

∀[a:Top × Top]. ∀[b,F:Top].  (let x ←─ a in let u,v = x in F[u;v] ~ let u,v = a in let x ←─ u in let y ←─ v in F[x;y])
BY
{ ((UnivCD THENA Auto)
   THEN DProdsAndUnions
   THEN SymbComp 0
   THEN RWO "lifting-callbyvalueall-pair" 0
   THEN Reduce 0
   THEN Auto) }

---

Latex:


\mforall{}[a:Top  \mtimes{}  Top].  \mforall{}[b,F:Top].
    (let  x  \mleftarrow{}{}  a
      in  let  u,v  =  x 
            in  F[u;v]  \msim{}  let  u,v  =  a 
                                    in  let  x  \mleftarrow{}{}  u
                                          in  let  y  \mleftarrow{}{}  v
                                                in  F[x;y])


By

((UnivCD  THENA  Auto)
  THEN  DProdsAndUnions
  THEN  SymbComp  0
  THEN  RWO  "lifting-callbyvalueall-pair"  0
  THEN  Reduce  0
  THEN  Auto)

---

Home Index