diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 124966f739f3a186928fdb08c89e8a5312c6f49d..f60677832bd32b5aab24e7278361f350c199e774 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -261,6 +261,11 @@ Proof.
 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).