rw [map_push, mapM_push, IH]
α : Type u
β : Type v
γ : Type w
n : Nat
f : α → β
x✝ : SizedArray α n
n✝ : Nat
x : SizedArray α n✝
a : α
IH : map f x = mapM f x
⊢ map f (push x a) = mapM f (push x a)
α : Type u
β : Type v
γ : Type w
n : Nat
f : α → β
x✝ : SizedArray α n
n✝ : Nat
x : SizedArray α n✝
a : α
IH : map f x = mapM f x
⊢ push (mapM f x) (f a) = do
    let y ← mapM f x
    let b ← f a
    pure (push y b)