diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index bab9041d3a38c13357199cdf1f6a4cc958ce0d9b..ec1f3abfcdbd4e1ffd885a725ac59535f0581581 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -2390,6 +2390,16 @@ Qed.
 Global Instance map_difference_right_id {A} : RightId (=) (∅:M A) (∖) := _.
 Lemma map_difference_empty {A} (m : M A) : m ∖ ∅ = m.
 Proof. by rewrite (right_id _ _). Qed.
+Lemma map_difference_delete_insert {A} (m m0 : M A) k v :
+  delete k (m ∖ m0) = m ∖ <[k:=v]> m0.
+Proof.
+  apply map_eq. intros i. apply option_eq. intros x.
+  rewrite lookup_delete_Some. rewrite !lookup_difference_Some. split.
+  - intros (Hne & Hm & Hm0). rewrite lookup_insert_ne by done. done.
+  - destruct (decide (k = i)) as [->|Hne].
+    + rewrite lookup_insert. naive_solver.
+    + rewrite lookup_insert_ne by done. done.
+Qed.
 End theorems.
 
 (** ** The seq operation *)