Given a term of the form "?!x.P[x]", the conversion EXISTS_UNIQUE_CONV
proves that this assertion is equivalent to the conjunction of two statements,
namely that there exists at least one value x such that P[x], and that
there is at most one value x for which P[x] holds. The theorem returned is:
|- (?! x. P[x]) = (?x. P[x]) /\ (!x x'. P[x] /\ P[x'] ==> (x = x'))
where x' is a primed variant of x that does not appear free in
the input term. Note that the quantified variable x need not in fact appear
free in the body of the input term. For example, EXISTS_UNIQUE_CONV "?!x.T"
returns the theorem:
|- (?! x. T) = (?x. T) /\ (!x x'. T /\ T ==> (x = x'))