[Agda] Infinite proofs

[Yasuyuki Ogawa]

 > The usual solution is to define a custom equivalence relation 
(bisimulation)

Although I tried following code (is used in CPDT), I couldn't.
Is there something wrong?

data StreamEq {A : Set} : Stream A -> Stream A -> Set where
   streamEq : forall {a xs ys} -> StreamEq xs ys
     -> StreamEq (cons a (# xs)) (cons a (# ys))

theorem-ones-eq' : StreamEq ones ones'
theorem-ones-eq' = ?