apply bind_congr
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f✝ : Fin (n + 1) → α → m β
x : SizedArray α n
a : α
f : Fin (0 + 1) → α → m β
⊢ (do
      let __do_lift ← f 0 (push empty a)[0]
      mapMIdx.loop f (push empty a) (0 + 1) (_ : 0 < 0 + 1) (push (mkEmpty (0 + 1)) __do_lift)) =
    do
    let b ← f 0 a
    pure (push (mkEmpty 0) b)
case h
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f✝ : Fin (n + 1) → α → m β
x : SizedArray α n
a : α
f : Fin (0 + 1) → α → m β
⊢ ∀ (a_1 : β),
    mapMIdx.loop f (push empty a) (0 + 1) (_ : 0 < 0 + 1) (push (mkEmpty (0 + 1)) a_1) = pure (push (mkEmpty 0) a_1)