Nuprl - Pf nth_tl

1. T: Type
2. x:
3. 0 < x
4. y:, as:T*. nth_tl(x-1;nth_tl(y;as)) = nth_tl(x-1+y;as)
5. y:
6. as: T*

nth_tl(x;nth_tl(y;as)) = nth_tl(x+y;as)

By: RecCaseSplit `nth_tl`

Generated subgoals:

1 7. x0
nth_tl(y;as) = nth_tl(x+y;as)

2 7. 0 < x
nth_tl(x-1;tl(nth_tl(y;as))) = nth_tl(x+y;as)

About:

1	7. `x0` `nth_tl(y;as) = nth_tl(x+y;as)`
2	7. `0 < x` `nth_tl(x-1;tl(nth_tl(y;as))) = nth_tl(x+y;as)`