Nuprl - Pf nth_tl_lem1 1 2 1 2

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*
7. 0 < x

nth_tl(x-1;tl(nth_tl(y;as))) = nth_tl(x+y;as)

By: Inst Thm* y:, as:T*. tl(nth_tl(y;as)) = nth_tl(y+1;as) [T;y;as]

Generated subgoal:

1 8. tl(nth_tl(y;as)) = nth_tl(y+1;as)
nth_tl(x-1;tl(nth_tl(y;as))) = nth_tl(x+y;as)

About: