The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

S3 wrote:
> How do you have induction over a data structure
> that contains a list?

This is a genuine Frequently Asked Question, and it's addressed in 
Section 3.8 of CPDT:
    http://adam.chlipala.net/cpdt/