diff --git a/coq-iris.opam b/coq-iris.opam
index ff290e260ef61556915ebf1e662feaee51a8581a..3655e80528533cbefb255eb5bf082de3200d4074 100644
--- a/coq-iris.opam
+++ b/coq-iris.opam
@@ -15,7 +15,7 @@ iris.prelude, iris.algebra, iris.si_logic, iris.bi, iris.proofmode, iris.base_lo
 
 depends: [
   "coq" { (>= "8.12" & < "8.15~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2021-06-24.1.f63bb74b") | (= "dev") }
+  "coq-stdpp" { (= "dev.2021-06-26.0.fe3b9967") | (= "dev") }
 ]
 
 build: ["./make-package" "iris" "-j%{jobs}%"]
diff --git a/iris/algebra/big_op.v b/iris/algebra/big_op.v
index 5bb45470789544c8150092f2b33f11965a016670..1d91fdb9e2eecc6f2c7c462848d34b39d2bef662 100644
--- a/iris/algebra/big_op.v
+++ b/iris/algebra/big_op.v
@@ -254,7 +254,7 @@ Lemma big_opM_delete `{Countable K} {B} (f : K → B → M) (m : gmap K B) i x :
   ([^o map] k↦y ∈ m, f k y) ≡ f i x `o` [^o map] k↦y ∈ delete i m, f k y.
 Proof.
   intros. rewrite -big_opM_insert ?lookup_delete //.
-  by rewrite insert_delete insert_id.
+  by rewrite insert_delete.
 Qed.
 
 Section gmap.
@@ -379,14 +379,14 @@ Section gmap.
   Lemma big_opM_insert_delete `{Countable K} {B} (f : K → B → M) (m : gmap K B) i x :
     ([^o map] k↦y ∈ <[i:=x]> m, f k y) ≡ f i x `o` [^o map] k↦y ∈ delete i m, f k y.
   Proof.
