exact foldlM_eq_foldlM_data'.aux f arr arr.size 0 rfl init
α : Type u
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
f : β → α → m β
init : β
arr : Array α
⊢ foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) (size arr) 0 init = List.foldlM f init arr.data
no goals