The Coq mailing list

["Akuma GnacGnac" <akumagnacgnac AT hotmail.com>]

Hi Li-Yang,

I'm not sure I pointed out the problem but it seems this lemma can easily be 
proven via the f_equal function of type (forall (A B : Type) (f : A -> B) (x 
y : A), x = y -> f x = f y) when applied with the following instance of f :
fun (A : Set) (P : A -> Set) (e : sigS P) :=
 match e with
| existS _ p => p end.

What I want to do here is using the fact that if two objects are equal, then 
applying any function to both objects will lead to the same result.
Then, we just have to apply a function that returns the last argument of the 
existS constructor.

But trying to declare such an instance of f leads to the following user 
error :
Inference of annotation not yet implemented in this case

So I guess the lemma is valid but can't be proven in Coq for the moment.

I hope I didn't say any big mistake, I hope I didn't point out the obvious 
and I hope I was of any help.

> Hi All,
>
> I am having trouble proving a seemingly intuitive fact about dependent
> records:
>
> Lemma projS2_eq :
>   forall (A : Set)(P : A -> Set)(x : A) (p1 p2 : P x),
>   existS P x p1 = existS P x p2 -> p1 = p2.