simp only [corec, map, nth, iterate_eq_Nat_iterate, Function.iterate_succ, Function.comp_apply]
α : Type ?u.5702
σ : Stream' α
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → α✝
g : α✝¹ → α✝¹
x : α✝¹
i : ℕ
⊢ corec f g x (i + 1) = corec f g (g x) i
no goals