proposition: Lemma fsval_free_convType_mor_supp (A B : choiceType) (f : {hom A , B}) d i : fsval (free_convType_mor_supp f d i) = f (fsval i).
proof: Proof. by case: i. 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