We have already seen the type of natural numbers and the type of well-founded trees as examples of types given by inductive definitions; the natural numbers is an example of an ordinary finitary inductive definition and the well-founded trees of a generalized possibly infinitary inductive definition. The introduction rules describe how elements of these types are inductively generated and the elimination and equality rules describe how functions from these types can be defined by structural recursion on the way these elements are generated. According to the propositions as types principle, the elimination rules are simultaneously rules for proof by structural induction on the way the elements are generated.