α : Type u
β : Type v
δ : Type w
f : α → β
g : α → α
a : α
⊢ f a :: map f (iterate g (g a)) = f a :: corec f g (g a)
α : Type u
β : Type v
δ : Type w
f : α → β
g : α → α
a : α
⊢ corec f g a = f a :: corec f g (g a)
rw [corec_def, map_eq, head_iterate, tail_iterate]
no goals
α : Type u
β : Type v
δ : Type w
f : α → β
g : α → α
a : α
⊢ f a :: map f (iterate g (g a)) = f a :: corec f g (g a)
rfl