Proving with co-induction principles

Question

I'm going through Adam Chlipala's "Certified Programming with Dependent Types" (available here for convenience), and I'm a bit stuck at internalizing the introduction of co-induction principle for the stream_eq predicate in Chapter 5.

Firstly, I'm used to induction schemes defined for data structures (stream in this case, if it were data and not codata). Yet, the co-induction principle being introduced seems to be defined for the predicate we're trying to prove itself, and how does it connect with the following (cursive ours)?

Dually, a co-induction principle ought to be parameterized over a predicate characterizing what we mean to prove, as a function of the arguments to the co-inductive predicate that we are trying to prove.

Or should I parse this as implying parametrization over the predicate R : stream A -> stream A -> Prop, which, to me, seems like a reformulation of stream_eq, taking the following hypothesis into account?

Hypothesis Cons_case_hd : forall s1 s2, R s1 s2 -> hd s1 = hd s2.
Hypothesis Cons_case_tl : forall s1 s2, R s1 s2 -> R (tl s1) (tl s2).

Secondly, considering the quoted text again, we're trying to prove stream_eq. What would be the arguments to that predicate here? Looks like it should be the streams, but the hypothesis seem to be much more complex than that.

Lastly, all of this stream_eq_coind looks to me a like a somewhat generic way to do the match acrobatics on the streams to allow the simplifier to proceed (as Chlipala does in the version of the proof preceding this part). Is this correct or am I missing some deeper sense?

Oh, and what would be some good sources for me to read on co-induction? A few papers or tutorials I've found refer to some algebra or logic (i.e. Kripke models) quite beyond my current knowledge.