proposition: Lemma MEnv_mapE (A B : UU0) (f : A -> B) (m : MEnv A) : (MEnv # f) m = (M # f) \o m.
proof: Proof. by apply: funext => r; rewrite /= fmapE. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib ifail_lib istate_lib