proposition: Lemma incl_bigcup a b (x:a) (A : set a) (f:a->set b) : x \in A -> f x \subset \bigcup_(x in A) f x.
proof: Proof. rewrite /set_incl /bigcup. by eauto 3. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)