`chars_(un)separate_string` is an automatic lemma. So no more need to include this in Section 30 on arrays of pointers.