The Coq mailing list

[Andrei Borac <zerosum42 AT gmail.com>]

I am a recent convert to Coq from previously having attempted to get
the hang of theorem proving in the Isabelle/HOL system.

So far I am finding that Coq is generally pleasant to use, except for
one caveat where I can't find essential functionality. I'm sure it's
there and I just don't know how to invoke it in Coq ...

Say I am trying to prove a lemma that starts with forall n a b c

How can I induct on n and make the inductive hypothesis contain forall
a b c so that I can specialize it with any a b c?

In Isabelle/HOL this was done using arbitrary: a b c, and I can't seem
to find anything similar mentioned in the Coq tactics index.

Regards,
Andrei