proposition: Lemma typed_tuples_are_typ_seq : (@row_of_tuple A n @: T_{ P }) \subset `TS P n 0.
proof: Proof. apply/subsetP => t Ht. rewrite /set_typ_seq inE /typ_seq tuple_dist_type_entropy; last first. case/imsetP : Ht => x Hx ->. by rewrite row_of_tupleK. by rewrite addR0 subR0 lexx. 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