diff --git a/CHANGELOG.md b/CHANGELOG.md
index 316a3a6e337a5017aaf2ad84e10c13625b1039b1..4f1dabb9841c26088f2e14e6558c0865c81f0b1f 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -135,12 +135,18 @@ API-breaking change is listed.
 - Add lemmas `map_singleton_subseteq_l` and `map_singleton_subseteq` for maps.
 - Add lemmas `singleton_submseteq_l` and `singleton_submseteq` for unordered
   list inclusion, as well as `lookup_submseteq` and `submseteq_insert`.
+- Make `map_empty` a biimplication.
+- Clean up `empty{',_inv,_iff}` lemmas:
+  + Write them all using `↔` and consistently use the `_iff` suffix.
+  + Remove `map_to_list_empty_inv_alt`; chain `Permutation_nil_r` and
+    `map_to_list_empty_iff` instead.
+  + Add lemma `map_filter_empty_iff`.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
 Note that the script is not idempotent, do not run it twice.
 ```
-sed -i -E '
+sed -i -E -f- $(find theories -name "*.v") <<EOF
 s/\bdecide_left\b/decide_True_pi/g
 s/\bdecide_right\b/decide_False_pi/g
 # Permutation
@@ -179,7 +185,17 @@ s/\blookup_gmap_uncurry_None\b/lookup_gmap_curry_None/g
 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
-' $(find theories -name "*.v")
+# 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
+EOF
 ```
 
 ## std++ 1.5.0 (2021-02-16)
diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v
index 402c7189c76b9de46bf01f340049623184a5dc34..dce00f29d05ec5b340ebb4dacc6a0d4ff668979a 100644
--- a/theories/fin_map_dom.v
+++ b/theories/fin_map_dom.v
@@ -70,8 +70,9 @@ Lemma dom_empty {A} : dom D (@empty (M A) _) ≡ ∅.
 Proof.
   intros x. rewrite elem_of_dom, lookup_empty, <-not_eq_None_Some. set_solver.
 Qed.
-Lemma dom_empty_inv {A} (m : M A) : dom D m ≡ ∅ → m = ∅.
+Lemma dom_empty_iff {A} (m : M A) : dom D m ≡ ∅ ↔ m = ∅.
 Proof.
+  split; [|intros ->; by rewrite dom_empty].
   intros E. apply map_empty. intros. apply not_elem_of_dom.
   rewrite E. set_solver.
 Qed.
@@ -228,8 +229,8 @@ Section leibniz.
   Proof. unfold_leibniz. apply dom_filter. Qed.
   Lemma dom_empty_L {A} : dom D (@empty (M A) _) = ∅.
   Proof. unfold_leibniz; apply dom_empty. 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_empty_iff_L {A} (m : M A) : dom D m = ∅ ↔ m = ∅.
+  Proof. unfold_leibniz. apply dom_empty_iff. 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 62255ab4e1cce756f71af2d5cf8a8f7a2e349ad9..2707671d9bdfe6af5f2d720005b8ba137ffa308a 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -221,8 +221,12 @@ Lemma lookup_weaken_inv {A} (m1 m2 : M A) i x y :
 Proof. intros Hm1 ? Hm2. eapply lookup_weaken in Hm1; eauto. congruence. Qed.
 Lemma lookup_ne {A} (m : M A) i j : m !! i ≠ m !! j → i ≠ j.
 Proof. congruence. Qed.
-Lemma map_empty {A} (m : M A) : (∀ i, m !! i = None) → m = ∅.
-Proof. intros Hm. apply map_eq. intros. by rewrite Hm, lookup_empty. Qed.
+Lemma map_empty {A} (m : M A) : m = ∅ ↔ ∀ i, m !! i = None.
+Proof.
+  split.
+  - intros -> i. by rewrite lookup_empty.
+  - intros Hm. apply map_eq. intros i. by rewrite Hm, lookup_empty.
+Qed.
 Lemma lookup_empty_is_Some {A} i : ¬is_Some ((∅ : M A) !! i).
 Proof. rewrite lookup_empty. by inversion 1. Qed.
 Lemma lookup_empty_Some {A} i (x : A) : ¬(∅ : M A) !! i = Some x.
