proposition: Lemma naturality_ret : hierarchy.naturality _ _ ret_.
proof: Proof. by move=> ? ? ?; rewrite (category.natural (@category.ret _ M)). Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib HB(structures) hierarchy