funext i
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
⊢ sum σ =
    corec Prod.fst
      (fun x =>
        match x with
        | (acc, σ) => (acc + head σ, tail σ))
      (head σ, tail σ)
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