one step towards restoring the old correctness condition

Unfortunately, because of the way program sets up things with
the inductive hypothesis, this isn't enough to just go back
to the old correctness condition, sadly
candidate definition of copy_insert_time