proposition: Lemma pr_mem mu (r : seq T) : uniq r -> \P_[mu] [pred x | x \in r] = \sum_(x <- r) mu x.
proof: Proof. elim: r => [_|y r ih]; first by rewrite big_nil pr_pred0_eq //. case/andP=> yNr /ih {ih}h; rewrite big_cons /= pr_pred1. by rewrite -h -pr_or_indep // => x /eqP ->. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum