diff --git a/theories/list.v b/theories/list.v
index e783a7ae1dc7f281c8c4baec78deccff6d85242a..48364041a9decb55cd86a82c58c662c9a0a1e737 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -2756,7 +2756,7 @@ Proof.
   destruct i as [|i];
     [by apply list_subseteq_cons|by apply list_subseteq_skip].
 Qed.
-Lemma list_filter_subseteq P `{! ∀ x : A, Decision (P x)} l :
+Lemma list_filter_subseteq P `{!∀ x : A, Decision (P x)} l :
   filter P l ⊆ l.
 Proof.
   induction l as [|x l IHl]; [done|]. rewrite filter_cons.