proposition: Lemma cinde_preim_equiv1 (I J K : {set 'I_n}) : cinde_preim vars2 I J K -> cinde_preim vars1 I J K.
proof: Proof. rewrite /cinde_preim => CI vals1. move: (CI (vals1to2 vals1)). by rewrite !preim_vars12. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba