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