(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 1 1 1 2 2 3
1. 
2. 
3. n : 
4. 0<n
5. f : 
  (one_one(;;f) & onto(;;f))  Prop
By: ((DTerm 0 5) THEN (Analyze 5)) THEN StrongAuto
THEN
Try (Complete (Unfold `label` 0))

Generated subgoals:

None

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

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