proposition: Lemma eq_bigcupr T U A (F : T -> set U) G : (forall x, F x <--> G x) -> \bigcup_(x in A) F x <--> \bigcup_(x in A) G x.
proof: Proof. by move=> eq_FG t; split; apply: incl_bigcupr => {t} x t; rewrite (eq_FG x t). Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)