proposition: Lemma incl_bigcup_list_hd (T U : Type) (h : T) (t : list T) (G : T -> set U) s : s \subset G h -> s \subset \bigcup_(x in h :: t) G x.
proof: Proof. intros Hyp x Hin. eapply Hyp in Hin. eexists. split. now left. eauto. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)