The Coq mailing list

[Keiko Nakata <keiko AT kurims.kyoto-u.ac.jp>]

> I have been looking for a way to forbid the intentional equality
> on colists at all so that any predicate on colists shall not distinguish
> bisimilar colists.

My point was that the presence of the intentional equality on colists
is the only reason that I can define a predicate on colists which can
distinguish bisimilar colists. (Am I correct?)
But, admittedly, even though I could forbid the use of the intentional
equality on colists, I will not be able to prove in Coq that any
definable predicate is indeed insensitive to bisimilarity. 

Keiko