finish the correctness part of the proof for copy_insert.

Do this by changing the correctness condition for copy_insert
to be in terms of SequenceR instead of IndexR.

It would be good to prove the two conditions are the same at some
point but it is too annoying to do now