EXISTS_UNIQUE_CONV
Conv.EXISTS_UNIQUE_CONV : conv
Expands with the definition of unique existence.
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".