diff --git a/CHANGELOG.md b/CHANGELOG.md
index 12133236b2f86e6adf82c06756345fde91ef1554..68701b609a437bd2f937781ffa9df527b641cd2b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -5,6 +5,8 @@ API-breaking change is listed.
 
 - Generalize `foldr_comm_acc`, `map_fold_comm_acc`, `set_fold_comm_acc`, and
   `gmultiset_set_fold_comm_acc` to have more general type. (by Yannick Zakowski)
+- Strengthen `map_disjoint_difference_l` and `map_disjoint_difference_l`, and
+  thereby make them consistent with the corresponding lemmas for sets.
 
 ## std++ 1.10.0 (2024-04-12)
 
diff --git a/stdpp/fin_maps.v b/stdpp/fin_maps.v
index 87f1f2c5b5f4654fcf7bfc75b126c15a6f1ba847..cd7705e826e21206711d1a87e4b8c064dd86e120 100644
--- a/stdpp/fin_maps.v
+++ b/stdpp/fin_maps.v
@@ -3041,14 +3041,16 @@ Proof.
   rewrite lookup_difference.
   destruct (m1 !! i), (m2 !! i); compute; naive_solver.
 Qed.
-Lemma map_disjoint_difference_l {A} (m1 m2 : M A) : m1 ⊆ m2 → m2 ∖ m1 ##ₘ m1.
+
+Lemma map_disjoint_difference_l {A} (m1 m2 m3 : M A) : m3 ⊆ m2 → m1 ∖ m2 ##ₘ m3.
 Proof.
   intros Hm i; specialize (Hm i).
   unfold difference, map_difference; rewrite lookup_difference_with.
-  by destruct (m1 !! i), (m2 !! i).
+  by destruct (m1 !! i), (m2 !! i), (m3 !! i).
 Qed.
-Lemma map_disjoint_difference_r {A} (m1 m2 : M A) : m1 ⊆ m2 → m1 ##ₘ m2 ∖ m1.
+Lemma map_disjoint_difference_r {A} (m1 m2 m3 : M A) : m3 ⊆ m2 → m3 ##ₘ m1 ∖ m2.
 Proof. intros. symmetry. by apply map_disjoint_difference_l. Qed.
+
 Lemma map_subseteq_difference_l {A} (m1 m2 m : M A) : m1 ⊆ m → m1 ∖ m2 ⊆ m.
 Proof.
   rewrite !map_subseteq_spec. setoid_rewrite lookup_difference_Some. naive_solver.