proposition: Lemma type_eqP A n : Equality.axiom (@type_eq A n).
proof: Proof. case=> d1 f1 H1 [] d2 f2 H2 /=. apply: (iffP idP) => [/eqP H|[] _ -> //]. subst f2. suff ? : d1 = d2 by subst d2; congr type.mkType; exact: boolp.Prop_irrelevance. apply fdist_ext => /= a; by rewrite H1 H2. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum perm) mathcomp(matrix) mathcomp(Rstruct) Reals ssrR Reals_ext realType_ext ssr_ext ssralg_ext logb fdist proba entropy num_occ channel_code channel typ_seq