simp [even, dropEveryNth, corec']
α : Type u_1
σ : Stream' α
⊢ dropEveryNth 2 σ = even σ
α : Type u_1
σ : Stream' α
⊢ corec (fun x => head x.fst)
      (fun x =>
        match x with
        | (σ, 0) => (tail (tail σ), 0)
        | (σ, Nat.succ m) => (tail σ, m))
      (σ, 0) =
    corec (fun s => head s) (fun s => tail (tail s)) σ