Terminology 50: A defined type will be declared by providing some word or phrase \mathsf{N} (the name) together with a placeholder variable \mathsf{p} and a defining statement (or definition) \phi . Given such information and some variable x , we may use abbreviations similar to \textup{"}x \textup{ is a } \mathsf{N}\textup{"} \hspace{3mm} \textup{to mean} \hspace{3mm} [\phi | \mathsf{p} \to x], where we are using variable substitution. In practice, such a defined type will typically be introduced by declaring something like \textup{"we will call }x \textup{ a } \mathsf{N} \textup{ if } [\phi | \mathsf{p} \to x]\textup{"}.