proposition: Lemma preim_vars_set_vals_tl (g e : {set 'I_n}) (A : prod_types types e) vals : e :&: g = set0 -> preim_vars g (set_vals A vals) = preim_vars g vals.
proof: Proof. move=> /setP eg. apply/eq_bigr => /= i ig. apply/setP => u. rewrite !inE set_vals_tl //. move: (eg i); by rewrite !inE ig andbT => ->. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba