rename insert_delete → insert_delete_insert; add new insert_delete matching delete_insert

As discussed this is currently inconsistent.

I propose we use insert_delete for the lemma with a precondition since it is used 7 times in std++ after this MR; the one without a precondition is used just 3 times (one of which is to prove insert_delete).