mk_exists : term * term -> term
STRUCTURE
SYNOPSIS
Term constructor for existential quantification.
DESCRIPTION
If v is a variable and t is a term of type bool, then mk_exists (v,t) returns the term ?v. t.
FAILURE
Fails if v is not a variable or if t is not of type bool.
SEEALSO
HOL  Kananaskis-13