x,y:
, as:T*. nth_tl(x;nth_tl(y;as)) = nth_tl(x+y;as) nth_tl_lem1
0
as else nth_tl(n-1;tl(as)) fi (recursive)
Thm* x,y:, as:T*. nth_tl(x;nth_tl(y;as)) = nth_tl(x+y;as) nth_tl_lem1
Thm* y:, as:T*. tl(nth_tl(y;as)) = nth_tl(y+1;as) nth_tl_lem0
In prior sections: list 1