[Vicious Circles][1] by Barwise and Moss is a cornucopia of co-algebraic/co-inductive reasoning, and includes material on co-inductive games.

Not sure if it will help you out in your specific need, but might be the source of some inspiration in this line of reasoning.

**Edit (x2):** 

I think you can follow a modified [Ehrenfeucht-Fra&iuml;ss&eacute;][2] style approach like this: <em>Falsifier</em> gets to select any item from the stream/disjunction/conjunction.
<em>Verifier</em> then has to show that any such item must be a black cat.

(You could put ordering or number of choices restrictions on <em>Falsifier</em> without loss of generality for a finite set of coinductive rules.)

If you think of coinduction as just induction without a base case, it is obvious that the only (co-)induction rule you have on <code>blackCats</code> is <code>cat == BlackCat</code>, so what else could an individual cat be in that stream?  Any cat that <em>Falsifier</em> selects will have to conform to that rule, so <em>Verifier</em> wins.

Obviously this would scale to more numerous and complex coinductive rules, where the "challenge" for <em>Verifier</em> becomes to choose the appropriate rule for whatever item <em>Falsifier</em> chooses.



  [1]: http://www-csli.stanford.edu/pubs/
  [2]: http://en.wikipedia.org/wiki/Ehrenfeucht%E2%80%93Fra%C3%AFss%C3%A9_game