fact: Definition preim_vars (I : {set 'I_n}) (vals : forall i, types i) := \bigcap_(i in I) finset (vars i @^-1 (vals i)).
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba