proposition: Lemma domm_fset_to_chset {T}: cancel (@fset_to_chset T) (@domm T 'unit).
proof: Proof. move=> [m Hm] /=. apply: fsval_eq. have H: (fst \o pair^~ tt =1 id) => //. by rewrite /fset_to_chset val_domm mkfmapK /unzip1 -map_comp (eq_map (H T)) map_id. Qed.
imports: Relational(OrderEnrichedCategory GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr realsum ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq) Mon(SPropBase) Crypt(Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb pkg_core_definition choice_type pkg_composition pkg_rhl Package Prelude) extructures(ord fset fmap) Equations(Equations)