suffices ∀ j,
  σ (i+j) = corec σ _ j i
from this 0
case h
α : Type u_1
σ✝ σ : Stream' α
i : ℕ
⊢ σ i = corec σ (fun x => x + 1) 0 i
case h
α : Type u_1
σ✝ σ : Stream' α
i : ℕ
⊢ ∀ (j : ℕ), σ (i + j) = corec σ (fun x => x + 1) j i