The Coq mailing list

[Sean Wilson <sean.wilson AT ed.ac.uk>]

Hi,

I'm working with goals containing existential quantifiers like the following:

h : A
t : list A
o : list A
______________________________________(1/1)
exists f : list A, f ++ o = h :: t ++ o

To progress, I must call "exists h::t", which you can work out by unification 
of the two sides of the equality. Does Coq have any way of inferring this and 
solving the goal automatically? Also, are there any other tactics 
besides "exists" that let me manipulate goals like this in useful ways?

Regards,

Sean