The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

If you use the tactic [subst a] (or [subst b]), and then [f_equal], you'll be left with the goal [prf_a = prf_b].  You can either prove this manually (if they're the same), or [apply proof_irrelevance], if you [Require Import ProofIrrelevance].

-Jason

On Fri, Jun 29, 2012 at 4:06 AM, Helge Bahmann <hcb AT chaoticmind.net> wrote:

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