proposition: Lemma naturality : naturality [the functor of (exponential_F A \o M)] M m.
proof: Proof. exact: Exception.naturality. Qed.
imports: Param(Param) mathcomp(all_ssreflect) HB(structures) imonae_lib ihierarchy imonad_lib ifmt_lifting imonad_model