simp only [foldlMIdx_cons f init a₁]
case cons
α : Type u
β✝ : Type v
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
n✝ : Nat
a₁ : α
x : SizedArray α n✝
IH :
  ∀ {β : Nat → Type v} (f : (i : Nat) → β i → α → m (β (i + 1))) (init : β 0),
    foldlMIdx f init (push x a) = do
      let b ← foldlMIdx f init x
      f n✝ b a
β : Nat → Type v
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
⊢ foldlMIdx f init (cons a₁ (push x a)) = do
    let b ← foldlMIdx f init (cons a₁ x)
    f (n✝ + 1) b a
case cons
α : Type u
β✝ : Type v
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
n✝ : Nat
a₁ : α
x : SizedArray α n✝
IH :
  ∀ {β : Nat → Type v} (f : (i : Nat) → β i → α → m (β (i + 1))) (init : β 0),
    foldlMIdx f init (push x a) = do
      let b ← foldlMIdx f init x
      f n✝ b a
β : Nat → Type v
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
⊢ (do
      let b ← f 0 init a₁
      foldlMIdx (fun i b => f (Nat.succ i) b) b (push x a)) =
    do
    let b ←
      do
        let b ← f 0 init a₁
        foldlMIdx (fun i b => f (Nat.succ i) b) b x
    f (n✝ + 1) b a