PrintForm Definitions list 3 autom Sections AutomataTheory Doc

At: append segment 1 1
1. T: Type
2. as: T*
3. i: {0...||as||}
4. j: {i...||as||}
5. k: {j...||as||}

(firstn(j-i;nth_tl(i;as)) @ firstn(k-j;nth_tl(j;as))) = firstn(k-i;nth_tl(i;as))
By: Let (x = j-i)
Generated subgoal:

16. x:
7. x = j-i
(firstn(x;nth_tl(i;as)) @ firstn(k-j;nth_tl(j;as))) = firstn(k-i;nth_tl(i;as))

About:
equallistsubtractuniversenatural_number