proposition: Lemma bigcup_imset T U V (f : T -> U) A (F : U -> set V) : \bigcup_(y in f @: A) (F y) <--> \bigcup_(x in A) F (f x).
proof: Proof. by rewrite bigcup_flatten; apply: eq_bigcupr => x; rewrite bigcup_set1. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)