proposition: Lemma imset_bigcup_setI_cons_subset_r : forall (A B : Type) (l : A) (ls : seq A) (f : A -> set (option B)) (s1 s2 : set B) (s3 : set A), s3 l -> Some @: s1 \subset f l -> Some @: s2 \subset \bigcup_(x in ls :&: s3) f x -> Some @: (s1 :|: s2) \subset \bigcup_(x in (l :: ls) :&: s3) f x.
proof: Proof. intros A B l ls f s1 s2 s3 H1 H2 H3. rewrite imset_union_set_eq. apply setU_l_subset. - intros x Hs1. eexists l; split; eauto. split; eauto. left; eauto. - intros x Hs1. eapply H3 in Hs1. edestruct Hs1 as [x' [[Hs3 Hls] Hin]]. eexists x'; split; eauto. split; eauto. right; eauto. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)