λ(k : Kind) → λ(a : k → k → Type) → λ(x : k) → a x