The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

marko AT ffri.hr
 wrote:
> The question is: "How can I compare hypotheses H in different subgoals and
> if in each subgoals the hypotheses H are the same then apply some tactic?"
>
> Any idea?
>
>   
I don't believe you can.  The idea behind tactics is rather that you 
address each goal independently
from the others...

Can you turn your problem around so that all cases appear in the same goal?

As a side note, the example you give is very strange.  Do you believe that
by assuming

H: lista_predikata = predikat a1 b2 a3 c4 :: predikat d1 c2 a3 c4::nil


you are actually asserting that predikat a1 b2 a3 c4 hold?  This is not 
the case!

Nobody prevents you from defining a list of propositions, even if no 
element in the proposition
hold, as in the following script:

Require Import List.

Definition l := False::nil.

Definition counter_example : l = False::nil := refl_equal l.

In this three line script, we never provide a proof of False.

Yves