proposition: Lemma free_choiceType_mor_comp_fun (a b c : Type) (g : {hom b, c}) (h : {hom a, b}): free_choiceType_mor [hom g \o h] = (free_choiceType_mor g) \o (free_choiceType_mor h) :> (_ -> _).
proof: Proof. by rewrite free_choiceType_mor_comp. 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