fact: Fixpoint insertM {a} (P : a → a → m bool) (z : a) (l : list a) : m (list a) := match l with | nil => ret (cons z nil) | cons x xs => b <- P x z ; if (b : bool) then cons x <$> insertM P z xs else ret (cons z (cons x xs)) end.
imports: Category.Lib Category.Theory.Category Category.Theory.Functor Category.Theory.Monad Category.Instance.Coq