induction x using cons_induction generalizing init with
| empty => rfl
| cons a x IH =>
  conv => lhs; dsimp [cons]
  rw [foldlMIdx_cons]
  apply bind_congr; intro b
  exact IH b
α : Type u
β : Type v
n : Nat
m : Type v → Type w
inst✝ : Monad m
f : β → α → m β
init : β
x : SizedArray α n
⊢ List.foldlM f init x.val.data = foldlMIdx (fun x => f) init x
no goals