diff --git a/CHANGELOG.md b/CHANGELOG.md
index f7b0037eaf69f3143dbd7053bfc50cc711bf6db3..c4dfd5f2ca7ae4a5b6296d3b392aeb1d2c936797 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -99,6 +99,7 @@ Changes in Coq:
 * A new tactic, `wp_pures`, executes as many pure steps as possible, excluding
   steps that would require unlocking subterms. Every impure wp_ tactic executes
   this tactic before doing anything else.
+* Add `big_sepM_insert_acc`.
 
 ## Iris 3.1.0 (released 2017-12-19)
 
diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index 8149b201fcb6daef0dd355f0bb5cf25fed5ff3ec..9ff0864e0ad894f24ace77d76c3aa99a2c47377b 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -628,6 +628,17 @@ Section gmap.
     rewrite -insert_delete big_sepM_insert ?lookup_delete //.
   Qed.
 
+  Lemma big_sepM_insert_acc Φ m i x :
+    m !! i = Some x →
+    ([∗ map] k↦y ∈ m, Φ k y) ⊢
+      Φ i x ∗ (∀ x', Φ i x' -∗ ([∗ map] k↦y ∈ <[i:=x']> m, Φ k y)).
+  Proof.
+    intros ?. rewrite {1}big_sepM_delete //. apply sep_mono; [done|].
+    apply forall_intro=> x'.
+    rewrite -insert_delete big_sepM_insert ?lookup_delete //.
+    by apply wand_intro_l.
+  Qed.
+
   Lemma big_sepM_fn_insert {B} (Ψ : K → A → B → PROP) (f : K → B) m i x b :
     m !! i = None →
        ([∗ map] k↦y ∈ <[i:=x]> m, Ψ k y (<[i:=b]> f k))