proposition: Lemma cpr_inE' (U : finType) (P : {fdist U}) (A B : finType) (X : {RV P -> A}) (Y : {RV P -> B}) (E : {set A}) (F : {set B}) : `Pr[ X \in E | Y \in F ] = `Pr_(`p_ [% X, Y]) [E `*T | T`* F].
proof: Proof. rewrite cpr_eq_setE /cPr /dist_of_RV; congr (_ / _). rewrite setTE EsetT setIX setIT setTI. by rewrite Pr_fdistmap_RV2. by rewrite setTE Pr_fdistmap_RV2; congr Pr; apply/setP => u; rewrite !inE. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct reals) Reals Lra ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist