proposition: Lemma pr_bigor_indep mu (P : I -> pred T) (r : seq I) : uniq r -> (forall p1 p2 x, p1 != p2 -> p1 \in r -> p2 \in r -> x \in P p1 -> x \notin P p2) -> \P_[mu] [pred x | has [pred p | x \in P p] r] = \sum_(p <- r) \P_[mu] (P p).
proof: Proof. move=> uq_r dj; pose S x := \big[orb/false]_(p <- r) (x \in P p). rewrite (eq_pr (B := S)) => [x|]; first by rewrite !inE -big_has. rewrite {}/S; elim: r uq_r dj => [_|p r ih /andP[pNr /ih {ih}h]] dj. by rewrite big_nil pr_pred0_eq // => x; rewrite big_nil. rewrite big_cons -h => [p1 p2 x ne_p p1r p2r|]. by apply/dj=> //; rewrite in_cons (p1r, p2r) orbT. rewrite -pr_or_indep => [x xNPp|]. rewrite -topredE /= big_has; apply/hasPn => y y_in_r. apply/(dj p); rewrite ?in_cons ?(eqxx, y_in_r, orbT) //. by apply/contra: pNr=> /eqP->. by apply/eq_pr=> x; rewrite -!topredE /= big_cons. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum