no goals
α : Type u_1
as : List α
acc : Array α
⊢ (List.toArrayAux as acc).data = acc.data ++ as
induction as generalizing acc <;> simp [*, List.toArrayAux, Array.push, List.append_assoc, List.concat_eq_append]