specialize ih (j+1)
case h.succ
α : Type u_1
σ✝ σ : Stream' α
j✝ i : ℕ
ih : ∀ (j : ℕ), σ (i + j) = corec σ (fun x => x + 1) j i
j : ℕ
⊢ σ (Nat.succ i + j) = corec σ (fun x => x + 1) j (Nat.succ i)
case h.succ
α : Type u_1
σ✝ σ : Stream' α
j✝ i j : ℕ
ih : σ (i + (j + 1)) = corec σ (fun x => x + 1) (j + 1) i
⊢ σ (Nat.succ i + j) = corec σ (fun x => x + 1) j (Nat.succ i)