IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
select upto21 1. m : 2. 0<m 3. n:(m-1). upto(m-1)[n] = n 4. n : m 5. m = 0
6. n<m-1
[(m-1)][(n-(m-1))] = n
By:
Subst' (n-(m-1) = 0) 0 THEN Reduce 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
n:
(m-1). upto(m-1)[n] = n
m = 0
[(m-1)][(n-(m-1))] = n
