{-# OPTIONS --guardedness #-}

open import Relation.Binary.PropositionalEquality

module _ (A : Set) where

  record Stream : Set where
    coinductive
    field
      hd : A
      tl : Stream

  open Stream

  record _≈_  (σ ψ : Stream) : Set where
    coinductive
    field
      hd-≡ : hd σ ≡ hd ψ
      tl-≈ : tl σ ≈ tl ψ

  open _≈_

  even : Stream → Stream
  hd (even σ) = hd σ
  tl (even σ) = even (tl (tl σ))

  odd : Stream → Stream
  hd (odd σ) = hd (tl σ)
  tl (odd σ) = odd (tl (tl σ))

  zip : Stream → Stream → Stream
  hd (zip σ ψ) = hd σ
  tl (zip σ ψ) = zip ψ (tl σ)

  lemma : ∀ σ → σ ≈ (zip (even σ) (odd σ))
  hd-≡ (lemma σ) = refl
  tl-≈ (lemma σ) = helper σ
    where
      helper : ∀ σ → tl σ ≈ zip (odd σ) (even (tl (tl σ)))
      hd-≡ (helper σ) = refl
      tl-≈ (helper σ) = lemma (tl (tl σ))