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..0c491c92381ddda38a26229c3ee414080153a948 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.