diff --git a/CHANGELOG.md b/CHANGELOG.md
index 7a82ef0c7dae75bba7cc22d4c459117745ec4849..fc8d8565ac9df9ecc081ec3f8fc318776c0443fa 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -53,6 +53,8 @@ Coq 8.13, 8.14, and 8.15 are no longer supported.
 * Add monotone resource algebra, `algebra/mra.v`, to enable reasoning about
   monotonicity with respect to an arbitrary preorder relation: the extension order
   of `mra R` is designed to embed the preorder relation `R`. (by Amin Timany)
+* Rename instances `union_with_proper` → `union_with_ne`,
+  `map_fmap_proper` → `map_fmap_ne`, `map_zip_with_proper` → `map_zip_with_ne`.
 
 **Changes in `bi`:**
 
diff --git a/iris/algebra/gmap.v b/iris/algebra/gmap.v
index fed922c7faf234ad418e3666d48b44d6d5e95f29..41542e659bf6924e78271d177114d9418fd1f98a 100644
--- a/iris/algebra/gmap.v
+++ b/iris/algebra/gmap.v
@@ -118,17 +118,17 @@ Proof.
   intros ?? Hf ?? Hm1 ?? Hm2 i. rewrite !lookup_merge.
   destruct (Hm1 i), (Hm2 i); try apply Hf; by constructor.
 Qed.
-Global Instance union_with_proper `{Countable K} {A : ofe} n :
+Global Instance union_with_ne `{Countable K} {A : ofe} n :
   Proper ((dist n ==> dist n ==> dist n) ==>
           dist n ==> dist n ==> dist n) (union_with (M:=gmap K A)).
 Proof.
   intros ?? Hf ?? Hm1 ?? Hm2 i; apply (merge_ne _ _); auto.
   by do 2 destruct 1; first [apply Hf | constructor].
 Qed.
-Global Instance map_fmap_proper `{Countable K} {A B : ofe} (f : A → B) n :
+Global Instance map_fmap_ne `{Countable K} {A B : ofe} (f : A → B) n :
   Proper (dist n ==> dist n) f → Proper (dist n ==> dist n) (fmap (M:=gmap K) f).
 Proof. intros ? m m' ? k; rewrite !lookup_fmap. by repeat f_equiv. Qed.
-Global Instance map_zip_with_proper `{Countable K} {A B C : ofe} (f : A → B → C) n :
+Global Instance map_zip_with_ne `{Countable K} {A B C : ofe} (f : A → B → C) n :
   Proper (dist n ==> dist n ==> dist n) f →
   Proper (dist n ==> dist n ==> dist n) (map_zip_with (M:=gmap K) f).
 Proof.