proposition: Lemma RetE T : (Ret : idfun T -> N T) = (Ret : FId T -> M T).
proof: Proof. apply funext => t /=. rewrite /ret_. rewrite [in LHS]/=. by rewrite HCompId HIdComp [X in _ (X t)]/= eta0E etaCE. 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 hierarchy