(4steps total) PrintForm Definitions hol bool Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hinfinity ax
  exists(f:hind  hind. and(one_one(f),not(onto(f))))
By: Simpsetp [`hol_to_nuprl`] THEN StrongAuto

Generated subgoal:

1   f:(). one_one(;;f) & onto(;;f)
3 steps

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

(4steps total) PrintForm Definitions hol bool Sections HOLlib Doc