diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v
index d46161ad4702b70cebe632f37134c2892a988304..402c7189c76b9de46bf01f340049623184a5dc34 100644
--- a/theories/fin_map_dom.v
+++ b/theories/fin_map_dom.v
@@ -24,20 +24,6 @@ Lemma lookup_lookup_total_dom `{!Inhabited A} (m : M A) i :
   i ∈ dom D m → m !! i = Some (m !!! i).
 Proof. rewrite elem_of_dom. apply lookup_lookup_total. Qed.
 
-Lemma dom_filter {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A) X :
-  (∀ i, i ∈ X ↔ ∃ x, m !! i = Some x ∧ P (i, x)) →
-  dom D (filter P m) ≡ X.
-Proof.
-  intros HX i. rewrite elem_of_dom, HX.
-  unfold is_Some. by setoid_rewrite map_filter_lookup_Some.
-Qed.
-Lemma dom_filter_subseteq {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A):
-  dom D (filter P m) ⊆ dom D m.
-Proof.
-  intros ?. rewrite 2!elem_of_dom.
-  destruct 1 as [?[Eq _]%map_filter_lookup_Some]. by eexists.
-Qed.
-
 Lemma dom_imap_subseteq {A B} (f: K → A → option B) (m: M A) :
   dom D (map_imap f m) ⊆ dom D m.
 Proof.
@@ -68,6 +54,18 @@ Proof.
   specialize (Hss2 i). rewrite !elem_of_dom in Hss2.
   destruct Hss2; eauto. by simplify_map_eq.
 Qed.
+
+Lemma dom_filter {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A) X :
+  (∀ i, i ∈ X ↔ ∃ x, m !! i = Some x ∧ P (i, x)) →
+  dom D (filter P m) ≡ X.
+Proof.
+  intros HX i. rewrite elem_of_dom, HX.
+  unfold is_Some. by setoid_rewrite map_filter_lookup_Some.
+Qed.
+Lemma dom_filter_subseteq {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A):
+  dom D (filter P m) ⊆ dom D m.
+Proof. apply subseteq_dom, map_filter_subseteq. Qed.
+
 Lemma dom_empty {A} : dom D (@empty (M A) _) ≡ ∅.
 Proof.
   intros x. rewrite elem_of_dom, lookup_empty, <-not_eq_None_Some. set_solver.
@@ -174,6 +172,14 @@ Proof.
   apply not_elem_of_dom. set_solver.
 Qed.
 
+Lemma dom_map_zip_with {A B C} (f : A → B → C) (ma : M A) (mb : M B) :
+  dom D (map_zip_with f ma mb) ≡ dom D ma ∩ dom D mb.
+Proof.
+  rewrite set_equiv. intros x.
+  rewrite elem_of_intersection, !elem_of_dom, map_lookup_zip_with.
+  destruct (ma !! x), (mb !! x); rewrite !is_Some_alt; naive_solver.
+Qed.
+
 Lemma dom_union_inv `{!RelDecision (∈@{D})} {A} (m : M A) (X1 X2 : D) :
   X1 ## X2 →
   dom D m ≡ X1 ∪ X2 →
@@ -254,6 +260,9 @@ Section leibniz.
   Lemma dom_singleton_inv_L {A} (m : M A) i :
     dom D m = {[i]} → ∃ x, m = {[i := x]}.
   Proof. unfold_leibniz. apply dom_singleton_inv. Qed.
+  Lemma dom_map_zip_with_L {A B C} (f : A → B → C) (ma : M A) (mb : M B) :
+    dom D (map_zip_with f ma mb) = dom D ma ∩ dom D mb.
+  Proof. unfold_leibniz. apply dom_map_zip_with. Qed.
   Lemma dom_union_inv_L `{!RelDecision (∈@{D})} {A} (m : M A) (X1 X2 : D) :
     X1 ## X2 →
     dom D m = X1 ∪ X2 →
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 8167e863e396cdeb3026eed8d99307f784cf120a..629c74984f0988406286a2c40d881d6031a453af 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1378,6 +1378,18 @@ Section map_filter_misc.
     (∀ i x, m !! i = Some x → Q (i, x) → P (i, x)) →
     filter P (filter Q m) = filter Q m.
   Proof. intros ?. rewrite map_filter_filter. apply map_filter_ext. naive_solver. Qed.
+
+  Lemma map_filter_id m :
+    (∀ i x, m !! i = Some x → P (i, x)) → filter P m = m.
+  Proof.
+    intros Hi. apply map_eq. intros i. rewrite map_filter_lookup.
+    destruct (m !! i) eqn:Hlook; [|done].
+    apply option_guard_True, Hi, Hlook.
+  Qed.
+
+  Lemma map_filter_subseteq f `{∀ (x : (K *A)), Decision (f x)} m :
+    filter f m ⊆ m.
+  Proof. apply map_subseteq_spec, map_filter_lookup_Some_1_1. Qed.
 End map_filter_misc.
 
 (** ** Properties of the [map_Forall] predicate *)
@@ -1603,7 +1615,7 @@ Proof.
   rewrite lookup_merge, lookup_omap. by destruct (m !! i).
 Qed.
 
-(** Properties of the [zip_with] and [zip] functions *)
+(** Properties of the [map_zip_with] and [map_zip] functions *)
 Lemma map_lookup_zip_with {A B C} (f : A → B → C) (m1 : M A) (m2 : M B) i :
   map_zip_with f m1 m2 !! i = (x ← m1 !! i; y ← m2 !! i; Some (f x y)).
 Proof.
@@ -1618,6 +1630,10 @@ Lemma map_lookup_zip_with_None {A B C} (f : A → B → C) (m1 : M A) (m2 : M B)
   map_zip_with f m1 m2 !! i = None ↔ m1 !! i = None ∨ m2 !! i = None.
 Proof. rewrite map_lookup_zip_with. destruct (m1 !! i), (m2 !! i); naive_solver. Qed.
 
+Lemma map_lookup_zip_Some {A B} (m1 : M A) (m2 : M B) l p :
+  (map_zip m1 m2) !! l = Some p ↔ m1 !! l = Some p.1 ∧ m2 !! l = Some p.2.
+Proof. rewrite map_lookup_zip_with_Some. destruct p. naive_solver. Qed.
+
 Lemma map_zip_with_empty {A B C} (f : A → B → C) :
   map_zip_with f (∅ : M A) (∅ : M B) = ∅.
 Proof. unfold map_zip_with. by rewrite merge_empty by done. Qed.
diff --git a/theories/sets.v b/theories/sets.v
index 12d584db2de21078e7864a023195e19cf0f76369..0d892c9fa23c46a43ad07902f6762f0df971821d 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -394,6 +394,11 @@ Section semi_set.
   Proof. done. Qed.
   Lemma elem_of_subset X Y : X ⊂ Y ↔ (∀ x, x ∈ X → x ∈ Y) ∧ ¬(∀ x, x ∈ Y → x ∈ X).
   Proof. set_solver. Qed.
+  Lemma elem_of_weaken x X Y : x ∈ X → X ⊆ Y → x ∈ Y.
+  Proof. set_solver. Qed.
+
+  Lemma not_elem_of_weaken x X Y : x ∉ Y → X ⊆ Y → x ∉ X.
+  Proof. set_solver. Qed.
 
   (** Union *)
   Lemma union_subseteq X Y Z : X ∪ Y ⊆ Z ↔ X ⊆ Z ∧ Y ⊆ Z.