From b84fcb1e475c86b913c0e97e1f32b6fe6b5e01e2 Mon Sep 17 00:00:00 2001
From: Jan Menz <s9jamenz@stud.uni-saarland.de>
Date: Mon, 7 Jun 2021 12:07:53 +0200
Subject: [PATCH] renamed list because l and 1 were indistinguishable

---
 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 d41a94f8..7ca1548f 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) ls : x ∈ ls → f x ≤ sum_list_with f ls.
   Proof. induction 1; simpl; lia. Qed.
   Lemma join_reshape szs l :
     sum_list szs = length l → mjoin (reshape szs l) = l.
-- 
GitLab