apply bind_congr
α : 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
⊢ (do
      let __do_lift ← f 0 init (cons a x)[0]
      foldlMIdx.loop f (cons a x) (0 + 1) (_ : 0 < n + 1) __do_lift) =
    do
    let b ← f 0 init a
    foldlMIdx.loop (fun i b => f (Nat.succ i) b) x 0 (_ : 0 ≤ n) b
case h
α : 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
⊢ ∀ (a_1 : β (0 + 1)),
    foldlMIdx.loop f (cons a x) (0 + 1) (_ : 0 < n + 1) a_1 =
      foldlMIdx.loop (fun i b => f (Nat.succ i) b) x 0 (_ : 0 ≤ n) a_1