proposition: Lemma bigfcup_imfset1 (I T : choiceType) (P : {fset I}) (f : I -> T) : \bigcup_(i <- P) [fset f i] = f @` P.
proof: Proof. apply/eqP; rewrite eqEfsubset; apply/andP; split; apply/fsubsetP => x. - by case/bigfcupP=> i /andP [] iP _; rewrite inE => /eqP ->; apply/imfsetP; exists i. - case/imfsetP => i /= iP ->; apply/bigfcupP; exists i; rewrite ?andbT //. by apply/imfsetP; exists (f i); rewrite ?inE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)