Comment by kmill

I used Lean too earlier today :-)

I saw what each #reduce c c ... c did to explore the "palette" I had to work with, and then accidentally stumbled upon the answer that way. I also stumbled on the c (c c) c solution.

May as well include a formalized proof while we're at it:

  def c (g : β → γ) (f : α → β) (x : α) : γ := g (f x)

  example (h : γ → δ) (g : β → γ) (f : α → β) (x : α) :
      h (g (f x)) = (c (c c) c) h g f x :=
    rfl

  -- Or
  example  :
      (fun (h : γ → δ) (g : β → γ) (f : α → β) (x : α) => h (g (f x)))
        = (c (c c) c) :=
    rfl