diff --git a/stdpp/list.v b/stdpp/list.v
index 82caddb47a2c5286e409ff15a93be35d3478f863..0ece735b8af3127b6d5519de8ccf41d33ccd5da9 100644
--- a/stdpp/list.v
+++ b/stdpp/list.v
@@ -954,10 +954,10 @@ Qed.
 Lemma list_cprod_list_prod {B} l1 (l2 : list B) :
   cprod l1 l2 = list_prod l1 l2.
 Proof.
-  induction l1.
+  induction l1 as [|?? IH].
   - by unfold cprod, list_cprod.
   - unfold cprod, list_cprod in *. simpl.
-    by setoid_rewrite IHl1.
+    by setoid_rewrite IH.
 Qed.
 Lemma elem_of_list_cprod {B} l1 (l2 : list B) (x : A * B) :
   x ∈ cprod l1 l2 ↔ x.1 ∈ l1 ∧ x.2 ∈ l2.