proposition: Lemma cover_imset J F : cover (F @: J) = \bigcup_(i in J) F i.
proof: Proof. apply/setP=> x. apply/bigcupP/bigcupP=> [[_ /imsetP[i Ji ->]] | [i]]; first by exists i. by exists (F i); first apply: imset_f. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)