proposition: Lemma incl_bigcup_list_nil (T U : Type) (G : T -> set U) s : \bigcup_(x in [::]) G x \subset s.
proof: Proof. intros x Hin. inv Hin. inv H. inv H0. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)