 Expressions of the form \(M\colon A\) above are called type assignments. A characteristic feature of type-assignment systems is that if \(M\colon A\) is provable then \(A\) is considered to be one of the types that can be assigned to \(M\). However, a provable assignment does not preclude other types from becoming associated to the same term \(M\), that is a type assignment does not fix the type of a term rigidly. \(\Delta\) and \(\Theta\) on the left-hand side of \(\vdash\)  are sets of type assignments to variables, and they are assumed to be consistent—meaning that no variable may be assigned two or more types.