(7steps 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: firstn upto 1 1
1. n : 
2. m : 
3. nm
  upto(m) ~ (upto(n) @ map(x.x+n;upto(m-n)))
By: BackThru Thm* m:, n:(m+1). upto(m) ~ (upto(n) @ map(x.x+n;upto(m-n)))

Generated subgoals:

None

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

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