proposition: Lemma bigcup_cons_subset_r : forall (A B : Type) (l : A) (ls : seq A) (f : A -> set B) (s1 s2 : set B), s1 \subset f l -> s2 \subset \bigcup_(x in ls) f x -> s1 :|: s2 \subset \bigcup_(x in (l :: ls)) f x.
proof: Proof. intros A B l ls f s1 s2 H1 H2. apply setU_l_subset. - rewrite bigcup_setU_l bigcup_set1. eapply setU_subset_l. eassumption. - rewrite bigcup_setU_l bigcup_set1. eapply setU_subset_r. eassumption. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)