proposition: Lemma bigcup_nil_set0 (T U : Type) (F : T -> set U) : \bigcup_(x in [::]) F x <--> set0.
proof: Proof. split; intros Hin; inv Hin; eauto. inv H. inv H0. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)