proposition: Lemma MX_mapE (A B : UU0) (f : A -> B) : [the functor of MX] # f = M # (fun x => match x with inl y => inl y | inr y => inr (f y) end).
proof: Proof. apply: boolp.funext => m. rewrite {1}/actm /= /bindX /= [in RHS]fmapE. congr (_ _). by apply: boolp.funext; case. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib state_lib