rw [iterate_eq_Nat_iterate]
α : Type u_1
σ✝ : Stream' α
i j : ℕ
σ : Stream' α
f : ℕ → ℕ
⊢ iterate (fun s i => s (f i)) σ i j = σ (f^[i] j)
α : Type u_1
σ✝ : Stream' α
i j : ℕ
σ : Stream' α
f : ℕ → ℕ
⊢ (fun s i => s (f i))^[i] σ j = σ (f^[i] j)