as:T*. tl(nth_tl(0;as)) = nth_tl(0+1;as)2. y:
3. 0 < y
4.
as:T*. tl(nth_tl(y-1;as)) = nth_tl(y-1+1;as) as:T*. tl(nth_tl(y;as)) = nth_tl(y+1;as) T:Type, y:
, as:T*. tl(nth_tl(y;as)) = nth_tl(y+1;as)| 1 | 1. T: Type as:T*. tl(nth_tl(0;as)) = nth_tl(0+1;as) |
| 2 | 1. T: Type 2. y: 3. 0 < y 4. as:T*. tl(nth_tl(y-1;as)) = nth_tl(y-1+1;as) as:T*. tl(nth_tl(y;as)) = nth_tl(y+1;as) |
About:
 |  |  |  |  |  |