Add insert delete lemma for big ops over gmap

These lemmas are similar to insert_delete but for big ops over gmaps.

They are convenient when one has deleted a conjunc with big_opM_delete and then later wants to add it back in.