induction x using cons_induction generalizing β f init with
| empty =>
  conv =>
    lhs; unfold foldlMIdx; unfold foldlMIdx.loop
    rw [dif_neg (by decide : 0 ≠ 0+1)]
    change f 0 init a >>= foldlMIdx.loop f (push empty a) 1 (.refl)
    rhs; ext; unfold foldlMIdx.loop; rw [dif_pos rfl]
  conv => rhs; rw [foldlMIdx_empty, pure_bind]
  rw [bind_pure]
| cons a₁ x IH =>
  rw [push_cons_eq_cons_push]
  simp only [foldlMIdx_cons f init a₁]
  rw [bind_assoc]
  apply bind_congr; intro b
  exact IH ..
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
x : SizedArray α n
a : α
⊢ foldlMIdx f init (push x a) = do
    let b ← foldlMIdx f init x
    f n b a
no goals