proposition: Lemma free_semiCompSemiLattConvType_morE (X : acto A) : NECSet.mixinType (free_semiCompSemiLattConvType_mor X) = image_neset f X.
proof: Proof. by rewrite /free_semiCompSemiLattConvType_mor; unlock; apply neset_ext. 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