The Coq mailing list

[Romain Janvier <Romain.Janvier AT imag.fr>]

Is there a tactic that can automaticly transforme a goal the same way
that "inversion" does with the hypothesys as (Pair A x)=(Pair A B)
giving x=B.

For example if I have (Pair A x)=(Pair A B) in my goal, can I
automaticly obtain x=B as my new goal?

And if it's possible, can I do the same with a goal as:
(EX x| (Pair A x)=(Pair A B))
And obtain:
(EX x| x=B)
?

Thank you.