proposition: Lemma pr_eq_pair_setT (U : finType) (P : {fdist U}) (A B : finType) (E : {set A}) (X : {RV P -> A}) (Y : {RV P -> B}) : `Pr[ [% X, Y] \in E `*T ] = `Pr[ X \in E ].
proof: Proof. apply/esym. rewrite (@pr_in_comp _ _ _ _ _ (fun a => (a, tt))); last by move=> u1 u2 -[]. rewrite 2!pr_eq_setE; congr Pr; apply/setP => u; rewrite !inE /=. by apply/imsetP/idP => [[a aE [] ->//]|XuE]; exists (X u). 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