titles more concise. (We usually don't need to repeat the name of a
section in the title of one of its subsections.)