In general, a judgment is hypothetical, that is, it is made in a context \(\Gamma\), that is, a list \(x_1 {:} A_1, \ldots, x_n {:} A_n\) of variables which may occur free in the judgment together with their respective types. Note that the types in a context can depend on variables of earlier types. For example, \(A_n\) can depend on \(x_1 {:} A_1, \ldots, x_{n-1} {:} A_{n-1}\). The four forms of hypothetical judgments are