rw [foldl_eq_foldl_data']
α : Type u
x y : Array α
⊢ (foldl (fun r v => push r v) x y 0 (size y)).data = x.data ++ y.data
α : Type u
x y : Array α
⊢ (List.foldl (fun r v => push r v) x y.data).data = x.data ++ y.data