proposition: Lemma eq_bigcup' : forall (T U : Type) (A B : set T) (F G : T -> set U), A <--> B -> (forall x, F x <--> G x) -> \bigcup_(x in A) F x <--> \bigcup_(x in B) G x.
proof: Proof. intros. eapply eq_bigcup; eauto. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)