@@ -636,8 +640,9 @@ Proof. apply map_empty; intros i. by rewrite lookup_fmap, lookup_empty. Qed.
 Lemma omap_empty {A B} (f : A → option B) : omap f ∅ =@{M B} ∅.
 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 B} ∅ → m = ∅.
+Lemma fmap_empty_iff {A B} (f : A → B) m : f <$> m =@{M B} ∅ ↔ m = ∅.
 Proof.
+  split; [|intros ->; by rewrite fmap_empty].
   intros Hm. apply map_eq; intros i. generalize (f_equal (lookup i) Hm).
   by rewrite lookup_fmap, !lookup_empty, fmap_None.
 Qed.
@@ -924,13 +929,11 @@ Proof.
   by rewrite <-list_to_map_fmap, map_to_list_to_map.
 Qed.
 
-Lemma map_to_list_empty_inv_alt {A}  (m : M A) : map_to_list m ≡ₚ [] → m = ∅.
-Proof. rewrite <-map_to_list_empty. apply map_to_list_inj. Qed.
-Lemma map_to_list_empty_inv {A} (m : M A) : map_to_list m = [] → m = ∅.
-Proof. intros Hm. apply map_to_list_empty_inv_alt. by rewrite Hm. Qed.
-Lemma map_to_list_empty' {A} (m : M A) : map_to_list m = [] ↔ m = ∅.
+Lemma map_to_list_empty_iff {A} (m : M A) : map_to_list m = [] ↔ m = ∅.
 Proof.
-  split; [apply map_to_list_empty_inv|]. intros ->. apply map_to_list_empty.
+  split.
+  - rewrite <-Permutation_nil_r, <-map_to_list_empty. apply map_to_list_inj.
+  - intros ->. apply map_to_list_empty.
 Qed.
 
 Lemma map_to_list_insert_inv {A} (m : M A) l i x :
@@ -946,15 +949,15 @@ Qed.
 
 Lemma map_choose {A} (m : M A) : m ≠ ∅ → ∃ i x, m !! i = Some x.
 Proof.
-  intros Hemp. destruct (map_to_list m) as [|[i x] l] eqn:Hm.
-  { destruct Hemp; eauto using map_to_list_empty_inv. }
+  rewrite <-map_to_list_empty_iff.
+  intros Hemp. destruct (map_to_list m) as [|[i x] l] eqn:Hm; [done|].
   exists i, x. rewrite <-elem_of_map_to_list, Hm. by left.
 Qed.
 
 Global Instance map_eq_dec_empty {A} (m : M A) : Decision (m = ∅) | 20.
 Proof.
   refine (cast_if (decide (map_to_list m = [])));
-    by rewrite <-?map_to_list_empty'.
+    by rewrite <-?map_to_list_empty_iff.
 Defined.
 
 (** Properties of the imap function *)
@@ -1035,14 +1038,9 @@ Proof. unfold map_imap. by rewrite map_to_list_empty. Qed.
 (** ** Properties of the size operation *)
 Lemma map_size_empty {A} : size (∅ : M A) = 0.
 Proof. unfold size, map_size. by rewrite map_to_list_empty. Qed.
-Lemma map_size_empty_inv {A} (m : M A) : size m = 0 → m = ∅.
-Proof.
-  unfold size, map_size. by rewrite length_zero_iff_nil, map_to_list_empty'.
-Qed.
 Lemma map_size_empty_iff {A} (m : M A) : size m = 0 ↔ m = ∅.
 Proof.
-  split; [apply map_size_empty_inv|].
-  by intros ->; rewrite map_size_empty.
+  unfold size, map_size. by rewrite length_zero_iff_nil, map_to_list_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.
@@ -1143,7 +1141,7 @@ Proof.
   { intros help m.
     apply (help (map_to_list m)); auto using NoDup_fst_map_to_list. }
   intros l. induction l as [|[i x] l IH]; intros Hnodup m Hml.
