Ssreflect Users Discussion List

["John Wiegley" <>]

>>>>> Enrico Tassi <> writes:

>> Is there a way of combining [elim] with a hand-made induction principle, as
>> in [induction x using my_ind]?

> This way

>   elim/my_ind: x.

Depending on your induction principle, there are some further syntactic
variations that may help.  See page 50 of the manual, in the section entitled
"Interpreting eliminations".

John