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