This chapter describes how you can construct predicate and data-types inductively. This correspond traditionnally to the definition of a set as the smallest set such that ...
This kind of definitions are not to difficult to write by hand, but they are not very readable and moreover, you need to prove many lemmas before using them. will generate and prove automatically these lemmas (most of the time)