The common structure of the rules of the type formers can be captured by a general schema for inductive definitions (Dybjer 1991). This general schema has many useful instances, for example, the type \(\List(A)\) of lists with elements of type \(A\) has the following introduction rules: