proposition: Lemma naturality_monadM : naturality M N e.
proof: Proof. move=> A B h; apply boolp.funext => m /=. by rewrite !fmapE monadMbind (compA (e B)) monadMret. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib state_lib