dest_uexists : term -> term * term

SYNOPSIS: Breaks apart a unique existence term.
DESCRIPTION: If t has the form ?!x. p[x] (there exists a unique [x such that p[x] then dest_uexists t returns the pair x,p[x]; otherwise it fails.
FAILURE CONDITIONS: Fails if the term is not a `unique existence' term.
SEE ALSO: dest_exists, dest_forall, is_uexists.