∀(k : Kind) → (k → k → Type) → k → k → Type