simp only [corec, map, nth]
case h
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
⊢ sum σ i =
    corec Prod.fst
      (fun x =>
        match x with
        | (acc, σ) => (acc + head σ, tail σ))
      (head σ, tail σ) i
case h
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
⊢ sum σ i = (iterate (fun x => (x.fst + head x.snd, tail x.snd)) (head σ, tail σ) i).fst