proposition: Lemma in_bigcup_list_hd (T U : Type) (h : T) (t : seq T) (G : T -> set U) (z : U) : G h z -> (\bigcup_(x in (h :: t)) G x) z.
proof: Proof. intros Hin. eapply incl_bigcup_list_hd. now eapply subset_refl. eassumption. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)