 Note that, as in the case of Val, the level \(m+1\) of \(D^{m+1}\) is determined entirely by the level of its second argument place. (5) is needed as a lemma in the proofs of (\(6'\)) and (\(7'\)). In (1995a) Church appeals to (5) without comment, perhaps assuming implicitly the \(D\)-analogue of axiom (4) of (1976) reflecting that the types of the semantical predicates are cumulative—as are the types of (1976) in general. It is also worth noting that in the background is an r-typed version of the  principle **  asserting that at any level \(m\) there is a word \(v\) denoting a property having the same extension as \(\het^m\). (Compare theorem (8) of (1976).)