fact: Definition preserves {M : monad} (A B : UU0) (f : A -> M A) (g : A -> B) := forall x, (f x >>= fun y => Ret (y, g y)) = (f x >>= fun y => Ret (y, g x)).
imports: ssrmatching mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy