proposition: Lemma MS_mapE (A B : UU0) (f : A -> B) (m : MS A) : ([the functor of MS] # f) m = (M # (fun x => (f x.1, x.2))) \o m.
proof: Proof. apply funext=> s. rewrite {1}/actm /= /bindS /= fmapE. congr bind. by apply: funext; case. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib ifail_lib istate_lib