no goals
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
β : Type u
f : ℕ → α → β → m β
b : β
as : List α
inst✝ : LawfulMonad m
⊢ foldrIdxM f b as = foldrM (uncurry f) b (enum as)
simp only [foldrIdxM, foldrM_eq_foldr, foldrIdx_eq_foldr_enum, uncurry]