no goals
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → β → α → m β
b : β
as : List α
⊢ foldlIdxM f b as = List.foldlM (fun b p => f p.fst b p.snd) b (enum as)
rw [foldlIdxM, foldlM_eq_foldl, foldlIdx_eq_foldl_enum]