proposition: Lemma mem_finsupp_free_convType_mor (A B : CC) (f : A -> B) (d : {dist A}) (x : finsupp d) : f (fsval x) \in finsupp (free_convType_mor (hom_choiceType f) d).
proof: Proof. by rewrite /= supp_fsdistmap; apply/imfsetP => /=; exists (fsval x). Qed.
imports: Reals mathcomp(all_ssreflect) mathcomp(boolp classical_sets) mathcomp(finmap) infotheo(Reals_ext classical_sets_ext ssrR ssr_ext) infotheo(fdist fsdist convex necset) monae_lib HB(structures) category