From 7f97e3843a3b64e614890822639434e3fd41ab81 Mon Sep 17 00:00:00 2001
From: Herman Bergwerf <post@hbergwerf.nl>
Date: Wed, 8 Mar 2023 14:57:16 +0100
Subject: [PATCH] Remove unused names.
---
stdpp/list.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/stdpp/list.v b/stdpp/list.v
index 09283c98..be8279fd 100644
--- a/stdpp/list.v
+++ b/stdpp/list.v
@@ -4233,7 +4233,7 @@ Section bind.
Proof.
intros inj Hf Hl; induction l; cbn; [constructor|inversion_clear Hl].
apply NoDup_app; repeat split; auto; intros b H1 H2.
- apply elem_of_list_bind in H2 as (a' & H3 & H4).
+ apply elem_of_list_bind in H2 as (a'&?&?).
apply (inj a a') in H1; subst; done.
Qed.
End bind.
--
GitLab