generalize x.data = l
α : Type u
x y : Array α
⊢ List.foldl (fun l a => l ++ [a]) x.data y.data = x.data ++ y.data
α : Type u
x y : Array α
l : List α
⊢ List.foldl (fun l a => l ++ [a]) l y.data = l ++ y.data