The Coq mailing list

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

Hi,

Thanks for all the replies! Sometimes I get slightly confused about the
difference between inversion (which does not give you the induction
hypothesis) and induction (which does give you the induction hypothesis,
but is a pain to use if the arguments to the inductive properties aren't
variables). The general suggestion of using induction to prove that
something must hold, and then use inversion to show that it doesn't is
indeed very useful.

Thanks!

Edsko