as:T*. (as[0..||as||
]) = as whole_segment
] == firstn(n-m;nth_tl(m;as))
Thm* as:T*. (as[0..||as||]) = as whole_segment
Thm* as:T*, i:{0...||as||}, j:{i...||as||}, k:{j...||as||}.
((as[i..j]) @ (as[j..k])) = (as[i..k])
append_segment
In prior sections: list 1