induction as
α : Type u
β : Type v
γ : Type w
g : β → γ
f : α → β
as : List α
⊢ map (g ∘ f) as = map g (map f as)
case nil
α : Type u
β : Type v
γ : Type w
g : β → γ
f : α → β
⊢ map (g ∘ f) [] = map g (map f [])

case cons
α : Type u
β : Type v
γ : Type w
g : β → γ
f : α → β
head✝ : α
tail✝ : List α
tail_ih✝ : map (g ∘ f) tail✝ = map g (map f tail✝)
⊢ map (g ∘ f) (head✝ :: tail✝) = map g (map f (head✝ :: tail✝))