 Normally when one assumes the Axiom of Choice in type theory, one assumes it as an axiom schema, and asserts AC\(^{\alpha}\) for each type symbol α. A similar remark applies to the axioms for extensionality and description. However, modern proof systems for Church’s type theory, which are, e.g., based on resolution, do in fact avoid the addition of such axiom schemata for reasons as further explained in  Sections 3.4  and  4  below. They work with more constrained, goal-directed proof rules instead.