EXISTS_UNIQUE_CONV : conv
STRUCTURE
SYNOPSIS
Expands with the definition of unique existence.
DESCRIPTION
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
HOL  Kananaskis-13