rw [map_push, IH]
α : Type u
β : Type v
γ : Type w
n : Nat
x✝ : SizedArray α n
n✝ : Nat
x : SizedArray α n✝
a : α
IH : map id x = x
⊢ map id (push x a) = push x a
α : Type u
β : Type v
γ : Type w
n : Nat
x✝ : SizedArray α n
n✝ : Nat
x : SizedArray α n✝
a : α
IH : map id x = x
⊢ push x (id a) = push x a