proposition: Lemma eta1'_natural : naturality _ _ eta1'.
proof: Proof. move=> a b h; rewrite funeqE => x; apply necset_ext => /=. by rewrite free_semiCompSemiLattConvType_morE' /= image_set1. 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