proposition: Lemma incl_bigcupr T U A (F : T -> set U) G : (forall x, F x \subset G x) -> \bigcup_(x in A) F x \subset \bigcup_(x in A) G x.
proof: Proof. by move=> subFG t [x [Ax Fxt]]; exists x; split=> //; apply: subFG. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)