-    rewrite -insert_delete big_opM_insert; first done. by rewrite lookup_delete.
+    rewrite -insert_delete_insert big_opM_insert; first done. by rewrite lookup_delete.
   Qed.
 
   Lemma big_opM_insert_override (f : K → A → M) m i x x' :
     m !! i = Some x → f i x ≡ f i x' →
     ([^o map] k↦y ∈ <[i:=x']> m, f k y) ≡ ([^o map] k↦y ∈ m, f k y).
   Proof.
-    intros ? Hx. rewrite -insert_delete big_opM_insert ?lookup_delete //.
+    intros ? Hx. rewrite -insert_delete_insert big_opM_insert ?lookup_delete //.
     by rewrite -Hx -big_opM_delete.
   Qed.
 
diff --git a/iris/algebra/lib/gmap_view.v b/iris/algebra/lib/gmap_view.v
index c384a18cdc7f8f535eb45a1e3d10e0df343d1999..196690bedbadd3006a5e180c1106d0ed6a749568 100644
--- a/iris/algebra/lib/gmap_view.v
+++ b/iris/algebra/lib/gmap_view.v
@@ -370,7 +370,7 @@ Section lemmas.
   Proof.
     rewrite gmap_view_delete.
     rewrite (gmap_view_alloc _ k (DfracOwn 1) v') //; last by rewrite lookup_delete.
-    rewrite insert_delete //.
+    rewrite insert_delete_insert //.
   Qed.
 
   Lemma gmap_view_update_big m m0 m1 :
diff --git a/iris/base_logic/lib/boxes.v b/iris/base_logic/lib/boxes.v
index 68ac12c2427959895c039a6d577cad94c739aeb9..8a00bc3a20228014469ac11f0e0877eea11ff9f7 100644
--- a/iris/base_logic/lib/boxes.v
+++ b/iris/base_logic/lib/boxes.v
@@ -152,7 +152,7 @@ Proof.
   iModIntro. iSplitL "Hγ HQ"; first (iNext; iExists true; by iFrame).
   iModIntro; iNext; iExists Φ; iSplit.
   - by rewrite big_opM_insert_override.
-  - rewrite -insert_delete big_opM_insert ?lookup_delete //.
+  - rewrite -insert_delete_insert big_opM_insert ?lookup_delete //.
     iFrame; eauto.
 Qed.
 
@@ -171,7 +171,7 @@ Proof.
   iModIntro. iSplitL "Hγ"; first (iNext; iExists false; by repeat iSplit).
   iModIntro; iNext; iExists Φ; iSplit.
   - by rewrite big_opM_insert_override.
-  - rewrite -insert_delete big_opM_insert ?lookup_delete //.
+  - rewrite -insert_delete_insert big_opM_insert ?lookup_delete //.
     iFrame; eauto.
 Qed.
 
@@ -197,7 +197,7 @@ Proof.
   iMod (slice_empty with "Hslice Hbox") as "[$ Hbox]"; try done.
   iMod (slice_delete_empty with "Hslice Hbox") as (P') "[Heq Hbox]"; first done.
   { by apply lookup_insert. }
-  iExists P'. iFrame. rewrite -insert_delete delete_insert ?lookup_delete //.
+  iExists P'. iFrame. rewrite -insert_delete_insert delete_insert ?lookup_delete //.
 Qed.
 
 Lemma box_fill E f P :
diff --git a/iris/base_logic/lib/gen_inv_heap.v b/iris/base_logic/lib/gen_inv_heap.v
index 2e196fbd9c11858c6bd9293707a727639477148b..359b0009e9312544db1a2ae3bf996fdc6868bf6e 100644
--- a/iris/base_logic/lib/gen_inv_heap.v
+++ b/iris/base_logic/lib/gen_inv_heap.v
@@ -247,7 +247,7 @@ Section inv_heap.
       apply: exclusive_local_update. done. }
     iDestruct (big_sepM_insert _ _ _ (w, I') with "[$HsepM $Hl //]") as "HsepM".
     { apply lookup_delete. }
-    rewrite insert_delete -to_inv_heap_insert. iIntros "!> {$Hâ—¯}".
+    rewrite insert_delete_insert -to_inv_heap_insert. iIntros "!> {$Hâ—¯}".
     iApply ("Hclose" with "[H● HsepM]"). iExists _; by iFrame.
   Qed.
 
diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index 577809374f0ea7e0063a332e83afe45c3a958092..60a087b43df6629ed76ebbe53adc9514ee1dae57 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -1191,7 +1191,7 @@ Section map.
     { destruct Ha; try apply _. }
     rewrite big_sepM_delete // assoc.
     rewrite (sep_elim_l (Φ i x)) -big_sepM_insert ?lookup_delete //.
-    by rewrite insert_delete.
+    by rewrite insert_delete_insert.
   Qed.
 
   Lemma big_sepM_lookup_acc Φ m i x :
@@ -1231,7 +1231,7 @@ Section map.
       (Φ i x' -∗ Φ i x) -∗ ([∗ map] k↦y ∈ m, Φ k y).
   Proof.
     intros ?. apply wand_intro_l.
-    rewrite -insert_delete big_sepM_insert ?lookup_delete //.
+    rewrite -insert_delete_insert big_sepM_insert ?lookup_delete //.
     by rewrite assoc wand_elim_l -big_sepM_delete.
   Qed.
 
@@ -1242,7 +1242,7 @@ Section map.
   Proof.
     intros ?. apply wand_intro_l.
     rewrite {1}big_sepM_delete //; rewrite assoc wand_elim_l.
-    rewrite -insert_delete big_sepM_insert ?lookup_delete //.
+    rewrite -insert_delete_insert big_sepM_insert ?lookup_delete //.
   Qed.
 
   Lemma big_sepM_insert_acc Φ m i x :
@@ -1252,7 +1252,7 @@ Section map.
   Proof.
     intros ?. rewrite {1}big_sepM_delete //. apply sep_mono; [done|].
     apply forall_intro=> x'.
-    rewrite -insert_delete big_sepM_insert ?lookup_delete //.
+    rewrite -insert_delete_insert big_sepM_insert ?lookup_delete //.
     by apply wand_intro_l.
   Qed.
 
@@ -1655,7 +1655,7 @@ Section map2.
     ([∗ map] k↦y1;y2 ∈ <[i:=x1]>m1; <[i:=x2]>m2, Φ k y1 y2)
     ⊣⊢ Φ i x1 x2 ∗ [∗ map] k↦y1;y2 ∈ delete i m1;delete i m2, Φ k y1 y2.
   Proof.
-    rewrite -(insert_delete m1) -(insert_delete m2).
+    rewrite -(insert_delete_insert m1) -(insert_delete_insert m2).
     apply big_sepM2_insert; by rewrite lookup_delete.
   Qed.
 
@@ -1667,7 +1667,7 @@ Section map2.
   Proof.
     intros ??. rewrite {1}big_sepM2_delete //. apply sep_mono; [done|].
     apply forall_intro=> x1'. apply forall_intro=> x2'.
-    rewrite -(insert_delete m1) -(insert_delete m2) big_sepM2_insert ?lookup_delete //.
+    rewrite -(insert_delete_insert m1) -(insert_delete_insert m2) big_sepM2_insert ?lookup_delete //.
     by apply wand_intro_l.
   Qed.
 
@@ -1952,7 +1952,7 @@ Section map2.
     { by rewrite -Hm' lookup_delete. }
     apply wand_intro_l.
     rewrite -(exist_intro (<[i:=y]> m1')) -(exist_intro m2'). apply and_intro.
-    { apply pure_intro. by rewrite -insert_union_l -Hm' insert_delete insert_id. }
+    { apply pure_intro. by rewrite -insert_union_l -Hm' insert_delete. }
     apply and_intro.
     { apply pure_intro. by apply map_disjoint_insert_l. }
     by rewrite big_sepM2_insert // -assoc.