The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

Hi,

Coq is giving me an error, and I'm not sure what it means. A tiny bit  
of context: in the proof of a simple lemma, I need to prove that

Hin : z === x
______________________________________(1/2)
List.In (x, c) ((z, c) :: l)

which surely should be easy (rewrite using Hin, since I cannot do  
"subst"), and then apply In_head (or whatever that lemma is called).  
However, calling "rewrite Hin" gives the following error:

Error: Tactic failure: setoid rewrite failed: unable to satisfy the  
rewriting constraints.
Unable to satisfy the following constraints:
In environment:
A : Type
B : Type
key : Type
x : key
a : A
E : list (key * A)
F : list (key * A)
G : list (key * A)
R : relation key
Equiv : Equivalence R
Eqdec : EqDec key R
Fset : FSet key Eqdec
z : key
c : A
l : list (key * A)
IHl : x `in` dom l -> exists b : A, binds x b l
Hin : z === x

?10768 == (Morphism (?10764 ==> flip impl) (eq (x, c)))
?10767 == (MorphismProxy ?10765 c)
?10766 == (Morphism (equiv ==> ?10765 ==> ?10764) pair)
?10765 == (relation A)
?10764 == (relation (key * A)).

I'm not sure what that means. Any pointers would be appreciated,

Edsko