[Typo] Sect 9 exercise error: "'List.append_assoc' has already been declared"

[mars0i]

January 2024 FPIL sect 9--not exactly a typo, but "technical error" seems too grand.

Prove that appending lists is associative using induction on lists: theorem List.append_assoc (xs ys zs : List α) : xs ++ (ys ++ zs) = (xs ++ ys) ++ zs

List.append_assoc is defined in Basic.lean, so theorem List.append_assoc generates

error:
'List.append_assoc' has already been declared

Perhaps it's better to use a different name in the exercise. Easy enough to rename it though.