Strengthen big_sepM_insert_override and use it.

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.

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.