The conversion FUN_EQ_CONV embodies the fact that two functions are equal
precisely when they give the same results for all values to which they can be
applied. When supplied with a term argument of the form f = g, where f and
g are functions of type ty1->ty2, FUN_EQ_CONV returns the theorem:
where x is a variable of type ty1 chosen by the conversion.
|- (f = g) = (!x. f x = g x)