proposition: Lemma joins_setU I (A B : {set I}) (F : I -> L) : \join_(i in (A :|: B)) F i = \join_(i in A) F i `|` \join_(i in B) F i.
proof: Proof. rewrite -!big_enum; have /= <- := @big_cat _ _ join. apply/eq_big_idem; first exact: joinxx. by move=> ?; rewrite mem_cat !mem_enum inE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)