proposition: Lemma bigcup_flatten T U V A (F : T -> set U) (G : U -> set V) : \bigcup_(x in \bigcup_(y in A) F y) G x <--> \bigcup_(y in A) \bigcup_(x in F y) G x.
proof: Proof. move=> t; split=> [[x [[y [Ay Fyx]] Gxt]] | [y [Ay [x [Fyx Gxt]]]]]. by exists y; split=> //; exists x. by exists x; split=> //; exists y. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)