fact: Fixpoint mapT_list@{} (ls : list A) : F (list B) := match ls with | nil => pure nil | l :: ls => ap (ap (pure (@cons B)) (f l)) (mapT_list ls) end.
imports: Coq.Lists.List ExtLib.Core.RelDec ExtLib.Structures.Monoid ExtLib.Structures.Reducible ExtLib.Tactics.Consider ExtLib.Tactics.Injection ExtLib.Structures.Traversable ExtLib.Structures.Functor ExtLib.Structures.Monads ExtLib.Structures.Applicative