(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. n : 
2. m : 
3. nm
  firstn(n;upto(m)) ~ upto(n)
By: Subst (upto(m) ~ (upto(n) @ map(x.x+n;upto(m-n)))) 0

Generated subgoals:

1   upto(m) ~ (upto(n) @ map(x.x+n;upto(m-n)))
1 step
2   firstn(n;upto(n) @ map(x.x+n;upto(m-n))) ~ upto(n)
3 steps

About:
addsubtractlambdasqequal
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