proposition: Lemma imfset_sep (T1 T2 : choiceType) (f : T1 -> T2) (A : {fset T1}) (P : pred T1) : [fset f x | x in [fset x | x in A & P x]] = [fset f x | x in A & P x].
proof: Proof. apply/fsetP => x. apply/imfsetP/imfsetP => /=. - case => x0. rewrite in_fsep => /andP [H1 H2] ->. exists x0 => //. by rewrite inE H1. - case => x0. rewrite inE => /andP [H1 H2] ->. exists x0 => //. by rewrite in_fset /= inE H1. Qed.
imports: mathcomp(all_ssreflect)