From fecd9cf4f46e31aa0eda39f3054fa6e38461af56 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <gitlab-sws@robbertkrebbers.nl>
Date: Mon, 7 Jun 2021 09:39:07 +0000
Subject: [PATCH] Robbert's compression

---
 theories/list_numbers.v | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/theories/list_numbers.v b/theories/list_numbers.v
index 11c1bb17..d41a94f8 100644
--- a/theories/list_numbers.v
+++ b/theories/list_numbers.v
@@ -201,10 +201,7 @@ Section sum_list.
     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.
-  Proof.
-    intros H. induction H.
-    all: simpl; lia.
-  Qed.
+  Proof. induction 1; simpl; lia. Qed.
   Lemma join_reshape szs l :
     sum_list szs = length l → mjoin (reshape szs l) = l.
   Proof.
-- 
GitLab