Description: Equality inference for the function predicate. (Contributed by Jonathan Ben-Naim, 3-Jun-2011)