diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3346a6e3eb33cfb60c376b61bfa006e4da26f449..b1d7e70ad2afdcce4371567f2912b3888d3e4550 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -57,6 +57,8 @@ Noteworthy additions and changes:
     `seqZ_lookup_ge` → `lookup_seqZ_ge`, and `seqZ_lookup` → `lookup_seqZ`
   + Rename `lookup_seq_inv` → `lookup_seq` and generalize it to a bi-implication
   + Add `NoDup_seqZ` and `Forall_seqZ`
+- Rename `fin_maps.singleton_proper` into `singletonM_proper` since it concerns
+  `singletonM` and to avoid overlap with `sets.singleton_proper`.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index eaab32feb7025cae2b46a9310334c89233bdf04f..966c44e9cc4b51188ea3637b52597210c1f822c5 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -184,7 +184,7 @@ Section setoid.
   Global Instance insert_proper (i : K) :
     Proper ((≡) ==> (≡) ==> (≡@{M A})) (insert i).
   Proof. by intros ???; apply partial_alter_proper; [constructor|]. Qed.
-  Global Instance singleton_proper k : Proper ((≡) ==> (≡@{M A})) (singletonM k).
+  Global Instance singletonM_proper k : Proper ((≡) ==> (≡@{M A})) (singletonM k).
   Proof.
     intros ???; apply insert_proper; [done|].
     intros ?. rewrite lookup_empty; constructor.