The Coq mailing list

[marko AT ffri.hr]

Greetings,

I send this problem on this mailing list already but question was little
different:

How to compare hypotheses over subgoals?

But now I am asking: "Is it possible to compare hypotheses over subgoals?"
So is it possible in environment:

Subgoal 1:

H : x=value_1

Subgoal 2:

H : x=value_2

...

Subgoal n:

H : x=value_n

find out are all x's have the same or different values and then to apply
different tactics according of this knowledge?

I spend five (5) days to find solution but every idea failed (pattern
matching, rewriting, abstracting lemma from one subgoal and applying to
other subgoals, etc...)

Yves Bertot already answers me that he doesn’t believe I can and I'm
gratefully for the answer.

But, I need to know is it impossible for sure? Are all tactics forbid it?
Or is it maybe possible but nobody did something like that?

Please, let me know.

Thank you very much,

Marko Malikoviæ