proposition: Lemma uniq_flatten_map x y l : has (mem (f x)) (f y) -> uniq (flatten (map f l)) -> x \in l -> y \in l -> x = y.
proof: Proof. move/hasP => [b Hby Hbx]. elim: l => // a l IH. rewrite !in_cons /= cat_uniq => /andP/proj2/andP[Hun1 Hun2] /orP[] Hx /orP[] Hy. - by rewrite (eqP Hx) (eqP Hy). - move/hasP: Hun1; elim. exists b. apply/flattenP. by exists (f y) => //; exact/map_f. by rewrite -(eqP Hx). - move/hasP: Hun1; elim. exists b. apply/flattenP. by exists (f x) => //; exact/map_f. by rewrite -(eqP Hy). - by apply IH. Qed.
imports: mathcomp(all_ssreflect fingroup perm)