The Coq mailing list

["Benjamin C. Pierce" <bcpierce AT cis.upenn.edu>]

Thanks to everyone for the enlightening comments!

> The downside is that inversion terms are heavyweight, so you
> should not use it for plain inductive types for instance.

So one possible conclusion of the discussion so far could be "inversion is a 
fancier version of destruct, so if I don't care so much about the size of 
proof terms and I do care a lot about minimizing the number of tactics I have 
to explain, I should just use inversion for everything."  

I know there are some caveats to this...

  - inversion requires an identifier, so you may have to do a "remember" 
before it

  - inversion sometimes generates lots of equalities that have to be tidied 
using subst

... but are there situations where inversion doesn't work and destruct does?

     - B