fact: Fixpoint replicateM_ (n : nat) (x : m ()) : m () := match n with | O => ret tt | S n' => x >> replicateM_ n' x end.
imports: Category.Lib Category.Theory.Category Category.Theory.Functor Category.Theory.Monad Category.Instance.Coq