intro as
α : Type u
β : Type v
γ : Type w
g : β → γ
f : α → β
⊢ ∀ {as : List α}, map (g ∘ f) as = map g (map f as)
α : Type u
β : Type v
γ : Type w
g : β → γ
f : α → β
as : List α
⊢ map (g ∘ f) as = map g (map f as)