proposition: Lemma Pr_jcPr_unit (A : finType) (E : {set A}) (P : {fdist A}) : Pr P E = \Pr_(fdistmap (fun a => (a, tt)) P) [E | setT].
proof: Proof. rewrite /jcPr (Pr_set1 _ tt). rewrite (_ : _`2 = fdist1 tt) ?fdist1xx ?divR1; last first. rewrite /fdist_snd fdistmap_comp; apply/fdist_ext; case. by rewrite fdistmapE fdist1xx (eq_bigl xpredT) // FDist.f1. rewrite /Pr big_setX /=; apply eq_bigr => a _; rewrite (big_set1 _ tt) /=. rewrite fdistmapE (big_pred1 a) // => a0; rewrite inE /=. by apply/eqP/eqP => [[] -> | ->]. Qed.
imports: mathcomp(all_ssreflect ssralg matrix) mathcomp(Rstruct) Reals ssrR realType_ext Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba