'a,'b:S.
  all
  (x:'a. all
  (x:'a. (y:'b. equal
  (x:'a. (y:'b. (pair(x,y)
  (x:'a. (y:'b. ,select(p:hprod('a; 'b). equal(rep_prod(p),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))))

6 steps

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