At:
append firstn lastn sq L:Top List, n:{0...||L||}. (firstn(n;L) @ nth_tl(n;L)) ~ L
By:
Analyze 0
THEN
ListInd -1
THEN
RecUnfold `firstn` 0
THEN
RecUnfold `nth_tl` 0
THEN
Reduce 0
THEN
Analyze 0
THEN
Repeat SplitOnConclITE
THEN
Reduce 0
THEN
Try (Complete Auto)
THEN
Analyze
THEN
EasyHyp
Generated subgoals:
L:Top List, n:{0...||L||}. (firstn(n;L) @ nth_tl(n;L)) ~ L