proposition: Lemma imfset_comp (T1 T2 T3 : choiceType) (f : T1 -> T2) (g : T2 -> T3) (A : {fset T1}) : [fset (g \o f) x | x in A] = [fset g x | x in [fset f x | x in A]].
proof: Proof. Abort. Lemma imfset1 (aT rT : choiceType) (f : aT -> rT) (z : aT) : [fset f x | x in [fset z]] = [fset f z]. Proof. apply/fsetP => x. rewrite inE. apply/imfsetP/eqP. - case => x0 /=. by rewrite inE => /eqP->. - move => ->. exists z => //. by rewrite inE. Qed.
imports: mathcomp(all_ssreflect)