diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index 234e65f164d8496b0a3b2d1bd3ab2cc46edb044b..f37790563368a3b4db2e47358628d38b7164d9fb 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -26,7 +26,7 @@ Proof.
   { eapply singleton_local_update. by rewrite lookup_fmap EQB.
     by apply (exclusive_local_update _ (Excl (Bor_open q Vtok V'))). }
   iExists V'. rewrite -fmap_insert. iFrame "∗%". iExists _. iFrame.
-  rewrite -insert_delete big_sepM_insert ?lookup_delete // big_sepM_delete //=.
+  rewrite -insert_delete_insert big_sepM_insert ?lookup_delete // big_sepM_delete //=.
   iIntros "/= !>". iNext. iDestruct "HB" as "[?$]". iFrame.
 Qed.
 
@@ -50,7 +50,7 @@ Proof.
   rewrite big_sepM_delete //. simpl. setoid_rewrite HVV'.
   iDestruct "HB" as "[>[% $] HB]". iSplitR "Hbor"; last by iExists (Vtok' ⊔ V); auto.
   iExists _. iFrame "Hbox Hown".
-  rewrite -insert_delete big_sepM_insert ?lookup_delete //=. iFrame.
+  rewrite -insert_delete_insert big_sepM_insert ?lookup_delete //=. iFrame.
   iPureIntro. by f_equiv.
 Qed.
 
diff --git a/theories/lifetime/model/boxes.v b/theories/lifetime/model/boxes.v
index 548df8b33670c46b07e6c4919d9032247a90234a..b3fdd23d65037b85e6d2318bc82e23cf8926301a 100644
--- a/theories/lifetime/model/boxes.v
+++ b/theories/lifetime/model/boxes.v
@@ -164,7 +164,7 @@ Proof.
   iMod ("Hclose" with "[Hγ HQ]") as "_"; [iNext; iExists (Some $ to_latT V); by iFrame|].
   iModIntro; iNext; iExists Φ; iSplit.
   - by rewrite big_sepM_insert_override.
-  - rewrite -insert_delete big_sepM_insert ?lookup_delete //. auto with iFrame.
+  - rewrite -insert_delete_insert big_sepM_insert ?lookup_delete //. auto with iFrame.
 Qed.
 
 Lemma slice_empty E q f P Q γ V :
@@ -181,7 +181,7 @@ Proof.
   iMod ("Hclose" with "[Hγ]") as "_"; [iNext; iExists None; by repeat iSplit|].
   iModIntro; iNext; iExists Φ; iSplit.
   - by rewrite big_sepM_insert_override.
-  - rewrite -insert_delete big_sepM_insert ?lookup_delete //. auto with iFrame.
+  - rewrite -insert_delete_insert big_sepM_insert ?lookup_delete //. auto with iFrame.
 Qed.
 
 Lemma slice_insert_full E q f P Q V :
@@ -205,7 +205,7 @@ Proof.
   iMod (slice_empty with "Hslice Hbox") as "[$ Hbox]"; try done.
   iDestruct (slice_delete_empty with "Hslice Hbox") as (P') "[Heq Hbox]".
   { 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 V :
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index 9bda0563b2ff5bfdf657703c9029ea1b1da2fe8a..e3fdee53c8e0a3ccc63efc29afe87ca8aa3794fb 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -80,7 +80,7 @@ Proof.
     rewrite /to_borUR !fmap_insert. iFrame "Hbox HB●".
     rewrite big_sepM_delete //. simpl. iDestruct "HB" as "[% HB]".
     rewrite (big_sepM_delete _ (<[_:=_]>_) i); last by rewrite lookup_insert.
-    rewrite -insert_delete delete_insert ?lookup_delete //=. iFrame. auto. }
+    rewrite -insert_delete_insert delete_insert ?lookup_delete //=. iFrame. auto. }
   clear B HB Pb' Pi'.
   rewrite {1}/lft_bor_alive. iDestruct "Hκalive'" as (B) "[[Hbox >HB●] HB]".
   set (P' := ((monPred_in V ∨ ⎡P V0⎤) ∧ (monPred_in V0 → P))%I).
@@ -143,7 +143,7 @@ Proof.
     iIntros (_). rewrite lft_inv_alive_unfold.
     iExists Pb', Pi'. iFrame "Hvs' Hinh". rewrite /lft_bor_alive.
     iExists (<[i:=Bor_in VP]>B'). rewrite /to_borUR !fmap_insert. iFrame.
-    rewrite -insert_delete big_sepM_insert ?lookup_delete //=. iFrame. auto. }
+    rewrite -insert_delete_insert big_sepM_insert ?lookup_delete //=. iFrame. auto. }
   rewrite -[S n]Nat.add_1_l -nat_op auth_frag_op own_cnt_op. by iFrame.
 Qed.
 
@@ -194,7 +194,7 @@ Proof.
   { iIntros "!>!>!>". by iDestruct  "HP'V" as "#HP'V". }
   { rewrite /lft_bor_alive (big_sepM_delete _ B i') //. iDestruct "HB" as "[_ HB]".
     iExists (delete i' B). rewrite -fmap_delete. iFrame.
-    rewrite fmap_delete -insert_delete delete_insert ?lookup_delete //=. }
+    rewrite fmap_delete -insert_delete_insert delete_insert ?lookup_delete //=. }
   { iModIntro. iModIntro. iApply (lft_vs_cons with "[] Hvs").
     iIntros "%% [??] %% _ !>". iNext. iRewrite "HeqPb'". iFrame. }
   iDestruct "HH" as "([HI Hinvκ] & Hb & Halive & Hvs)".