exact hR
case h.a.zero
α : 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'
⊢ R (iterate g a Nat.zero) (iterate g' a' Nat.zero)
no goals