(6steps 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: length upto
  n:. ||upto(n)|| ~ n
By: InductionOnNat THEN Reduce 0 THEN Try Trivial

Generated subgoal:

1 1. n : 
2. 0<n
3. ||upto(n-1)|| ~ (n-1)
  ||upto(n)|| ~ n
5 steps

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

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