The Coq mailing list

[Kirill Taran <kirill.t256 AT gmail.com>]

Hello,

I am trying to craft custom induction principle.
Its purpose is to solve such problem:

...
case Eq_x_y: (x == y).
+ (* 1 *) by ... . (* can be done *)
+ (* 2 *) by ... . (* I want to have induction hypothesis here *)
...

Branch 1 can be solved easily with hypothesis "(x == y) = true" while
branch 2 requires additional hypothesis of the type "forall x y, (x == y) = true -> P x y".

I wanted to create custom boolean induction principle but got stuck.
Has anybody idea how to do it?

Sincerely,
Kirill Taran