proposition: Lemma Pr_preim_vars_sub (e f : {set 'I_n}) (vals : univ_types types) : f \subset e -> Pr P (preim_vars (e :\: f) vals) = \sum_(A : Tfin_img (prod_vars f)) Pr P (preim_vars e (set_vals (nth_fin_img A) vals)).
proof: Proof. rewrite /Pr => fe. rewrite -partition_disjoint_bigcup; last first. move=> /= A B. rewrite -(tnth_uniq A B (t:=in_tuple _)) ?undup_uniq => // AB. exact: disjoint_preim_vars. apply/eq_bigl => u. apply/esym/bigcupP/(equivPif idP). move=> [A _ /preim_varsP HA]. apply/preim_varsP => /= i /setDP [/HA -> Hif]. by rewrite set_vals_tl. move=> /= /preim_varsP /= Hu. exists (map_fin_img (prod_vars f) u) => //. apply/preim_varsP => /= i ie. case/boolP: (i \in f) => Hif. by rewrite nth_fin_imgK set_vals_prod_vars. by rewrite set_vals_tl // Hu // inE Hif. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba