have ⟨A⟩ := A
β : Type u_1
α : Type u_2
f : β → α → β
init : β
A B : Array α
⊢ foldl f init (A ++ B) 0 = foldl f (foldl f init A 0) B 0
β : Type u_1
α : Type u_2
f : β → α → β
init : β
A✝ B : Array α
A : List α
⊢ foldl f init ({ data := A } ++ B) 0 = foldl f (foldl f init { data := A } 0) B 0