At: append segment 1 1 1 1 1 1 2 1 1 1 1 1 1 1 1 1 1 1 1 1 2 1
1. T: Type
2. as: T*
3. i: {0...||as||}
4. j: {i...||as||}
5. k: {j...||as||}
6. x: 
7. 0 < x
8. k
x+i
9. tl(nth_tl(-1+i+x;as)) = nth_tl(i+x;as)
10. aas: T*
nil = nil 
T* 
hd(nil).firstn(-i+k+-x;tl(nil)) = firstn(1+-i+k+-x;nil) T*
By:
Analyze 0
THEN
Analyze -1
Generated subgoals:None
About:
