proposition: Lemma preim_vars12 (I : {set 'I_n}) (vals1 : univ_types types1) : preim_vars vars2 I (vals1to2 vals1) = preim_vars vars1 I vals1.
proof: Proof. rewrite /preim_vars. apply/setP => v. apply/preim_varsP; case: ifP => /preim_varsP /= H1. - move=> i iI; rewrite ffunE. move/H1: (iI). by case: varsE => -[f g] [/= fK gK] /(_ v) -> <-. - move=> Hv; elim: H1 => /= i iI. move/Hv: (iI); rewrite ffunE. case: varsE => -[f g] [/= fK gK] /(_ v) -> /(f_equal g). by rewrite !fK => ->. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba