The Coq mailing list

[marko AT ffri.hr]

Greetings,

If I have something like this:

Section Proba.
Inductive elementi1 : Set := a1 | b1 | c1 | d1 | e1 | f1 | g1.
Inductive elementi2 : Set := a2 | b2 | c2 | d2 | e2 | f2 | g2.
Inductive elementi3 : Set := a3 | b3 | c3 | d3 | e3 | f3 | g3.
Inductive elementi4 : Set := a4 | b4 | c4 | d4 | e4 | f4 | g4.
Require Import List.
Parameter predikat : elementi1 -> elementi2 -> elementi3 -> elementi4 ->
Prop.
Parameter lista_predikata : list Prop.
Parameter goal : Prop.
Hypothesis H : lista_predikata = predikat a1 b2 a3 c4 :: predikat d1 c2 a3
c4 :: nil.

Coq < Goal goal.
1 subgoal

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

Unnamed_thm <

and if I have several subgoals but each subgoal contain hypothesis H of
same type and the same lenght but (maybe) with different elements (a1
b2... and so on can be different on different places).

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?

Thank you wery much,

Marko Malikoviæ