proposition: Lemma preim_vars_inter (e f : {set 'I_n}) vals : preim_vars (e :|: f) vals = preim_vars e vals :&: preim_vars f vals.
proof: Proof. by rewrite /preim_vars bigcap_setU. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba