From 09d8a70fb6b3c942b3a2342e38009dfecaf9d816 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <gitlab-sws@robbertkrebbers.nl>
Date: Mon, 7 Jun 2021 09:37:40 +0000
Subject: [PATCH] Robbert's changes to spaces

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

diff --git a/theories/list_numbers.v b/theories/list_numbers.v
index a3fce30e..11c1bb17 100644
--- a/theories/list_numbers.v
+++ b/theories/list_numbers.v
@@ -200,7 +200,7 @@ Section sum_list.
   Proof.
     induction l; simpl; rewrite ?reverse_cons, ?sum_list_with_app; simpl; lia.
   Qed.
-  Lemma sum_list_with_in x (f: A → nat) l: x ∈ l → f x ≤ sum_list_with f l.  
+  Lemma sum_list_with_in x (f : A → nat) l : x ∈ l → f x ≤ sum_list_with f l.
   Proof.
     intros H. induction H.
     all: simpl; lia.
-- 
GitLab