simp only [foldl_eq_foldl_data, append_data]
β : Type u_1
α : Type u_2
f : β → α → β
init : β
A✝ B✝ : Array α
A B : List α
⊢ foldl f init ({ data := A } ++ { data := B }) 0 = foldl f (foldl f init { data := A } 0) { data := B } 0
β : Type u_1
α : Type u_2
f : β → α → β
init : β
A✝ B✝ : Array α
A B : List α
⊢ List.foldl f init (A ++ B) = List.foldl f (List.foldl f init A) B