diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index d33449b0845b4c5579ea278c4edf78e3fc27eca9..3dcbe66b9414d3e8cfd035323e8c8d2464ff561e 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -2600,6 +2600,14 @@ Section setoid.
     intros f f' ? m m' ? k; rewrite !lookup_omap. by apply option_bind_proper.
   Qed.
 
+  Global Instance map_filter_proper (P : K * A → Prop) `{!∀ kx, Decision (P kx)} :
+    (∀ k, Proper ((≡) ==> iff) (uncurry P k)) →
+    Proper ((≡@{M A}) ==> (≡)) (filter P).
+  Proof.
+    intros ? m1 m2 Hm i. rewrite !map_filter_lookup.
+    destruct (Hm i); simpl; repeat case_option_guard; try constructor; naive_solver.
+  Qed.
+
   Global Instance map_singleton_equiv_inj :
     Inj2 (=) (≡) (≡) (singletonM (M:=M A)).
   Proof.