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