 When the definitions of  Section 1.2.1  are employed, where equality has been defined in terms of Leibniz’ principle, then this statement is not implied for all types α. It only holds if we additionally require that the domains \(\cD_{{o}\alpha}\) contain all the unit sets of objects of type α, or, alternatively, that the domains \(\cD_{{o}\alpha\alpha}\) contain the respective identity relations on objects of type α (which entails the former). The need for this additional requirement, which is not included in the original work of Henkin (1950), has been demonstrated in Andrews 1972a.