diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 6cb16d4ea5bf867750440e3962959d8bb18c7164..e5c1e0658d821af83d94dcc061f385e830c90750 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1279,6 +1279,13 @@ Section map_filter_lookup.
     m !! i = None ∨ (∀ x : A, m !! i = Some x → ¬ P (i, x)) →
     filter P m !! i = None.
   Proof. apply map_filter_lookup_None. Qed.
+
+  Lemma map_filter_empty_not_lookup m i x :
+    filter P m = ∅ → P (i,x) → m !! i ≠ Some x.
+  Proof.
+    rewrite map_empty. setoid_rewrite map_filter_lookup_None. intros Hm ?.
+    destruct (Hm i); naive_solver.
+  Qed.
 End map_filter_lookup.
 
 Section map_filter_ext.
diff --git a/theories/fin_sets.v b/theories/fin_sets.v
index ed7e1034b49bd8598d64583744ec2386083242c5..41f8311c9f2e5884d6cc3dbf328e57a5cf668909 100644
--- a/theories/fin_sets.v
+++ b/theories/fin_sets.v
@@ -353,6 +353,9 @@ Section filter.
   Lemma filter_singleton_not x : ¬P x → filter P ({[ x ]} : C) ≡ ∅.
   Proof. set_solver. Qed.
 
+  Lemma filter_empty_not_elem_of X x : filter P X ≡ ∅ → P x → x ∉ X.
+  Proof. set_solver. Qed.
+
   Lemma disjoint_filter X Y : X ## Y → filter P X ## filter P Y.
   Proof. set_solver. Qed.
   Lemma filter_union X Y : filter P (X ∪ Y) ≡ filter P X ∪ filter P Y.
@@ -371,6 +374,9 @@ Section filter.
     Lemma filter_singleton_not_L x : ¬P x → filter P ({[ x ]} : C) = ∅.
     Proof. unfold_leibniz. apply filter_singleton_not. Qed.
 
+    Lemma filter_empty_not_elem_of_L X x : filter P X = ∅ → P x → x ∉ X.
+    Proof. unfold_leibniz. apply filter_empty_not_elem_of. Qed.
+
     Lemma filter_union_L X Y : filter P (X ∪ Y) = filter P X ∪ filter P Y.
     Proof. unfold_leibniz. apply filter_union. Qed.
     Lemma filter_union_complement_L X Y : filter P X ∪ filter (λ x, ¬P x) X = X.
diff --git a/theories/list.v b/theories/list.v
index 3b05646885b314c4a1891bca7d1e53617a03722a..ccfdef77c4b32a5a1f711e62722f901ad9d75eef 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -1987,6 +1987,9 @@ Section filter.
     intros [k ->]%elem_of_Permutation ?; simpl.
     rewrite decide_False, Nat.lt_succ_r by done. apply filter_length.
   Qed.
+
+  Lemma filter_nil_not_elem_of l x : filter P l = [] → P x → x ∉ l.
+  Proof. induction 3; simplify_eq/=; case_decide; naive_solver. Qed.
 End filter.
 
 Lemma list_filter_iff (P1 P2 : A → Prop)