'c,'a,'b:S.
  all
  (f:hprod('a; 'b)  'c. all
  (f:hprod('a; 'b)  'c. (x:'a. all
  (f:hprod('a; 'b)  'c. (x:'a. (y:'b. equal(curry(f,x,y),f(pair(x,y))))))

None

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