Robbert's compression

fecd9cf4 · Robbert Krebbers · Jan · 09d8a70f · fecd9cf4
Commit fecd9cf4 authored Jun 07, 2021 by Robbert Krebbers Committed by Jan Jun 07, 2021
--- 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.