proposition: Lemma incl_bigcup_compat_list_inter (T U : Type) (h1 h2 : T) (t1 t2 : seq T) (F G : T -> set U) S : S :&: F h1 \subset S :&: G h2 -> S :&: \bigcup_(x in t1) F x \subset S :&: \bigcup_(x in t2) G x -> S :&: \bigcup_(x in (h1 :: t1)) F x \subset S :&: \bigcup_(x in (h2 :: t2)) G x.
proof: Proof. intros Hs1 Hs2. intros x Hin. inv Hin. constructor; eauto. inv H0. inv H1. inv H2. - eexists. split. now left. eapply Hs1. split; eauto. - edestruct Hs2. split. eassumption. eexists. split; eauto. destruct H6. destruct H6. eexists. split. right; eauto. eassumption. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)