simp only [foldlM, Nat.le_refl, dif_pos, Nat.sub_zero]
α : Type u
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
f : β → α → m β
init : β
arr : Array α
⊢ foldlM f init arr 0 (size arr) = List.foldlM f init arr.data
α : 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