diff --git a/CHANGELOG.md b/CHANGELOG.md
index cf2bd38cf7792d06198518705aecc781a4f5b295..c5d05fd0ac61de3efd80c2a3feb3d4740b83e650 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -38,6 +38,8 @@ Coq 8.8 and 8.9 are no longer supported.
     for Coq's number types `nat`, `N`, and `Z`.
 - Fix a bug where `pretty 0` was defined as `""`, the empty string. It now
   returns `"0"` for `N`, `Z`, and `nat`.
+- Remove duplicate `map_fmap_empty` of `fmap_empty`, and rename
+  `map_fmap_empty_inv` into `fmap_empty_inv` for consistency's sake.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
@@ -52,6 +54,8 @@ s/\bQp_not_plus_ge\b/Qp_not_add_le_l/g
 s/\bQp_le_plus_l\b/Qp_le_add_l/g
 s/\bQp_mult_plus_distr_l\b/Qp_mul_add_distr_r/g
 s/\bQp_mult_plus_distr_r\b/Qp_mul_add_distr_l/g
+s/\bmap_fmap_empty\b/fmap_empty/g
+s/\bmap_fmap_empty_inv\b/fmap_empty_inv/g
 ' $(find theories -name "*.v")
 ```
 
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 10bd2a24593681b2005706f8ad3656c6b81585f7..2b37071339478ef3f662aee63101dbfd02d6ca26 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -296,13 +296,6 @@ Lemma map_subset_empty {A} (m : M A) : m ⊄ ∅.
 Proof.
   intros [_ []]. rewrite map_subseteq_spec. intros ??. by rewrite lookup_empty.
 Qed.
-Lemma map_fmap_empty {A B} (f : A → B) : f <$> (∅ : M A) = ∅.
-Proof. by apply map_eq; intros i; rewrite lookup_fmap, !lookup_empty. Qed.
-Lemma map_fmap_empty_inv {A B} (f : A → B) m : f <$> m = ∅ → m = ∅.
-Proof.
-  intros Hm. apply map_eq; intros i. generalize (f_equal (lookup i) Hm).
-  by rewrite lookup_fmap, !lookup_empty, fmap_None.
-Qed.
 
 Lemma map_subset_alt {A} (m1 m2 : M A) :
   m1 ⊂ m2 ↔ m1 ⊆ m2 ∧ ∃ i, m1 !! i = None ∧ is_Some (m2 !! i).
@@ -663,6 +656,13 @@ Lemma fmap_empty {A B} (f : A → B) : f <$> ∅ = ∅.
 Proof. apply map_empty; intros i. by rewrite lookup_fmap, lookup_empty. Qed.
 Lemma omap_empty {A B} (f : A → option B) : omap f ∅ = ∅.
 Proof. apply map_empty; intros i. by rewrite lookup_omap, lookup_empty. Qed.
+
+Lemma fmap_empty_inv {A B} (f : A → B) m : f <$> m = ∅ → m = ∅.
+Proof.
+  intros Hm. apply map_eq; intros i. generalize (f_equal (lookup i) Hm).
+  by rewrite lookup_fmap, !lookup_empty, fmap_None.
+Qed.
+
 Lemma fmap_insert {A B} (f: A → B) m i x: f <$> <[i:=x]>m = <[i:=f x]>(f <$> m).
 Proof.
   apply map_eq; intros i'; destruct (decide (i' = i)) as [->|].
@@ -692,7 +692,7 @@ Proof.
 Qed.
 Lemma map_fmap_singleton {A B} (f : A → B) i x : f <$> {[i := x]} = {[i := f x]}.
 Proof.
-  by unfold singletonM, map_singleton; rewrite fmap_insert, map_fmap_empty.
+  by unfold singletonM, map_singleton; rewrite fmap_insert, fmap_empty.
 Qed.
 Lemma omap_singleton {A B} (f : A → option B) i x y :
   f x = Some y → omap f {[ i := x ]} = {[ i := y ]}.