Add note about β-reduction for type variables.