The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Adam Chlipala wrote:
> Here's the code, which will probably deserve some stepping-through and 
> pondering.  The [pattern] tactic is key to abstracting some uses of [f 
> n] but not others, in a way that preserves well-typedness of the goal.

Oh, and I just noticed that the proof was depending on a hint introduced 
by [Require Import Program.], which I had there from when I was 
experimenting with [dependent destruction] (which didn't easily get the 
job done).  You could either add that import or add an extra line 
[discriminate] to the end of the proof.