Nuprl - Pf append_segment 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||}

k0+i (firstn(0;nth_tl(i;as)) @ firstn(k-(0+i);nth_tl(0+i;as))) = firstn(k-i;nth_tl(i;as))

By: ArithSimp 0

Generated subgoal:

1 ki (firstn(0;nth_tl(i;as)) @ firstn(-i+k;nth_tl(i;as))) = firstn(-i+k;nth_tl(i;as))

About: