funext x
α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
f : α → β
g : β → γ
h : γ → δ
⊢ (h ∘ g) ∘ f = h ∘ g ∘ f
case h
α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
f : α → β
g : β → γ
h : γ → δ
x : α
⊢ comp (h ∘ g) f x = comp h (g ∘ f) x