diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 48aae385833f66d4077b8a72b3fce07e026f4b2d..06ef84efc34a76c875b58a0e810c31fd519d7f2a 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1388,7 +1388,7 @@ Section map_filter_misc.
   Proof. apply map_fold_empty. Qed.
 
   Lemma map_filter_singleton i x :
-    P (i,x) → filter P ({[i := x]} : M A) = {[i := x]}.
+    P (i,x) → filter P {[i := x]} =@{M A} {[i := x]}.
   Proof.
     intros ?. rewrite <-insert_empty, map_filter_insert; [|done].
     by rewrite map_filter_empty.
@@ -1438,7 +1438,7 @@ Section map_filter_misc.
 End map_filter_misc.
 
 Lemma map_filter_comm {A}
-  (P : K * A → Prop) `{!∀ x, Decision (P x)} Q `{!∀ x, Decision (Q x)} (m : M A) :
+    (P Q : K * A → Prop) `{!∀ x, Decision (P x), !∀ x, Decision (Q x)} (m : M A) :
   filter P (filter Q m) = filter Q (filter P m).
 Proof. rewrite !map_filter_filter. apply map_filter_ext. naive_solver. Qed.