α : Type u_1
arr : Array α
l : List α
⊢ (Array.appendList arr l).data = arr.data ++ l
α : Type u_1
arr : Array α
l : List α
⊢ (arr ++ l).data = arr.data ++ l
rw [← appendList_eq_append]
α : Type u_1
arr : Array α
l : List α
⊢ (List.foldl (fun r v => push r v) arr l).data = arr.data ++ l
α : Type u_1
arr : Array α
l : List α
⊢ (Array.appendList arr l).data = arr.data ++ l
unfold Array.appendList
no goals
α : Type u_1
arr : Array α
l : List α
⊢ (List.foldl (fun r v => push r v) arr l).data = arr.data ++ l
induction l generalizing arr <;> simp [*]