(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
1. n : 
2. 0<n
3. ||upto(n-1)|| ~ (n-1)
4. n = 0
  ||upto(n-1) @ [(n-1)]|| = ||upto(n-1)||+1  
By: RWO Thm* as,bs:T List. ||as @ bs|| = ||as||+||bs||   0

Generated subgoals:

None

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