Problems with a conductive proof

Question

I'm trying to understand coinduction (I'm reading Sangiorgi's book) using Agda. I already managed to prove some simple equalities between streams, but I'm stuck trying to prove that all natural numbers (values of type ℕ) are in the stream allℕ --- function allℕisℕ. Any tip on how should I proceed with this?

open import Coinduction
open import Data.Nat

module Simple where

   data Stream (A : Set) : Set where
     _∷_ : A → ∞ (Stream A) → Stream A

   infix 4 _∈_

   data _∈_ {A : Set} : A → Stream A → Set where
     here  : ∀ {x xs} → x ∈ x ∷ xs
     there : ∀ {x y xs} → (x ∈ ♭ xs) → x ∈ y ∷ xs

   enum : ℕ → Stream ℕ
   enum n = n ∷ (♯ enum (suc n))

   allℕ : Stream ℕ
   allℕ = enum 0

   allℕisℕ : ∀ (n : ℕ) → n ∈ allℕ
   allℕisℕ n = ?

Answer 1

Just sharing the complete solution...

open import Coinduction
open import Data.Nat

module Simple where

  data Stream (A : Set) : Set where
    _∷_ : A → ∞ (Stream A) → Stream A

  infix 4 _∈_

  data _∈_ {A : Set} : A → Stream A → Set where
    here  : ∀ {x xs} → x ∈ x ∷ xs
    there : ∀ {x y xs} → (x ∈ ♭ xs) → x ∈ y ∷ xs

  enum : ℕ → Stream ℕ
  enum n = n ∷ (♯ enum (suc n))

  allℕ : Stream ℕ
  allℕ = enum 0

  ∈-suc : ∀ {n m : ℕ} → n ∈ enum m → suc n ∈ enum (suc m)
  ∈-suc here = here
  ∈-suc (there p) = there (∈-suc p)

  allℕisℕ : ∀ (n : ℕ) → n ∈ allℕ
  allℕisℕ zero = here
  allℕisℕ (suc n) = there (∈-suc (allℕisℕ n))