α : Type u
β : Type v
δ : Type w
g : α → β
f : α → α
a : α
⊢ corec g f a = g a :: corec g f (f a)
α : Type u
β : Type v
δ : Type w
g : α → β
f : α → α
a : α
⊢ unfolds g f a = g a :: unfolds g f (f a)
unfold unfolds
no goals
α : Type u
β : Type v
δ : Type w
g : α → β
f : α → α
a : α
⊢ corec g f a = g a :: corec g f (f a)
rw [corec_eq]