proposition: Lemma jtype_eqP A B n : Equality.axiom (@jtype_eq A B n).
proof: Proof. case=> d1 f1 Hf1 H1 [] d2 f2 Hf2 H2 /=. apply: (iffP idP) => [/eqP H |[] _ -> //]. subst f2. have ? : d1 = d2. apply/Channel1.chan_star_eq. by rewrite boolp.funeqE => a /=; apply/fdist_ext => b; rewrite H1 H2. subst d2; congr JType.mk; exact/boolp.Prop_irrelevance. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum fingroup perm) Reals mathcomp(Rstruct) ssrR Reals_ext realType_ext ssr_ext ssralg_ext logb fdist entropy num_occ channel types