The Coq mailing list

[Adam Megacz <megacz AT cs.berkeley.edu>]

Aaron Bohannon 
<bohannon AT cis.upenn.edu>
 writes:
> It seems like something must be wrong here.  Is there something I
> should be using instead of "inversion H; congruence"?

If "destruct H" gives you the hypotheses you need (it doesn't always),
you might try using it instead of inversion.  At least for me it speeds
things up dramatically.

  - a