proposition: Lemma cinde_preim_equiv (types1 types2 : 'I_n -> finType) (vars1 : forall i : 'I_n, {RV P -> types1 i}) (vars2 : forall i : 'I_n, {RV P -> types2 i}) I J K : (forall i : 'I_n, RV_equiv (vars1 i) (vars2 i)) -> cinde_preim vars1 I J K <-> cinde_preim vars2 I J K.
proof: Proof. split; apply cinde_preim_equiv1 => // i; by apply RV_equivC. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba