Nuprl - Proof: hcomma def 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hcomma def 1 1

'a,'b:S, x:'a, y:'b.

<x,y> = (@x@0:hprod('a; 'b). ((rep_prod(x@0)) =

(mk_pair(x,y))))

By:

Auto

Generated subgoal:

1 1. 'a : S
2. 'b : S
3. x : 'a
4. y : 'b
<x,y> = (@x@0:hprod('a; 'b). ((rep_prod(x@0)) = (mk_pair(x,y))))
4 steps

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html