----------------------------------------------------------------------
EXISTS_UNIQUE_CONV                                              (Conv)
----------------------------------------------------------------------
EXISTS_UNIQUE_CONV : conv

SYNOPSIS
Expands with the definition of unique existence.

KEYWORDS
conversion, quantifier, existential, unique.

DESCRIBE
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'))




FAILURE
{EXISTS_UNIQUE_CONV tm} fails if {tm} does not have the form {"?!x.P"}.

SEEALSO
Conv.EXISTENCE.

----------------------------------------------------------------------