1. m : 
2. 0<m
3. n:(m-1+1). upto(m-1) ~ (upto(n) @ map(x.x+n;upto(m-1-n)))
4. n : (m+1)
5. n = m
  upto(m) ~ (upto(n) @ map(x.x+n;upto(m-n)))

By:	Subst' (m-n = 0) 0 THEN Reduce 0 THEN Try (Complete Auto) THEN RWO Thm* l:T List. (l @ nil) ~ l 0 THEN Analyze

None

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