no goals
α : Type u
β : Type v
δ : Type w
f : α → β
a : α
l : List α
s : Stream' α
⊢ map f (a :: l ++ₛ s) = List.map f (a :: l) ++ₛ map f s
rw [cons_append_stream, List.map_cons, map_cons, cons_append_stream, map_append_stream f l]