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.