proposition: Lemma bigcup_set0_r (T U : Type) (s : set T) (F : T -> set U) : (forall x, F x <--> set0) -> \bigcup_(x in s) F x <--> set0.
proof: Proof. firstorder. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)