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