diff --git a/algebra/upred_big_op.v b/algebra/upred_big_op.v
index c7bc183b68e40363d538c90bd7959c27aa9c3eb5..d25e6fd85b92c5e9c19794c748311017c8f12c65 100644
--- a/algebra/upred_big_op.v
+++ b/algebra/upred_big_op.v
@@ -180,9 +180,9 @@ Section gmap.
     f_equiv; apply reflexive_eq, list_fmap_ext. by intros []. done.
   Qed.
 
-  Lemma big_sepM_insert_override (Φ : K → uPred M) m i x :
+  Lemma big_sepM_insert_override (Φ : K → uPred M) m i x y :
     m !! i = Some x →
-    ([★ map] k↦_ ∈ <[i:=x]> m, Φ k) ⊣⊢ ([★ map] k↦_ ∈ m, Φ k).
+    ([★ map] k↦_ ∈ <[i:=y]> m, Φ k) ⊣⊢ ([★ map] k↦_ ∈ m, Φ k).
   Proof.
     intros. rewrite -insert_delete big_sepM_insert ?lookup_delete //.
     by rewrite -big_sepM_delete.
diff --git a/program_logic/boxes.v b/program_logic/boxes.v
index 6e3f3f46159bf99a1557ea200260e7ccb4df8c7d..625ac17dec93f26bbf10f71dd4cebfbaf6b02d60 100644
--- a/program_logic/boxes.v
+++ b/program_logic/boxes.v
@@ -144,7 +144,7 @@ Proof.
     as "[Hγ Hγ']"; first by iFrame "Hγ".
   iPvsIntro; iNext; iSplitL "Hγ HQ"; first (iExists true; by iFrame "Hγ HQ").
   iExists Φ; iSplit.
-  - by rewrite -insert_delete big_sepM_insert ?lookup_delete // big_sepM_delete.
+  - by rewrite big_sepM_insert_override.
   - rewrite -insert_delete big_sepM_insert ?lookup_delete //.
     iFrame "Hγ'". by repeat iSplit.
 Qed.
@@ -165,7 +165,7 @@ Proof.
     as "[Hγ Hγ']"; first by iFrame "Hγ".
   iPvsIntro; iNext; iSplitL "Hγ"; first (iExists false; by repeat iSplit).
   iExists Φ; iSplit.
-  - by rewrite -insert_delete big_sepM_insert ?lookup_delete // big_sepM_delete.
+  - by rewrite big_sepM_insert_override.
   - rewrite -insert_delete big_sepM_insert ?lookup_delete //.
     iFrame "Hγ'". by repeat iSplit.
 Qed.