The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

On Fri, Oct 12, 2007 at 03:59:52PM +0200, Santiago Zanella wrote:
> You can always write your own induction principle or make your goal
> stronger as Jean-Francois Monin suggested.

But a stronger induction hypothesis also makes the proof more
complicated -- perhaps not in this case, but this was a much simplified
example. The real example is already rather complicated, and I'd rather
not modify it if I don't have to. 

It just seemed to me that this might be a common pattern (where we want
to be able to make recursive calls to various subcomponents) -- but
perhaps not.

Thanks! 

Edsko