At: append segment 1 1 1 1 1 1 1 1 1 1 1
1. T: Type
2. as: T*
3. i: {0...||as||}
4. j: {i...||as||}
5. k: {j...||as||}
6. w: T*
7. w = nth_tl(i;as)
(Case of w; nil 
nil ; a.as' nil) = nil 
T*
By:
Thin -1
THEN
Analyze -1
THEN
Reduce 0
Generated subgoals:None
About:
