'a:S. 
  all
  (f:'a  hbool. all
  (f:'a  hbool. (x1:'a. all
  (f:'a  hbool. (x1:'a. (x2:'a. implies
  (f:'a  hbool. (x1:'a. (x2:'a. (and(f(x1),not(f(x2)))
  (f:'a  hbool. (x1:'a. (x2:'a. ,not(equal(x1,x2))))))

None

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