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

None

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