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