rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex
.
H >> 
ext x:A#B by intro product A new x 
ext B
.
H >> x:A#B in 
by intro [new y]
*
>> A in 
*
y:A >> B[y/x]
in 
.
H >> 
ext A#B by intro product
*
>> 
ext A
*
>> 
ext B
.
H >> A#B in 
by intro
*
>> A in 
*
>> B in 
rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex
.
H >> x:A#B ext <a,b> by intro at 
a [new y] 
.
H >> <a,b> in x:A#B by intro at 
[new y]
*
>> a in A
*
>> b in B[a/x]
*
y:A >> B[y/x]
in 
.
H >> A#B ext <a,b> by intro
*
>> A ext a
*
>> B ext b
.
H >> <a,b> in A#B by intro
*
>> a in A
*
>> b in B
rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex
.
H,z:(x:A#B),
>> T
ext spread(z;u,v.t)
by elim z new u,v
.
H >> spread(e;
) in T[e/z]
*
by intro [over 
] using w:A#B [new u,v]
*
>> e in w:A#B
*
u:A,v:B[u/w]
,e=<u,v> in w:A#B >>
t[u,v/x,y]
in T[<u,v>/z]
rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex
.
H >> spread(<a,b>;
) = s in T by reduce 1