λ(a : *) → λ(b : *) → λ(c : *) → λ(g : b → c) → λ(f : a → b) → λ(x : a) → g (f x)