x < ||nil|| 
firstn(x+1;nil) = (firstn(x;nil) @ [nil[x]]) 
T*7. v: T*
8. x < ||v||
firstn(x+1;v) = (firstn(x;v) @ [v[x]]) x < ||u.v|| firstn(x+1;u.v) = (firstn(x;u.v) @ [(u.v)[x]])
as:T*. x-1 < ||as|| firstn(x-1+1;as) = (firstn(x-1;as) @ [as[(x-1)]]) firstn(x+1;as) = (firstn(x;as) @ [as[x]])| 1 | x < ||nil|| firstn(x+1;nil) = (firstn(x;nil) @ [nil[x]]) T* |
| 2 | 6. u: T 7. v: T* 8. x < ||v|| firstn(x+1;v) = (firstn(x;v) @ [v[x]]) x < ||u.v|| firstn(x+1;u.v) = (firstn(x;u.v) @ [(u.v)[x]]) |
About:
 |  |  |  |  |  |
 |  |  |  |  |  |