Nuprl - Proof: length upto 1 2 2

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

1. n :

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

n = 0

(||upto(n-1)||+1) ~ n

By:	Subst (\|\|upto(n-1)\|\| ~ (n-1)) 0

Generated subgoals:

None

About:

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