Γ ⊢ S = { t₀ : *, t₁ : *, ... tₙ : * }
Γ ⊢ f : * → *₀ → *₁ → ... → *ₙ
|S| ≠ 0
──────────────────────────────────
Γ ⊢ [f t₀ t₁ ... tₙ] : *

TypeApplication