 If x is a variable of type \( \tau \) and A is a wff then \(\lambda x A\) is a term of r-type \((\tau)/n\) (where n is one more than the highest order of any bound variable in A and at least as high as the order of any free variable in A).