simp only [foldl_eq_foldl_data]
β : Type u_1
α : Type u_2
f : β → α → β
init : β
a : α
as : List α
⊢ foldl f init { data := a :: as } 0 = foldl f (f init a) { data := as } 0
β : Type u_1
α : Type u_2
f : β → α → β
init : β
a : α
as : List α
⊢ List.foldl f init (a :: as) = List.foldl f (f init a) as