'a,'b:S.
  all
  (b:'b. all
  (b:'b. (a:'a. all
  (b:'b. (a:'a. (y:'b. all
  (b:'b. (a:'a. (y:'b. (x:'a. equal
  (b:'b. (a:'a. (y:'b. (x:'a. (equal(pair(x,y),pair(a,b))
  (b:'b. (a:'a. (y:'b. (x:'a. ,and(equal(x,a),equal(y,b)))))))

None

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