!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 
xy(P(x)
P(y)
x = y). The two parts of the proof are
labeled Existence and Uniqueness.