proposition: Lemma eq_count_undup a s1 s2 : {in a, s1 =i s2} -> count a (undup s1) = count a (undup s2).
proof: Proof. move=> s1_eq_s2; rewrite -!size_filter !filter_undup. apply/perm_size/perm_undup => x. by rewrite !mem_filter; case: (boolP (a x)) => //= /s1_eq_s2. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)