Def one_one == f:'a'b. one_one('a;'b;f)

is mentioned by

Thm* exists(f:hind  hind. and(one_one(f),not(onto(f))))	[hinfinity_ax]
Thm* 'b,'a:S. Thm* all Thm* (f:'a  'b. equal Thm* (f:'a  'b. (one_one(f) Thm* (f:'a  'b. ,all Thm* (f:'a  'b. ,(x1:'a. all Thm* (f:'a  'b. ,(x1:'a. (x2:'a. implies Thm* (f:'a  'b. ,(x1:'a. (x2:'a. (equal(f(x1),f(x2)) Thm* (f:'a  'b. ,(x1:'a. (x2:'a. ,equal(x1,x2))))))	[hone_one_def]

Try larger context: HOLlib IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html