proposition: Lemma MC_mapE (A B : UU0) (f : A -> B) (m : MC A) : ([the functor of MC] # f) m = fun k : B -> M r => m (k \o f).
proof: Proof. by []. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib ifail_lib istate_lib