Use coqdoc's header feature to make it easier to find key concepts and
improve/tweak a few comments.