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.