unfold foldlMIdx
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
a : α
x : SizedArray α n
⊢ foldlMIdx f init (cons a x) = do
    let b ← f 0 init a
    foldlMIdx (fun i b => f (Nat.succ i) b) b x
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
a : α
x : SizedArray α n
⊢ foldlMIdx.loop f (cons a x) 0 (_ : 0 ≤ n + 1) init = do
    let b ← f 0 init a
    foldlMIdx.loop (fun i b => f (Nat.succ i) b) x 0 (_ : 0 ≤ n) b