 The type system is enforced by the grammar of the language. Atomic sentences are equations or membership statements, and they are only well-formed if they take one of the forms \(x^{n} = y^{n}\) or \(x^{n} \in y^{n+1}\).