proposition: Lemma imset_bigcup_incl_l : forall {T U V : Type} (f : U -> V) (A : set T) (F : T -> set U), f @: (\bigcup_(x in A) F x) \subset \bigcup_(x in A) f @: F x.
proof: Proof. firstorder. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)