unfold iterate Nat.iterate
case succ
α : Type ?u.15
σ : Stream' α
α✝ : Type u_1
f : α✝ → α✝
a : α✝
i : ℕ
ih : iterate f a i = f^[i] a
⊢ iterate f a (Nat.succ i) = f^[Nat.succ i] a
case succ
α : Type ?u.15
σ : Stream' α
α✝ : Type u_1
f : α✝ → α✝
a : α✝
i : ℕ
ih : iterate f a i = f^[i] a
⊢ f (iterate f a i) = f^[i] (f a)