Kind Well-Formedness

$$\infer{\Gamma \vdash \mathsf{Type}}{} \quad \infer{\Gamma \vdash ... ...(\kappa_1 \times \ldots \times \kappa_n)}{ \forall i: \Gamma \vdash \kappa_i }$$

$$\infer{\Gamma \vdash X}{ X \in \Gamma } \quad \infer{\Gamma \vdash X \longrightarrow \kappa}{ \Gamma, X \vdash \kappa }$$