From 8b84aff76f6ccb165f998a327acfc9c900989d74 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thibaut=20P=C3=A9rami?= <thibaut.perami@cl.cam.ac.uk>
Date: Mon, 21 Oct 2024 15:07:54 +0100
Subject: [PATCH] Fix naming bug
---
stdpp/list.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/stdpp/list.v b/stdpp/list.v
index 82caddb4..0ece735b 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.
--
GitLab