PrintForm Definitions list 3 autom Sections AutomataTheory Doc

At: firstn lem1 1 2 2 1 1 1 1 2 2 2 1 1
1. T: Type
2. x:
3. 0 < x
4. as:T*. -1+x < ||as|| firstn(x;as) = (firstn(-1+x;as) @ [as[(-1+x)]])
5. as: T*
6. u: T
7. v: T*
8. x < ||v||+1
9. 0 < x+1
10. 0 < x
11. firstn(x;v) = (firstn(-1+x;v) @ [v[(-1+x)]])

[hd(nth_tl(-1+x;v))] = [hd(nth_tl(x;u.v))]
By: RWH (AddrC [3] (RecUnfoldC `nth_tl`)) 0
Generated subgoal:

1 [hd(nth_tl(-1+x;v))] = [hd(if x0 u.v else nth_tl(x-1;tl((u.v))) fi)]

About:
equallistconsaddminusnatural_numbernil
universeintless_thanallimpliesifthenelsesubtract