proposition: Lemma bigcup_cons_subset {A B} l (ls : seq A) (f : A -> set B) s : f l \subset s -> \bigcup_(x in ls) (f x) \subset s -> \bigcup_(x in l :: ls) (f x) \subset s.
proof: Proof. intros H1 H2 x [y [Hl Hr]]. inv Hl. - eauto. - eapply H2. eexists; split; eauto. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)