The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

Christine's answer is fine.  I would just like to correct the 
bibliographic reference, the paper
at TLCA  in 2005, not 1995.

Also, you can find the Coq example at

ftp://ftp-sop.inria.fr/lemme/Yves.Bertot/filters.tar.gz

Another example is also given in the Coq'Art book, Section 15.4 (pp.  
427-431
yes, it's marked with 3 stars, considered extremely difficult).

The Coq source for this example is on the book's website:

http://www.labri.fr/perso/casteran/CoqArt/gen-rec/SRC/chap15.v

lines 241-322

You can also look at the exercise 15.20, also an extremely difficult one 
but it's correction
is also on the book's website.