unfold List.foldl
case cons
α : Type u
x y : Array α
b : α
bs : List α
IH : ∀ (l : List α), List.foldl (fun l a => l ++ [a]) l bs = l ++ bs
l : List α
⊢ List.foldl (fun l a => l ++ [a]) l (b :: bs) = l ++ b :: bs
case cons
α : Type u
x y : Array α
b : α
bs : List α
IH : ∀ (l : List α), List.foldl (fun l a => l ++ [a]) l bs = l ++ bs
l : List α
⊢ List.foldl (fun l a => l ++ [a]) (l ++ [b]) bs = l ++ b :: bs