theorem Function.comp_assoc (f : γ → δ) (g : β → γ) (h : α → β) : (f∘g)∘h = f∘g∘h := rfl