Follow same scheme for other map lemmas.

stdpp/binders.v

@@ -108,5 +108,5 @@ Section binder_delete_insert.
   Proof. intros. destruct b; simpl; by rewrite ?delete_insert_ne by congruence. Qed.
   Lemma binder_delete_delete {A} b s (m : M A) :
     binder_delete b (delete s m) = delete s (binder_delete b m).
-  Proof. destruct b; simpl; by rewrite 1?delete_commute. Qed.
+  Proof. destruct b; simpl; by rewrite 1?delete_delete. Qed.
 End binder_delete_insert.

stdpp/fin_map_dom.v

@@ -122,10 +122,10 @@ Proof.
 Qed.
 Lemma delete_partial_alter_dom {A} (m : M A) i f :
   i ∉ dom m → delete i (partial_alter f i m) = m.
-Proof. rewrite not_elem_of_dom. apply delete_partial_alter. Qed.
+Proof. rewrite not_elem_of_dom. apply delete_partial_alter_id. Qed.
 Lemma delete_insert_dom {A} (m : M A) i x :
   i ∉ dom m → delete i (<[i:=x]>m) = m.
-Proof. rewrite not_elem_of_dom. apply delete_insert. Qed.
+Proof. rewrite not_elem_of_dom. apply delete_insert_id. Qed.
 Lemma map_disjoint_dom {A} (m1 m2 : M A) : m1 ##ₘ m2 ↔ dom m1 ## dom m2.
 Proof.
   rewrite map_disjoint_spec, elem_of_disjoint.
@@ -203,7 +203,7 @@ Proof.
   rewrite dom_insert in Hdom.
   assert (i ∉ dom m2) by (by apply not_elem_of_dom).
   assert (i ∈ dom m1) as [x' Hx']%elem_of_dom by set_solver.
-  rewrite <-(insert_delete m1 i x') by done.
+  rewrite <-(insert_delete_id m1 i x') by done.
   rewrite !map_size_insert_None, <-Nat.succ_le_mono
     by (by rewrite ?lookup_delete_eq).
   apply IH. rewrite dom_delete. set_solver.
@@ -217,7 +217,7 @@ Proof.
   rewrite dom_insert in Hdom.
   assert (i ∉ dom m2) by (by apply not_elem_of_dom).
   assert (i ∈ dom m1) as [x' Hx']%elem_of_dom by set_solver.
-  rewrite <-(insert_delete m1 i x') by done.
+  rewrite <-(insert_delete_id m1 i x') by done.
   rewrite !map_size_insert_None, <-Nat.succ_lt_mono
     by (by rewrite ?lookup_delete_eq).
   apply IH. rewrite dom_delete. split; [set_solver|].

stdpp/gmultiset.v

@@ -515,7 +515,7 @@ Section more_lemmas.
     revert Y; induction X as [|x n X HX IH] using map_ind; intros Y.
     { by rewrite (left_id_L _ _ Y), map_to_list_empty. }
     destruct (Y !! x) as [n'|] eqn:HY.
-    - rewrite <-(insert_delete Y x n') by done.
+    - rewrite <-(insert_delete_id Y x n') by done.
       erewrite <-insert_union_with by done.
       rewrite !map_to_list_insert, !bind_cons
         by (by rewrite ?lookup_union_with, ?lookup_delete_eq, ?HX).