fact: Definition Maybe_bind {X Y} (m : Maybe X) (f : X → Maybe Y) : Maybe Y := match m with | Nothing => Nothing | Just m' => f m' end.
imports: Category.Lib Category.Theory.Coq.Functor Category.Theory.Coq.Applicative Category.Theory.Coq.Monad Category.Theory.Coq.Semigroup Category.Theory.Coq.Monoid Category.Theory.Coq.Traversable