The Coq mailing list

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

Hello,

Are there any potentially bad consequences of having 
"Add Relation sequence bisimilar", 
where sequence and bisimilar are defined coinductively, 
i.e. infinite lists and the bisimilar relation on them?

I am aware of an issue concerning type preservation discussed: 

http://logical.saclay.inria.fr/coq-puma/messages/b35593715e6cbad3#msg-b35593715e6cbad3

I also remember someone told me that he suspect that there might be
some bad interactions between Coq's criterion of guardedness and Setoids.

I was thinking if, with "Add Relation sequence bisimilar", 
any predicate on sequences will not distinguish bisimilar lists; 
this sounds interesting to me.

Best regards,
Keiko