However, these rules make it possible to define terms without normal forms. Since the type-checking algorithm relies on the computation of normal forms of types, it no longer works for extensional type theory, see (Castellan, Clairambault, and Dybjer 2015).