diff --git a/CHANGELOG.md b/CHANGELOG.md
index bade5df0d729a3dd47673da0e2aebbfdde45622c..9b87bae3ebb6ab058ef8118abdd0215732452927 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -138,6 +138,7 @@ API-breaking change is listed.
 - Make `map_empty` a biimplication.
 - Clean up `empty{',_inv,_iff}` lemmas:
   + Write them all using `↔` and consistently use the `_iff` suffix.
+    (But keep the `_inv` version when it is useful for rewriting.)
   + Remove `map_to_list_empty_inv_alt`; chain `Permutation_nil_r` and
     `map_to_list_empty_iff` instead.
   + Add lemma `map_filter_empty_iff`.
@@ -202,15 +203,10 @@ s/\bmap_union_subseteq_(r|l)_alt\b/map_union_subseteq_\1'/g
 # singleton
 s/\bgmultiset_elem_of_singleton_subseteq\b/gmultiset_singleton_subseteq_l/g
 # empty_iff
-s/\bfmap_empty_inv\b/fmap_empty_iff/g
 s/\bmap_to_list_empty('|_inv)\b/map_to_list_empty_iff/g
-s/\bmap_size_empty_inv\b/map_size_empty_iff/g
 s/\bkmap_empty_inv\b/kmap_empty_iff/g
-s/\belements_empty('|_inv)\b/elements_empty_iff/g
-s/\bsize_empty_inv\b/size_empty_iff/g
-s/\bdom_empty_inv(_L|)\b/dom_empty_iff\1/g
-s/\bgmultiset_elements_empty('|_inv)\b/gmultiset_elements_empty_iff/g
-s/\bgmultiset_size_empty_inv\b/gmultiset_size_empty_iff/g
+s/\belements_empty'\b/elements_empty_iff/g
+s/\bgmultiset_elements_empty'\b/gmultiset_elements_empty_iff/g
 # map_filter_insert
 s/\bmap_filter_insert\b/map_filter_insert_True/g
 s/\bmap_filter_insert_not_delete\b/map_filter_insert_False/g
diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v
index dce00f29d05ec5b340ebb4dacc6a0d4ff668979a..c9951d4a8d715cbc4410885cea2693983a24084a 100644
--- a/theories/fin_map_dom.v
+++ b/theories/fin_map_dom.v
@@ -76,6 +76,8 @@ Proof.
   intros E. apply map_empty. intros. apply not_elem_of_dom.
   rewrite E. set_solver.
 Qed.
+Lemma dom_empty_inv {A} (m : M A) : dom D m ≡ ∅ → m = ∅.
+Proof. apply dom_empty_iff. Qed.
 Lemma dom_alter {A} f (m : M A) i : dom D (alter f i m) ≡ dom D m.
 Proof.
   apply set_equiv; intros j; rewrite !elem_of_dom; unfold is_Some.
@@ -231,6 +233,8 @@ Section leibniz.
   Proof. unfold_leibniz; apply dom_empty. Qed.
   Lemma dom_empty_iff_L {A} (m : M A) : dom D m = ∅ ↔ m = ∅.
   Proof. unfold_leibniz. apply dom_empty_iff. Qed.
+  Lemma dom_empty_inv_L {A} (m : M A) : dom D m = ∅ → m = ∅.
+  Proof. by intros; apply dom_empty_inv; unfold_leibniz. Qed.
   Lemma dom_alter_L {A} f (m : M A) i : dom D (alter f i m) = dom D m.
   Proof. unfold_leibniz; apply dom_alter. Qed.
   Lemma dom_insert_L {A} (m : M A) i x : dom D (<[i:=x]>m) = {[ i ]} ∪ dom D m.
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 653842a565d3dc83b1f9b18077b2d5a6cc96c15c..8bbcffa18b8e2386d2c106cbcdb48dbe795e3ccc 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -646,6 +646,8 @@ 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_empty_inv {A B} (f : A → B) m : f <$> m =@{M B} ∅ → m = ∅.
+Proof. apply fmap_empty_iff. Qed.
 
 Lemma fmap_insert {A B} (f: A → B) (m : M A) i x :
   f <$> <[i:=x]>m = <[i:=f x]>(f <$> m).
@@ -1042,6 +1044,8 @@ Lemma map_size_empty_iff {A} (m : M A) : size m = 0 ↔ m = ∅.
 Proof.
   unfold size, map_size. by rewrite length_zero_iff_nil, map_to_list_empty_iff.
 Qed.
+Lemma map_size_empty_inv {A} (m : M A) : size m = 0 → m = ∅.
+Proof. apply map_size_empty_iff. Qed.
 Lemma map_size_non_empty_iff {A} (m : M A) : size m ≠ 0 ↔ m ≠ ∅.
 Proof. by rewrite map_size_empty_iff. Qed.
 
diff --git a/theories/fin_sets.v b/theories/fin_sets.v
index c47c8e643bc6c25aaa0341c37e921c8e0c472e50..5f5168a7040b0f573c8a708fbf84f52cb1cb1094 100644
--- a/theories/fin_sets.v
+++ b/theories/fin_sets.v
@@ -83,6 +83,8 @@ Proof.
   intros HX. apply elem_of_equiv_empty; intros x.
   rewrite <-elem_of_elements, HX. apply not_elem_of_nil.
 Qed.
+Lemma elements_empty_inv X : elements X = [] → X ≡ ∅.
+Proof. apply elements_empty_iff. Qed.
 
 Lemma elements_union_singleton (X : C) x :
   x ∉ X → elements ({[ x ]} ∪ X) ≡ₚ x :: elements X.
@@ -129,6 +131,8 @@ Proof.
   intros; apply equiv_empty; intros x; rewrite <-elem_of_elements.
   by rewrite (nil_length_inv (elements X)), ?elem_of_nil.
 Qed.
+Lemma size_empty_inv (X : C) : size X = 0 → X ≡ ∅.
+Proof. apply size_empty_iff. Qed.
 Lemma size_non_empty_iff (X : C) : size X ≠ 0 ↔ X ≢ ∅.
 Proof. by rewrite size_empty_iff. Qed.
 
diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index c6eb06ca60458c57172b019160d89ffead06a66a..f6a8a17158c3358a25b78bd5ab55e594ae247785 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -414,6 +414,8 @@ Section more_lemmas.
     - by apply map_to_list_empty_iff.
     - naive_solver.
   Qed.
+  Lemma gmultiset_elements_empty_inv X : elements X = [] → X = ∅.
+  Proof. apply gmultiset_elements_empty_iff. Qed.
 
   Lemma gmultiset_elements_singleton x : elements ({[+ x +]} : gmultiset A) = [ x ].
   Proof.
@@ -480,6 +482,8 @@ Section more_lemmas.
     unfold size, gmultiset_size; simpl.
     by rewrite length_zero_iff_nil, gmultiset_elements_empty_iff.
   Qed.
+  Lemma gmultiset_size_empty_inv X : size X = 0 → X = ∅.
+  Proof. apply gmultiset_size_empty_iff. Qed.
   Lemma gmultiset_size_non_empty_iff X : size X ≠ 0 ↔ X ≠ ∅.
   Proof. by rewrite gmultiset_size_empty_iff. Qed.