From a38f98468642d3e0bc7fb7de40cc4f90c6fe71ad Mon Sep 17 00:00:00 2001
From: Matthias Meijers <research@mmeijers.com>
Date: Thu, 20 Feb 2025 11:49:49 +0100
Subject: [PATCH] Imagine not removing the duplicate lemmas.

---
 theories/datatypes/List.ec | 9 ---------
 1 file changed, 9 deletions(-)

diff --git a/theories/datatypes/List.ec b/theories/datatypes/List.ec
index 05f9052d8..d7159c869 100644
--- a/theories/datatypes/List.ec
+++ b/theories/datatypes/List.ec
@@ -1753,15 +1753,6 @@ move=> peq_s1s2; rewrite uniq_perm_eq 1,2:undup_uniq => x.
 by rewrite 2!mem_undup &(perm_eq_mem).
 qed.
 
-lemma count_mem_uniq (s : 'a list):
-  (forall x, count (pred1 x) s = b2i (mem s x)) => uniq s.
-proof.
-  move=> count1_s; have Uus := undup_uniq s.
-  apply (perm_eq_uniq (undup s)); last by apply undup_uniq.
-  rewrite /perm_eq allP => x _ /=; rewrite count1_s.
-  by rewrite (count_uniq_mem (undup s) x) ?undup_uniq // mem_undup.
-qed.
-
 lemma filter_swap ['a] (xs ys : 'a list) :
   uniq xs => uniq ys =>
     perm_eq (filter (mem xs) ys) (filter (mem ys) xs).