 To obtain a Unifying Principle for extensional type theory with defined equality, Benzmüller &amp; Kohlhase 1997 added the following conditions for boolean extensionality, functional extensionality and saturation to the above conditions 1.-7. for \(\cT\) (their presentation has been adapted here; for technical reasons, they also employ a slightly stronger variant for condition 2. based on β-conversion rather than β-normalization):