proposition: Lemma eq_bigjoin r : r != [::] -> {x : T | x \in r & (\join_(i <- r) F i)%O == F x}.
proof: Proof. by case: r => // x r _; case: bigjoinP => // y y_in_r; exists y. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset order) mathcomp(ssralg)