proposition: Lemma bigcup_pointwise_incl A B (s : set A) (t : A -> set B) (u : set B) : (forall x, x \in s -> t x \subset u) -> \bigcup_(x in s) t x \subset u.
proof: Proof. intros H b [x []]; eapply H; eauto. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)