Nested datatypes (R. Bird et al) are families of datatypes that are indexed over all types such that the constructors may relate different family members (unlike the homogeneous lists). Moreover, even the family name may be involved in the expression that gives the index the argument type of the constructor refers to. Especially in this case, termination of functions that traverse these data structures is far from being obvious.
A joint article with A. Abel and T. Uustalu (TCS 333(1-2), pp. 3-66, 2005) proposes iteration schemes that guarantee termination not by structural requirements but just by polymorphic typing.
However, there have not been induction principles for the verification of the programs thus obtained. In the framework of intensional type theory, i.e. the Calculus of Inductive Constructions that underlies Coq, these principles are now derived for a representation of nested datatypes that makes use of the concept of simultaneous inductive-recursive definitions (P. Dybjer). The whole construction together with extended examples has been carried out in Coq.