The Coq mailing list

[Marko Malikovi� <marko AT ffri.hr>]

Greetings,

Is there some contribution about tactics for solving first order formulae
but with mixed inductive types?
For example, to prove this:

Section Proba.

Inductive tip : Set := a | b | c | d | e.

Hypothesis H : a=b \/ 3=4.

Parameter goal : Prop.

Goal goal.

I have to destruct hypothesis H but it is embarrassingly sometimes (if I
have long hypotheses).

Thank you very much,

Marko Malikoviæ