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