diff --git a/theories/list_numbers.v b/theories/list_numbers.v
index c9a39d2da43cbe62bdcaa495261bee2a911178de..28c37363d517ea7fa3964de959207e9cd90c9cc2 100644
--- a/theories/list_numbers.v
+++ b/theories/list_numbers.v
@@ -202,7 +202,7 @@ Section sum_list.
   Qed.
   Lemma sum_list_with_in x (f: A -> nat) l: x ∈ l -> f x ≤ sum_list_with f l.  
   Proof.
-    intros. induction l.
+    intros H. induction l.
     - contradict H. apply not_elem_of_nil. 
     - cbn. rewrite elem_of_cons in H. destruct H as [H | H].
       + simplify_eq. lia.