fact: Definition forFoldrM `{Monad m} {A B : Type} (s : A) (l : list B) (f : B → A → m A) : m A := foldrM f s l.
imports: Coq.Lists.List Equations(Equations) Equations.Type.EqDec Category.Lib Category.Theory.Coq.Functor Category.Theory.Coq.Applicative Category.Theory.Coq.Monad Category.Theory.Coq.Maybe Coq.Lists.List