proposition: Lemma disjoint_preim_vars (e f : {set 'I_n}) (A B : prod_types types f) vals : f \subset e -> A != B -> [disjoint preim_vars e (set_vals A vals) & preim_vars e (set_vals B vals)].
proof: Proof. move=> fe AB. rewrite -setI_eq0. apply/eqP/setP => u. rewrite !inE. apply/negP => /andP [] /preim_varsP /= HA /preim_varsP /= HB. case: (prod_types_neq AB) => /= i /andP [Hif HAB]. have ie : i \in e by move/subsetP: fe; apply. move/(_ _ ie)/eqP: HB. rewrite HA // set_vals_eq => /orP [] H. - by rewrite H in HAB. - by rewrite Hif in H. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba