α : Type u
β : Type v
δ : Type w
f : α → β
a : α
s : Stream' α
⊢ head (f (head (a :: s)) :: map f (tail (a :: s))) :: tail (f (head (a :: s)) :: map f (tail (a :: s))) =
    f a :: map f s
α : Type u
β : Type v
δ : Type w
f : α → β
a : α
s : Stream' α
⊢ map f (a :: s) = f a :: map f s
rw [← Stream'.eta (map f (a::s)), map_eq]
no goals
α : Type u
β : Type v
δ : Type w
f : α → β
a : α
s : Stream' α
⊢ head (f (head (a :: s)) :: map f (tail (a :: s))) :: tail (f (head (a :: s)) :: map f (tail (a :: s))) =
    f a :: map f s
rfl