The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 06/02/2013 05:45 PM, Floyd Lee wrote:
> Is this deceptively simple theorem provable in Coq's logic?
>
> Lemma sig_map_eq : forall
>    {A   : Type}
>    (P   : A ->  Prop)
>    (x y : sig P),
>    proj1_sig x = proj1_sig y ->  x = y.
>    

No, I think this is close to one of the standard corollaries of Axiom K, 
for which an axiom-free proof isn't known.  Perhaps this fact has even 
been proved independent of CIC, as K has.

The library fact I'm thinking of is [inj_pair2], which you can get at 
after [Require Import Eqdep].  An important difference is that 
[inj_pair2] is about [sigT] instead of [sig], and also it only concludes 
something about one component of a pair.

On the bright side, when [A] has decidable equality, you may be able to 
use [Eqdep_dec]-y tricks to prove your lemma!