proposition: Lemma eq_bigcupl T U A B (F : T -> set U) : A <--> B -> \bigcup_(x in A) F x <--> \bigcup_(x in B) F x.
proof: Proof. by move=> /subset_eqP[? ?]; split; apply: incl_bigcupl. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)