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