simp [mkArray_data, List.replicate]
case h
α : Type u_1
n : Nat
a : α
⊢ (mkArray (n + 1) a).data = (push (mkArray n a) a).data
case h
α : Type u_1
n : Nat
a : α
⊢ a :: List.replicate n a = List.replicate n a ++ [a]