proposition: Lemma bigcup_set0 T U (F : T -> set U) : \bigcup_(x in set0) F x <--> set0.
proof: Proof. by move=> t; split=> // [[? []]]. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)