(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 1
1. 
2. 
3. n : 
4. 0<n
  (m:. m+1)  
By: Analyze

Generated subgoals:

None

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

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