'b,'a:S.
  all
  (f:'a  'b. equal
  (f:'a  'b. (one_one(f)
  (f:'a  'b. ,all
  (f:'a  'b. ,(x1:'a. all
  (f:'a  'b. ,(x1:'a. (x2:'a. implies(equal(f(x1),f(x2)),equal(x1,x2))))))

1

1. 'b : S 2. 'a : S 3. f : 'a'b   (one_one('a;'b;f)) = (x1,x2:'a.  ((f(x1)) = (f(x2)))(x1 = x2))

3 steps

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