(2steps total) PrintForm Definitions hol arithmetic 1 Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nnsub wf
  m,n:. nnsub(m;n)  
By: Unfold `nnsub` 0

Generated subgoal:

1 1. m : 
2. n : 
3. m<n
  0m-n
1 step

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

(2steps total) PrintForm Definitions hol arithmetic 1 Sections HOLlib Doc