When stating the rules we will use the letter \(\Gamma\) as a meta-variable ranging over contexts, \(A,B,\ldots\) as meta-variables ranging over types, and \(a,b,c,d,e,f,\ldots\) as meta-variables ranging over terms.