exact Eq.symm $ l.append_cons 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 α
⊢ l ++ [b] ++ bs = l ++ b :: bs
no goals