 We use \(\textsf{Sub}(\bB,\bv,\bA)\) as a notation for the result of substituting \(\bB\) for \(\bv\) in \(\bA\), and \(\textsf{SubFree}(\bB,\bv,\bA)\) as a notation for the result of substituting \(\bB\) for all free occurrences of \(\bv\) in \(\bA\). The process of replacing \([\lambda \bv_{\beta}\bA_{\alpha}]\bB_{\beta}\) by \(\textsf{SubFree}(\bB_{\beta},\bv_{\beta},\bA_{\alpha})\) (or vice-versa) is known as β-conversion, which is one form of λ-conversion. Of course, when \(\bA_{{o}}\) is a wff of type \({o}\), \([\lambda \bv_{\beta}\bA_{{o}}]\) denotes the set of all elements \(\bv_{\beta}\) (of type \(\beta)\) of which \(\bA_{{o}}\) is true; this set may also be denoted by \(\{\bv_{\beta}|\bA_{{o}}\}\). For example, \([\lambda x\ x&lt;y]\) denotes the set of x such that x is less than y (as well as that property which a number x has if it is less than y). In familiar set-theoretic notation, 