proposition: Lemma preim_vars_vals (e : {set 'I_n}) (A : prod_types types e) vals1 vals2 : (forall x, x \in e -> vals1 x = vals2 x) -> preim_vars e vals1 = preim_vars e vals2.
proof: Proof. move=> Hvals. apply/eq_bigr => /= i ie. apply/setP => u; by rewrite !inE Hvals. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba