At: nth tl lem1 1 2 1 2 1 1
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
8. tl(nth_tl(y;as)) = nth_tl(y+1;as)
9. nth_tl(x-1;nth_tl(y+1;as)) = nth_tl(x-1+y+1;as)
nth_tl(x-1;nth_tl(y+1;as)) = nth_tl(x+y;as)
By:
ArithSimp 0
THEN
ArithSimp -1
Generated subgoals:None
About:
