The Coq mailing list

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

On 12/14/2012 10:33 AM, Harley D. Eades III wrote:
> A while ago I formalized some of my research on the hereditary substitution
> function in Coq.  At first I tried to define the function in Set using 
> Program Fixpoint
> and the wf annotation.  I was able to define the function and satisfy all the 
> obligations.
> However, I can't compute with it.  Even worse the subgoals generated are 
> huge.  They
> are over 1000 lines long.
>    

Chapter 7 of CPDT <http://adam.chlipala.net/cpdt/> may be of interest.  
It surveys a variety of techniques for general recursion in Coq (not 
including Program, which I've never gotten into, partly because of the 
issues you mention).