intro a a' hR
α : Type u_3
σ : Stream' α
β : Type u_1
α' : Type u_2
f : α → β
g : α → α
f' : α' → β
g' : α' → α'
R : α → α' → Prop
hf : ∀ (a : α) (a' : α'), R a a' → f a = f' a'
hg : ∀ (a : α) (a' : α'), R a a' → R (g a) (g' a')
⊢ ∀ {a : α} {a' : α'}, R a a' → corec f g a = corec f' g' a'
α : Type u_3
σ : Stream' α
β : Type u_1
α' : Type u_2
f : α → β
g : α → α
f' : α' → β
g' : α' → α'
R : α → α' → Prop
hf : ∀ (a : α) (a' : α'), R a a' → f a = f' a'
hg : ∀ (a : α) (a' : α'), R a a' → R (g a) (g' a')
a : α
a' : α'
hR : R a a'
⊢ corec f g a = corec f' g' a'