(2steps total) PrintForm Definitions mb event system 1 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: upto wf
  n:. upto(n)  n List
By: InductionOnNat THEN RecUnfold `upto` 0 THEN Reduce 0

Generated subgoal:

1 1. n : 
2. 0<n
3. upto(n-1)  (n-1) List
  upto(n-1)  n List
1 step

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

(2steps total) PrintForm Definitions mb event system 1 Sections EventSystems Doc