[Agda] Infinite proofs

[Yasuyuki Ogawa]

Hi! I'm studying Agda with CPDT, and now reading
"Infinite Data and Proofs" section.

(http://adam.chlipala.net/cpdt/html/Coinductive.html)

But I can't prove a following infinite proof...
In CPDT, this requires StreamEq, so I tried it but
I couldn't. Can anyone help me?

zeros : Stream N
zeros = cons 0 (# zeros)

ones : Stream N
ones = cons 1 (# ones)

map : forall {A B} -> (A -> B) -> Stream A -> Stream B
map f (cons x xs) = cons (f x) (# map f (b xs))

ones' : Stream N
ones' = map suc zeros

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

Thank you!