title: Problems with a conductive proof
body: <p>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?</p>
  
  <pre><code>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 = ?
  </code></pre>