proposition: Lemma prod_vars1 (i : 'I_n) : RV_equiv (prod_vars [set i]) (vars i).
proof: Proof. exists ((fun A : prod_types types [set i] => set_vals A vals0 i), prod_vals [set i] \o set_val (i:=i) ^~ vals0). split => x /=. apply/ffunP => /= j. apply (set_vals_inj (vals := vals0)). case/boolP: (j \in [set i]) => Hj; last by rewrite !set_vals_tl. rewrite set_vals_prod_vals //. rewrite inE in Hj. move/eqP: Hj (set_vals _ _) => -> v. by rewrite set_val_hd. by rewrite set_vals_prod_vals ?inE // set_val_hd. move=> u /=. by rewrite set_vals_prod_vars // inE. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba