proposition: Lemma fcover_imfset (J : {fset I}) F (P : pred I) : fcover [fset F i | i in J & P i]%fset = (\bigcup_(i <- J | P i) F i)%fset.
proof: Proof. apply/fsetP=> x; apply/bigfcupP/bigfcupP => [[/= t]|[i /andP[iJ Pi xFi]]]. by rewrite andbT => /imfsetP[i /= Ji -> xFi]; exists i. exists (F i) => //; rewrite andbT; apply/imfsetP; exists i => //=. by rewrite inE Pi andbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)