mk_exists : term * term -> term

SYNOPSIS
Term constructor for existential quantification.

DESCRIPTION
mk_exists(`v`,`t`) returns `?v. t`.

FAILURE CONDITIONS
Fails with if first term is not a variable or if t is not of type `:bool`.

EXAMPLE
  # mk_exists(`x:num`,`x + 1 = 1 + x`);;
  val it : term = `?x. x + 1 = 1 + x`

SEE ALSO
dest_exists, is_exists, list_mk_exists.