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

1

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

5 steps

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