EXISTS_EQN_CONV : conv
STRUCTURE
SYNOPSIS
Proves the existence of a line that has a non-recursive equation.
LIBRARY
unwind
DESCRIPTION
EXISTS_EQN_CONV "?l. !y1 ... ym. l x1 ... xn = t" returns the theorem:
   |- (?l. !y1 ... ym. l x1 ... xn = t) = T
provided l is not free in t. Both m and n may be zero.
FAILURE
Fails if the argument term is not of the specified form or if l appears free in t.
SEEALSO
HOL  Trindemossen-1