(46steps total) PrintForm Definitions hol num Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: num iso 2 1 2 1 1 1 1 1
1. f : 
2. one_one(;;f)
3. onto(;;f)
  (x:. f(x)) = f
By: Ext THEN Simp THEN StrongAuto

Generated subgoals:

None

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

(46steps total) PrintForm Definitions hol num Sections HOLlib Doc