All the material for this topic is contained in the Induction and Lists chapters of Software Foundations.