fact: Fixpoint mapM {M : Type -> Type} `{RawMonad M} {A B : Type} (f : A -> M B) (xs : list A) : M (list B) := match xs with | nil => pure nil | cons x xs' => bind (f x) (fun fx => fmap (cons fx) (mapM f xs')) end.