-  { apply map_to_list_empty_inv_alt in Hml. by subst. }
+  { rewrite Permutation_nil_r, map_to_list_empty_iff in Hml. by rewrite Hml. }
   inversion_clear Hnodup.
   apply map_to_list_insert_inv in Hml; subst m. apply Hins.
   - by apply not_elem_of_list_to_map_1.
@@ -1155,7 +1153,7 @@ Proof.
   revert m2. induction m1 as [|i x m ? IH] using map_ind.
   { intros m2 Hm2. rewrite map_to_list_empty. simpl.
     apply neq_0_lt. intros Hlen. symmetry in Hlen.
-    apply nil_length_inv, map_to_list_empty_inv in Hlen.
+    apply nil_length_inv, map_to_list_empty_iff in Hlen.
     rewrite Hlen in Hm2. destruct (irreflexivity (⊂) ∅ Hm2). }
   intros m2 Hm2.
   destruct (insert_subset_inv m m2 i x) as (m2'&?&?&?); auto; subst.
@@ -1360,6 +1358,15 @@ Section map_filter_misc.
   Lemma map_filter_empty : filter P ∅ =@{M A} ∅.
   Proof. apply map_fold_empty. Qed.
 
+  Lemma map_filter_empty_iff m :
+    filter P m = ∅ ↔ map_Forall (λ i x, ¬P (i,x)) m.
+  Proof.
+    rewrite map_empty. setoid_rewrite map_filter_lookup_None. split.
+    - intros Hm i x Hi. destruct (Hm i); naive_solver.
+    - intros Hm i. destruct (m !! i) as [x|] eqn:?; [|by auto].
+      right; intros ? [= <-]. by apply Hm.
+  Qed.
+
   Lemma map_filter_alt m : filter P m = list_to_map (filter P (map_to_list m)).
   Proof.
     apply list_to_map_flip. induction m as [|k x m ? IH] using map_ind.
@@ -3027,11 +3034,8 @@ Section kmap.
 
   Lemma kmap_empty {A} : kmap f ∅ =@{M2 A} ∅.
   Proof. unfold kmap. by rewrite map_to_list_empty. Qed.
-  Lemma kmap_empty_inv {A} (m : M1 A) : kmap f m = ∅ → m = ∅.
-  Proof.
-    intros Hm. apply map_empty; intros i.
-    apply (lookup_kmap_None _ (f i)); [|done]. by rewrite Hm, lookup_empty.
-  Qed.
+  Lemma kmap_empty_iff {A} (m : M1 A) : kmap f m = ∅ ↔ m = ∅.
+  Proof. rewrite !map_empty. setoid_rewrite lookup_kmap_None. naive_solver. Qed.
 
   Lemma kmap_singleton {A} i (x : A) : kmap f {[ i := x ]} = {[ f i := x ]}.
   Proof. unfold kmap. by rewrite map_to_list_singleton. Qed.
diff --git a/theories/fin_sets.v b/theories/fin_sets.v
index 2aaa7c5361acef463dd63a664ec0e5e883af6b5e..c47c8e643bc6c25aaa0341c37e921c8e0c472e50 100644
--- a/theories/fin_sets.v
+++ b/theories/fin_sets.v
@@ -77,15 +77,11 @@ Proof.
   apply elem_of_nil_inv; intros x.
   rewrite elem_of_elements, elem_of_empty; tauto.
 Qed.
-Lemma elements_empty_inv X : elements X = [] → X ≡ ∅.
+Lemma elements_empty_iff X : elements X = [] ↔ X ≡ ∅.
 Proof.
-  intros HX; apply elem_of_equiv_empty; intros x.
-  rewrite <-elem_of_elements, HX, elem_of_nil. tauto.
-Qed.
-Lemma elements_empty' X : elements X = [] ↔ X ≡ ∅.
-Proof.
-  split; intros HX; [by apply elements_empty_inv|].
-  by rewrite <-Permutation_nil_r, HX, elements_empty.
+  rewrite <-Permutation_nil_r. split; [|intros ->; by rewrite elements_empty].
+  intros HX. apply elem_of_equiv_empty; intros x.
+  rewrite <-elem_of_elements, HX. apply not_elem_of_nil.
 Qed.
 
 Lemma elements_union_singleton (X : C) x :
@@ -127,13 +123,12 @@ Proof. intros ?? E. apply Permutation_length. by rewrite E. Qed.
 
 Lemma size_empty : size (∅ : C) = 0.
 Proof. unfold size, set_size. simpl. by rewrite elements_empty. Qed.
-Lemma size_empty_inv (X : C) : size X = 0 → X ≡ ∅.
+Lemma size_empty_iff (X : C) : size X = 0 ↔ X ≡ ∅.
 Proof.
+  split; [|intros ->; by rewrite size_empty].
   intros; apply equiv_empty; intros x; rewrite <-elem_of_elements.
   by rewrite (nil_length_inv (elements X)), ?elem_of_nil.
 Qed.
-Lemma size_empty_iff (X : C) : size X = 0 ↔ X ≡ ∅.
-Proof. split; [apply size_empty_inv|]. by intros ->; rewrite size_empty. 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 46486b49b33f973a708c89d08bb4b76b3b233418..c6eb06ca60458c57172b019160d89ffead06a66a 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -406,18 +406,15 @@ Section more_lemmas.
   Proof.
     unfold elements, gmultiset_elements; simpl. by rewrite map_to_list_empty.
   Qed.
-  Lemma gmultiset_elements_empty_inv X : elements X = [] → X = ∅.
+  Lemma gmultiset_elements_empty_iff X : elements X = [] ↔ X = ∅.
   Proof.
+    split; [|intros ->; by rewrite gmultiset_elements_empty].
     destruct X as [X]; unfold elements, gmultiset_elements; simpl.
     intros; apply (f_equal GMultiSet). destruct (map_to_list X) as [|[]] eqn:?.
-    - by apply map_to_list_empty_inv.
+    - by apply map_to_list_empty_iff.
     - naive_solver.
   Qed.
-  Lemma gmultiset_elements_empty' X : elements X = [] ↔ X = ∅.
-  Proof.
-    split; intros HX; [by apply gmultiset_elements_empty_inv|].
-    by rewrite HX, gmultiset_elements_empty.
-  Qed.
+
   Lemma gmultiset_elements_singleton x : elements ({[+ x +]} : gmultiset A) = [ x ].
   Proof.
     unfold elements, gmultiset_elements; simpl. by rewrite map_to_list_singleton.
@@ -478,15 +475,10 @@ Section more_lemmas.
   (** Properties of the size operation *)
   Lemma gmultiset_size_empty : size (∅ : gmultiset A) = 0.
   Proof. done. Qed.
-  Lemma gmultiset_size_empty_inv X : size X = 0 → X = ∅.
-  Proof.
-    unfold size, gmultiset_size; simpl. rewrite length_zero_iff_nil.
-    apply gmultiset_elements_empty_inv.
-  Qed.
   Lemma gmultiset_size_empty_iff X : size X = 0 ↔ X = ∅.
   Proof.
-    split; [apply gmultiset_size_empty_inv|].
-    by intros ->; rewrite gmultiset_size_empty.
+    unfold size, gmultiset_size; simpl.
+    by rewrite length_zero_iff_nil, gmultiset_elements_empty_iff.
   Qed.
   Lemma gmultiset_size_non_empty_iff X : size X ≠ 0 ↔ X ≠ ∅.
   Proof. by rewrite gmultiset_size_empty_iff. Qed.
@@ -494,7 +486,7 @@ Section more_lemmas.
   Lemma gmultiset_choose_or_empty X : (∃ x, x ∈ X) ∨ X = ∅.
   Proof.
     destruct (elements X) as [|x l] eqn:HX; [right|left].
-    - by apply gmultiset_elements_empty_inv.
+    - by apply gmultiset_elements_empty_iff.
     - exists x. rewrite <-gmultiset_elem_of_elements, HX. by left.
   Qed.
   Lemma gmultiset_choose X : X ≠ ∅ → ∃ x, x ∈ X.