[chriswarbo]

Co-inductive methods are useful for that sort of thing.

For example, we can prove two infinite streams are equal by showing that their definitions/generators are "bisimilar".

[maweki]

But the question is not whether their infinite extensions or limit are equal, but whether at each finite combination some property about the stream progress holds.