simp only [append_push]
α : Type u
x y z✝ z : Array α
c : α
IH : x ++ y ++ z = x ++ (y ++ z)
⊢ x ++ y ++ push z c = x ++ (y ++ push z c)
α : Type u
x y z✝ z : Array α
c : α
IH : x ++ y ++ z = x ++ (y ++ z)
⊢ push (x ++ y ++ z) c = push (x ++ (y ++ z)) c