⁴Note that, since when the predicate is not true it remains unevaluated, we have defined it at the kind level, that is, as a partial Boolean function; however, using the owise attribute (see Section 4.5.4) it is very easy to add an extra equation making _occurs-inner_ a total Boolean function.