induction l' generalizing l with
| nil => exact Eq.symm $ l.append_nil
| cons b bs IH =>
  unfold List.foldl; rw [IH]; exact Eq.symm $ l.append_cons b bs
α : Type u
x y : Array α
l l' : List α
⊢ List.foldl (fun l a => l ++ [a]) l l' = l ++ l'
no goals