## Strategy Menu:

# Existence & Uniqueness Command

The Existence & Uniqueness command can only be used when you
have a goal of the form !*xP*(*x*). If you select a goal of
this form and give the Existence & Uniqueness command, then Proof
Designer will say that to complete the proof you have to prove both *xP*(*x*) and *x**y*(*P*(*x*)*P*(*y*)*x* = *y*). The two parts of the proof are
labeled Existence and Uniqueness.