proposition: Lemma cinde_events_vals : [forall i in (e :&: g), set_vals C vals0 i == set_vals A vals0 i] \/ cinde_events P (finset (prod_vars e @^-1 A)) (finset (prod_vars f @^-1 B)) (finset (prod_vars g @^-1 C)).
proof: Proof. case /boolP: [forall i in (e :&: g), _]. by left. rewrite negb_forall => /existsP [i]. rewrite inE negb_imply => /andP [] /andP [Hie Hig] /eqP Hvi. right; rewrite /cinde_events. rewrite (proj2 (cPr_eq0 _ _ _)); last first. apply/Pr_set0P => u; rewrite !inE => Hprod; elim: Hvi. case/andP: Hprod => /andP[] /eqP <- _ /eqP <-; exact: prod_vars_inter. rewrite (proj2 (cPr_eq0 _ _ _)) ?mul0R //. apply/Pr_set0P => u; rewrite !inE => Hprod; elim: Hvi. case/andP: Hprod => /eqP <- /eqP <-; exact: prod_vars_inter. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba