Church's type theory is a formulation of higher-order logic that allows quantification over sets and functions. In this logic, any set definable by an expression of the language can be proved to exist. This expressive power allows a natural formalization of much of mathematics.

To ensure completeness, a higher-order theorem prover must ensure that instantiations for sets definable using logical constants can be discovered. In the presence of extensionality, one can make several restrictions to the set instantiations necessary without sacrificing completeness. For example, one can restrict the logical constants available for set instantiations. Also, one can assume set instantiations are in a prenex conjunctive normal form.

The theorem prover TPS has traditionally been used to search for theorems provable without using extensionality. TPS has now been updated to include search procedures appropriate for extensional type theory. I will describe the search procedure and give examples of theorems of extensional type theory which TPS can now prove.