Nuprl - Proof: length upto 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: length upto 1

1. n :

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

||upto(n)|| ~ n

By:	RecUnfold `upto` 0 THEN SplitOnConclITE

Generated subgoals:

1 4. n = 0
||nil|| ~ n
Auto

2 4. n = 0
||upto(n-1) @ [(n-1)]|| ~ n
3 steps

About:

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

1	4. n = 0 \|\|nil\|\| ~ n	Auto
2	4. n = 0 \|\|upto(n-1) @ [(n-1)]\|\| ~ n	3 steps