fact: Definition catMaybes {a} (l : list (Maybe a)) : list a := (fun f => fold_right f [] l) (fun mx rest => match mx with | Some x => x :: rest | None => rest end).
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