The Coq mailing list

[anoun AT labri.fr]

Hi,
Let's consider an inductif type toto with a constructor c1 which takes n
arguments  whose respective types are: t1 t2 ...tn

If we have a current goal of the form
============================
c1 a1 a2 ..an=c1 b1 b2 ...bn

Is there a direct tactic that simplifies this goal into n sub-goals ai=bi
(i=1..n)
? Of course we can use the cut tactic n times,but it's not what I'm looking 
for,
I need a generic tactic ...

Does such a tactic exist?
Thanks
Houda

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.