The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Hai WAN wrote:
> (* Here are the Coq codes abstracted from a real problem.*)
>
> Section test.
> Variable P Q : Prop.
> Variable a : P /\ Q.
> Variable get : P -> Set.
> Variable H0 :
>     match a with
>         | conj H0 _ => get H0
>     end.
> Variable b : P.
>
> (* I want to prove this goal, but got stuck. Could any one help? 
> Thanks in advance!*)
>
> Goal (get b).

I expect you need something like proof irrelevance to prove your 
theorem, like so:
====
 Require Import ProofIrrelevance.

 Goal (get b).
   rewrite (proof_irrelevance P b (match a with
                                     | conj H _ => H
                                   end));
   generalize dependent H0; case a; tauto.
 Qed.
====

Intuitively, the theorem seems false without proof irrelevance, because 
you have no way of showing that [get] can't return different [Set]s for 
different proofs of [P].  Alternatively, you could avoid axioms by 
adding a [Hypothesis] asserting that [get] has this property.