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