proposition: Lemma naturality_monadM : naturality M N e.
proof: Proof. move=> A B h; apply funext => m /=. by rewrite !fmapE monadMbind (compA (e B)) monadMret. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib ifail_lib istate_lib