Def hind == 

is mentioned by

Thm* exists(f:hind  hind. and(one_one(f),not(onto(f))))

[hinfinity_ax]

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