proposition: Lemma incl_bigcup_list_tl_inter {T U : Type} (h : T) (t : list T) (G : T -> set U) s S : s \subset S :&: (\bigcup_(x in t) G x) -> s \subset S :&: (\bigcup_(x in h :: t) G x).
proof: Proof. intros Hyp x Hin. eapply Hyp in Hin. inv Hin. inv H0. inv H1. split. eassumption. eexists. split. now right; eauto. eauto. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)