proposition: Lemma eq_dep_Convn n (g : 'I_n -> T) (d : {fdist 'I_n}) n0 (g0 : 'I_n0 -> T) (d0 : {fdist 'I_n0}) (Hn : n = n0) (Hg : eq_rect n (fun m => 'I_m -> T) g n0 Hn = g0) (Hd : eq_rect n (fun m => {fdist 'I_m}) d n0 Hn = d0) : <|>_d g = <|>_d0 g0.
proof: Proof. refine (match Hd with erefl => _ end). refine (match Hg with erefl => _ end). refine (match Hn with erefl => _ end). reflexivity. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg fingroup perm matrix) mathcomp(mathcomp_extra boolp classical_sets Rstruct) mathcomp(ssrnum ereal) mathcomp(lra Rstruct reals) Reals ssrR Reals_ext Ranalysis_ext ssr_ext ssralg_ext logb realType_ext fdist