The Coq mailing list

[Robert Helgesson <robert AT rycee.net>]

Hello,

I'm just starting to learn Coq and have been playing around a bit with
setoids.  It's been challenging for sure but with a bit of effort and
reading I've been able to figure out the problems I've run into.
However, now I've encountered an interesting thing which, while it
doesn't seem very tricky, I can't figure out!

Ok, so it's easily possible to prove

 Lemma sym_sym_eq : forall (A : Type) (x y : A) (H : x = y),
    symmetry (symmetry H) = H.

But I haven't been able to figure out how to prove something like

 Lemma sym_sym_equiv : forall (A : Type) (S : Setoid A) (x y : A)
    (H : x == y), symmetry (symmetry H) = H.

Is it at all possible to prove this general case and if so, how?  If
it's not possible then I would appreciate a short description why.

Many thanks.

/Robert