EXISTS_DEL_CONV "?x1 ... xn. t" returns the theorem:
|- (?x1 ... xn. t) = t
provided x1,...,xn are not free in t.
FAILURE
Fails if any of the x’s appear free in t. The function does not perform a
partial deletion; for example, if x1 and x2 do not appear free in t but
x3 does, the function will fail; it will not return: