From 03bdbb8dc14904a3c8305b1f8733353929ec43b9 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <gitlab-sws@robbertkrebbers.nl>
Date: Fri, 14 Jan 2022 10:58:19 +0000
Subject: [PATCH] Apply 1 suggestion(s) to 1 file(s)

---
 theories/list.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/list.v b/theories/list.v
index e783a7ae..48364041 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.
-- 
GitLab