diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 8861aea53b8afb2f32d93a92025f2067ebfc337b..9d4ce12c76ce5afe25643954df8762ae34923b1b 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -677,6 +677,14 @@ Proof.
   - by rewrite lookup_omap, !lookup_insert.
   - by rewrite lookup_omap, !lookup_insert_ne, lookup_omap by done.
 Qed.
+Lemma omap_insert_None {A B} (f : A → option B) m i x :
+  f x = None → omap f (<[i:=x]>m) = delete i (omap f m).
+Proof.
+  intros; apply map_eq; intros i'; destruct (decide (i' = i)) as [->|].
+  - by rewrite lookup_omap, lookup_insert, lookup_delete.
+  - by rewrite lookup_omap, lookup_insert_ne,
+     lookup_delete_ne, lookup_omap by done.
+Qed.
 Lemma map_fmap_singleton {A B} (f : A → B) i x : f <$> {[i := x]} = {[i := f x]}.
 Proof.
   by unfold singletonM, map_singleton; rewrite fmap_insert, map_fmap_empty.