rw [mapM_empty, pure_bind]
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
x : SizedArray α n
a : α
⊢ mapM f (push empty a) = do
    let y ← mapM f empty
    let b ← f a
    pure (push y b)
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
x : SizedArray α n
a : α
⊢ mapM f (push empty a) = do
    let b ← f a
    pure (push empty b)