(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 1 2
1. n : 
2. 0<n
3. ||upto(n-1)|| ~ (n-1)
4. n = 0
  ||upto(n-1) @ [(n-1)]|| ~ n
By: Subst' (||upto(n-1) @ [(n-1)]|| = ||upto(n-1)||+1) 0

Generated subgoals:

1   ||upto(n-1) @ [(n-1)]|| = ||upto(n-1)||+1  
1 step
2   (||upto(n-1)||+1) ~ n
1 step

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