 Cut-elimination proofs (see also the SEP entry on  proof theory)  for Church’s type theory, which are often closely related to such proofs (Takahashi 1967, 1970; Prawitz 1968; Mints 1999) for other formulations of type theory, may be found in Andrews 1971, Dowek &amp; Werner 2003, and Brown 2004. In Benzmüller et al. 2009 it is shown how certain wffs\(_{{o}}\), such as axioms of extensionality, descriptions, choice (see  Sections 1.3.3  to  1.3.5),  and induction, can be used to justify cuts in cut-free sequent calculi for elementary type theory. Moreover, the notions of cut-simulation and cut-strong axioms are introduced in this work, and the need for omitting defined equality and for eliminating cut-strong axioms such as extensionality, description, choice and induction in machine-oriented calculi (e.g., by replacing them with more constrained, goal-directed rules) in order to reduce cut-simulation effects are discussed as a major challenge for higher-order automated theorem proving. In other words, including cut-strong axioms in a machine-oriented proof calculus for Church’s type theory is essentially as bad as including a cut rule, since the cut rule can be mimicked by them.