dsimp [map]
α : Type u
β : Type v
γ : Type w
g : β → γ
f : α → β
a : α
as : List α
h_ind : map (g ∘ f) as = map g (map f as)
⊢ map (g ∘ f) (a :: as) = map g (map f (a :: as))
α : Type u
β : Type v
γ : Type w
g : β → γ
f : α → β
a : α
as : List α
h_ind : map (g ∘ f) as = map g (map f as)
⊢ g (f a) :: map (g ∘ f) as = g (f a) :: map g (map f as)