proposition: Lemma jcPr_fdistmap_r (A B B' : finType) (f : B -> B') (d : {fdist A * B}) (E : {set A}) (F : {set B}): injective f -> \Pr_d [E | F] = \Pr_(fdistmap (fun x => (x.1, f x.2)) d) [E | f @: F].
proof: Proof. move=> injf; rewrite /jcPr; congr (_ / _). - rewrite (@Pr_fdistmap _ _ (fun x => (x.1, f x.2))) /=; last first. by move=> [? ?] [? ?] /= [-> /injf ->]. congr (Pr _ _); apply/setP => -[a b]; rewrite !inE /=. apply/imsetP/andP. - case=> -[a' b']; rewrite inE /= => /andP[a'E b'F] [->{a} ->{b}]; split => //. apply/imsetP; by exists b'. - case=> aE /imsetP[b' b'F] ->{b}; by exists (a, b') => //; rewrite inE /= aE. by rewrite /fdist_snd fdistmap_comp (@Pr_fdistmap _ _ f) // fdistmap_comp. Qed.
imports: mathcomp(all_ssreflect ssralg matrix) mathcomp(Rstruct) Reals ssrR realType_ext Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba