 A further extended Unifying Principle for extensional type theory with primitive equality is presented and used in Backes &amp; Brown 2011 to prove the completeness of a tableau calculus for type theory which incorporates the axiom of choice.