have (g : ℕ × Stream' ℕ → ℕ) (y) : 
    Prod.snd ((fun x => (g x, tail x.snd))^[i] (y, tail σ))
    = ((fun x => tail x)^[i] (tail σ)) := by
  induction i generalizing y σ <;> simp [*]
case h.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
⊢ σ (i + 1) = Prod.snd ((fun x => (x.fst + Prod.snd x 0, tail x.snd))^[i] (σ 0, tail σ)) 0
case h.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
this :
  ∀ (g : ℕ × Stream' ℕ → ℕ) (y : ℕ), ((fun x => (g x, tail x.snd))^[i] (y, tail σ)).snd = (fun x => tail x)^[i] (tail σ)
⊢ σ (i + 1) = Prod.snd ((fun x => (x.fst + Prod.snd x 0, tail x.snd))^[i] (σ 0, tail σ)) 0