diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index a30f41b07302dee829e696855d5f75e661ae30ca..7974c11da856208f4e87f9171d0fa2e4162d4536 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1314,13 +1314,17 @@ Section map_filter_ext.
     filter P m = filter Q m.
   Proof. intro. apply map_filter_strong_ext. naive_solver. Qed.
 
-  Lemma map_filter_subseteq_ext (m : M A) :
-    (∀ i x, m !! i = Some x → P (i, x) → Q (i, x)) →
-    filter P m ⊆ filter Q m.
+  Lemma map_filter_strong_subseteq_ext (m1 m2 : M A) :
+    (∀ i x, (P (i, x) ∧ m1 !! i = Some x) → (Q (i, x) ∧ m2 !! i = Some x)) →
+    filter P m1 ⊆ filter Q m2.
   Proof.
     rewrite map_subseteq_spec. intros Himpl ??.
     rewrite 2!map_filter_lookup_Some. naive_solver.
   Qed.
+  Lemma map_filter_subseteq_ext (m : M A) :
+    (∀ i x, m !! i = Some x → P (i, x) → Q (i, x)) →
+    filter P m ⊆ filter Q m.
+  Proof. intro. apply map_filter_strong_subseteq_ext. naive_solver. Qed.
 End map_filter_ext.
 
 Section map_filter_insert_and_delete.
@@ -1399,8 +1403,8 @@ Section map_filter_misc.
 
   Lemma map_filter_subseteq_mono m1 m2 : m1 ⊆ m2 → filter P m1 ⊆ filter P m2.
   Proof.
-    rewrite 2!map_subseteq_spec. intros Le i x.
-    rewrite 2!map_filter_lookup_Some. naive_solver.
+    rewrite map_subseteq_spec. intros Hm1m2.
+    apply map_filter_strong_subseteq_ext. naive_solver.
   Qed.
 
   Lemma map_filter_alt m : filter P m = list_to_map (filter P (map_to_list m)).