diff --git a/tests/fin_maps.ref b/tests/fin_maps.ref
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/fin_maps.v b/tests/fin_maps.v
new file mode 100644
index 0000000000000000000000000000000000000000..842c20a80d908673e12a5e5e11a4460ce2f77db6
--- /dev/null
+++ b/tests/fin_maps.v
@@ -0,0 +1,13 @@
+From stdpp Require Import fin_maps.
+
+Section map_disjoint.
+  Context `{FinMap K M}.
+
+  Lemma solve_map_disjoint_singleton_1 {A} (m1 m2 : M A) i x :
+    m1 ##ₘ <[i:=x]> m2 → {[ i:= x ]} ∪ m2 ##ₘ m1 ∧ m2 ##ₘ ∅.
+  Proof. intros. solve_map_disjoint. Qed.
+
+  Lemma solve_map_disjoint_singleton_2 {A} (m1 m2 : M A) i x :
+    m2 !! i = None → m1 ##ₘ {[ i := x ]} ∪ m2 → m2 ##ₘ <[i:=x]> m1 ∧ m1 !! i = None.
+  Proof. intros. solve_map_disjoint. Qed.
+End map_disjoint.
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index bcce9efdf60f708d6e280c38d4f259ecd2c7c46a..d4cdfd3ebd8a60c539bf3d2c97ec16a7f6456ef8 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1932,6 +1932,8 @@ Hint Extern 2 (_ ##ₘ {[ _ := _ ]}) =>
   apply map_disjoint_singleton_r_2 : map_disjoint.
 Hint Extern 2 (_ ∪ _ ##ₘ _) => apply map_disjoint_union_l_2 : map_disjoint.
 Hint Extern 2 (_ ##ₘ _ ∪ _) => apply map_disjoint_union_r_2 : map_disjoint.
+Hint Extern 2 ({[_:= _]} ##ₘ _) => apply map_disjoint_singleton_l : map_disjoint.
+Hint Extern 2 (_ ##ₘ {[_:= _]}) => apply map_disjoint_singleton_r : map_disjoint.
 Hint Extern 2 (<[_:=_]>_ ##ₘ _) => apply map_disjoint_insert_l_2 : map_disjoint.
 Hint Extern 2 (_ ##ₘ <[_:=_]>_) => apply map_disjoint_insert_r_2 : map_disjoint.
 Hint Extern 2 (delete _ _ ##ₘ _) => apply map_disjoint_delete_l : map_disjoint.