(13steps 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: upto decomp 1
1. n : 1
  nil ~ (upto(n) @ map(x.x+n;upto(0-n)))
By: Subst (n = 0) 0 THEN Reduce 0

Generated subgoals:

None

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

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