(4steps total) PrintForm Definitions Lemmas mb event system 1 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: select upto
  m:, n:m. upto(m)[n] = n
By: InductionOnNat THEN RecUnfold `upto` 0 THEN SplitOnConclITE THEN Decide (n<m-1)

Generated subgoals:

1 1. m : 
2. 0<m
3. n:(m-1). upto(m-1)[n] = n
4. n : m
5. m = 0
6. n<m-1
  (upto(m-1) @ [(m-1)])[n] = n
1 step
2 1. m : 
2. 0<m
3. n:(m-1). upto(m-1)[n] = n
4. n : m
5. m = 0
6. n<m-1
  (upto(m-1) @ [(m-1)])[n] = n
2 steps

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

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