The Coq mailing list

[Helge Bahmann <hcb AT chaoticmind.net>]

Hello,

I am stuck in a proof with the goal "exist P a prf_a = exist P b prf_b" with 
the assumption "a = b" available -- I have read about dependent pairs, but I 
have been unable to figure out how to apply this syntactically to my problem 
(if it applies at all?).

Could anyone give me a hint how I could proceed?

Regards
Helge