Nuprl - Proof: length nth tl 2

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

1. A : Type
2. A List
3. u : A
4. v : A List
5.

n:{0...||v||}. ||nth_tl(n;v)|| = ||v||-n

n:{0...||u.v||}. ||nth_tl(n;u.v)|| = ||u.v||-n

By:	Reduce 0 THEN ((Analyze 0) THEN (RecCaseSplit `nth_tl`))

Generated subgoals:

1 6. n : {0...||v||+1}
7. n0
||v||+1 = ||v||+1-n
Auto

2 6. n : {0...||v||+1}
7. 0<n
||nth_tl(n-1;v)|| = ||v||+1-n
1 step

About:

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

1	6. n : {0...\|\|v\|\|+1} 7. n0 \|\|v\|\|+1 = \|\|v\|\|+1-n	Auto
2	6. n : {0...\|\|v\|\|+1} 7. 0<n \|\|nth_tl(n-1;v)\|\| = \|\|v\|\|+1-n	1 step