proposition: Lemma bigcup_of_const (P : set U) (X : U -> set T) (i : U) : P i -> (forall j, P j -> X j = X i) -> \bigcup_(j in P) X j = X i.
proof: Proof. move=> Pi H; rewrite eqEsubset; split=> a; by [case=> j /H -> | exists i]. Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp classical_sets)