proposition: Lemma jtype_ext A B n (t1 t2 : P_ n ( A , B )) : JType.f t1 = JType.f t2 -> t1 = t2.
proof: Proof. case: t1 t2 => d1 f1 Hf1 H1 /= [] d2 f2 Hf2 H2 /= ?; 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