rw [← y.data.foldl_hom Array.data Array.push (λ l a => l ++ [a]) x λ arr a => (arr.push_data a).symm]
α : Type u
x y : Array α
⊢ (List.foldl (fun r v => push r v) x y.data).data = x.data ++ y.data
α : Type u
x y : Array α
⊢ List.foldl (fun l a => l ++ [a]) x.data y.data = x.data ++ y.data