The Coq mailing list

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

Dear Coq experts,

Someone in my class asked a question about destruct vs. inversion: They can 
be described in similar terms  ("generate subgoals for each of the possible 
ways that such-and-such could have been built..."), and there are many 
situations where either can be used; so what's the actual difference?  

Does anyone have a concise, intuitive way of explaining how they overlap in 
function and how they differ, and/or a snappy characterization of when to use 
one and when the other? 

Thanks!

   - Benjamin