proposition: Lemma bigcup_codom T U V (f : T -> U) (F : U -> set V) : \bigcup_(y in codom f) (F y) <--> \bigcup_x F (f x).
proof: Proof. by rewrite -imsetT bigcup_imset. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)