simp [even, corec, map, head, nth, tail, iterate_stream_eq_index_iterate, iterate_add_eq_mul 2]
case h
α : Type u_1
σ✝ σ : Stream' α
i : ℕ
⊢ even σ i = σ (i * 2)
case h
α : Type u_1
σ✝ σ : Stream' α
i : ℕ
⊢ σ (2 * i) = σ (i * 2)