The Coq mailing list

[Robin Green <greenrd AT greenrd.org>]

If I use Proof. ... Defined. to build a term, and I use inversion in
the proof, the generated proof term can be quite complicated. If I use
"info inversion" to see what tactics are being used in that proof step,
the output is quite long. So it looks like it would be a lot of work
for me to understand how the inversion tactic works in this particular
situation.

Is there any way, apart from using the simple inversion tactic, to make
the proof terms less complicated for a proof involving inversion? Or at
least, in some sense easier to work with in a subsequent proof
involving that definition?
-- 
Robin