Imagine not removing the duplicate lemmas.

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).