proposition: Lemma preim_prod_vars (g : {set 'I_n}) (C : prod_types types g) vals : finset (prod_vars g @^-1 C) = preim_vars g (set_vals C vals).
proof: Proof. apply/setP => x; rewrite !inE. apply/esym/preim_varsP; case: ifP. - move/eqP => <- i ig. by rewrite set_vals_prod_vals // ffunE. - move/negP => /= Hf Hcap; elim: Hf. apply/eqP/ffunP => /= i. rewrite /prod_vars (prod_vals_eq (vals2:=set_vals C vals)). by rewrite prod_vals_set_vals. rewrite ffunE; exact: Hcap. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba