diff --git a/stdpp/fin_maps.v b/stdpp/fin_maps.v
index 596b3dbf4ef9e514b8eae42de65c7198a80ee029..3eb4f8e0990b807deabc6fc5d4dca6aea71f46e4 100644
--- a/stdpp/fin_maps.v
+++ b/stdpp/fin_maps.v
@@ -528,6 +528,9 @@ Lemma lookup_insert_rev {A}  (m : M A) i x y : <[i:=x]>m !! i = Some y → x = y
 Proof. rewrite lookup_insert. congruence. Qed.
 Lemma lookup_insert_ne {A} (m : M A) i j x : i ≠ j → <[i:=x]>m !! j = m !! j.
 Proof. unfold insert. apply lookup_partial_alter_ne. Qed.
+Lemma lookup_insert_eq {A} (m : M A) i j x :
+  <[i:=x]>m !! j = if decide (i = j) then Some x else m !! j.
+Proof. case_decide; simplify_eq; eauto using lookup_insert, lookup_insert_ne. Qed.
 Lemma lookup_total_insert_ne `{!Inhabited A} (m : M A) i j x :
   i ≠ j → <[i:=x]>m !!! j = m !!! j.
 Proof. intros. by rewrite lookup_total_alt, lookup_insert_ne. Qed.