PrintForm Definitions list 3 autom Sections AutomataTheory Doc

At: nth tl lem1 1 2 1 2 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)

nth_tl(x-1;tl(nth_tl(y;as))) = nth_tl(x+y;as)
By:
RWH (HypC -1) 0
THEN
InstHyp [y+1;as] 4
Generated subgoal:

19. 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)

About:
equallistsubtractnatural_numberadd
universeintless_thanall