diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v
index 4da774f931ce3e36173ada01da174020e0bf5f06..b956dce9d738e9c988cdf601a3f2ade16b4ca539 100644
--- a/theories/fin_map_dom.v
+++ b/theories/fin_map_dom.v
@@ -42,6 +42,10 @@ Lemma elem_of_dom_2 {A} (m : M A) i x : m !! i = Some x → i ∈ dom m.
 Proof. rewrite elem_of_dom; eauto. Qed.
 Lemma not_elem_of_dom {A} (m : M A) i : i ∉ dom m ↔ m !! i = None.
 Proof. by rewrite elem_of_dom, eq_None_not_Some. Qed.
+Lemma not_elem_of_dom_1 {A} (m : M A) i : i ∉ dom m → m !! i = None.
+Proof. apply not_elem_of_dom. Qed.
+Lemma not_elem_of_dom_2 {A} (m : M A) i : m !! i = None → i ∉ dom m.
+Proof. apply not_elem_of_dom. Qed.
 Lemma subseteq_dom {A} (m1 m2 : M A) : m1 ⊆ m2 → dom m1 ⊆ dom m2.
 Proof.
   rewrite map_subseteq_spec.
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 6331dde71f90e3031c41f1686f867b8c23347224..1ade48beb3838aacf5b25818f6ead4bc80f57445 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -2273,6 +2273,12 @@ Proof. rewrite lookup_union. destruct (m1 !! i), (m2 !! i); naive_solver. Qed.
 Lemma lookup_union_None {A} (m1 m2 : M A) i :
   (m1 ∪ m2) !! i = None ↔ m1 !! i = None ∧ m2 !! i = None.
 Proof. rewrite lookup_union.  destruct (m1 !! i), (m2 !! i); naive_solver. Qed.
+Lemma lookup_union_None_1 {A} (m1 m2 : M A) i :
+  (m1 ∪ m2) !! i = None → m1 !! i = None ∧ m2 !! i = None.
+Proof. apply lookup_union_None. Qed.
+Lemma lookup_union_None_2 {A} (m1 m2 : M A) i :
+  m1 !! i = None → m2 !! i = None → (m1 ∪ m2) !! i = None.
+Proof. intros. by apply lookup_union_None. Qed.
 Lemma lookup_union_Some {A} (m1 m2 : M A) i x :
   m1 ##ₘ m2 → (m1 ∪ m2) !! i = Some x ↔ m1 !! i = Some x ∨ m2 !! i = Some x.
 Proof.