The Coq mailing list

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

Hi Yves,

> You really sent us very little context, but assuming you are using a  
> defined equality because it is
> more strictly more liberal than Leibniz equality (i.e. there are a  
> and b such that a === b and a <> b),
> I think that what you are trying to prove is not true!  List.in  
> explicitly relies on Leibniz equality.

Aah, I see. That makes perfect sense, thank you.

(The === relation came from the Metatheory library bundled with Brian  
Aydemir's LNgen tool; quite frankly, I didn't really understand it and  
I was trying to copy the style of an existing lemma. "Proof by  
incantation" as my previous advisor would say ;)

Changing the relation R to be simply eq solves it.

Thanks,

Edsko