The applications of K in chapter 17 were discovered after the invention of mice, whereas K was designed with the covering lemma in mind. Much of the motivation for this part was discussed in the introduction. The historical notes to chapters 18 and 19 discuss the connection between the proof given here and the proof originally discovered.

Chapter 18 opens with a summary of the proof. The reader is strongly urged to consult the proof for L at this point: for although a proof for L is embedded in our proof it can be substantially simplified. As we have said, we are concerned not to abridge proofs to such an extent that important techniques are lost, provided that it seems that those techniques show off the structure of K in an important way. It may well be that fine structure could be done without in this proof; we have explained why it is used here in the introduction. Chapter 18 is mainly occupied with a technical property called goodness; the reader who is unfamiliar with covering lemma proofs would be wise to take goodness on faith.

Chapter 19 proves the covering lemma. Up to the case where CN is infinite the proof is very similar to the proof in L, but a mucky argument is needed to settle this final case. The muck intensifies in chapter 20 when we extract a Prikry sequence from this final case and obtain a covering lemma on the assumption −0†.

The pace relaxes in chapter 21 and there is no fine-structure in the discussion of SCH or patterns of indiscernibles that it contains.