The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Jeff Terrell wrote:
> Does anyone know if there's a prototypical implementation of Coq that 
> would allow f to pass the guardedness checker?

There is a simple design pattern to overcome this limitation: represent 
your lists as functions over an appropriate index domain.  See Section 
8.4 of CPDT (http://adam.chlipala.net/cpdt/).

I suggested a concrete solution on coq-club when more or less the same 
question was asked a few months ago.  I didn't find the thread in a 
cursory search, but you might have more luck.