 which replaces  ***,  when level indicators are supplied, defines an infinite list of het predicates, “het2”, “het3”, …, and the two other starred principles are also to be supplied with level indicators. Church now gives what appears to be a hastily composed list of inferences with annotations but no comment. However, Church in effect here proves the analogues of theorems (6) and (7) of (1976), with \(D\) in place of Val. These are: