[plt-scheme] Check for function equality?

On Thu, 2009-02-19 at 18:26 -0500, Marco Morazan wrote:
   . . .
> Others have suggested using theorem provers. This is also something
> that can lead you down an enlightening path. :-)

This brings up an interesting question.  We know that there is no
decision procedure for First-Order Predicate with Equality, but
Herbrand's Theorem tells us there is a semi-decision procedure, that is,
there is a procedure that halts on any theorem saying "it's a theorem",
but some non-theorems cause it to spin.  Is there anything analogous for
the Halting Problem or function equivalence, or are we in a situation
like Second-Order Predicate Calculus which has no semi-decision
procedure because any such could be used to build a decision procedure
for FOPC?

 -- Bill Wood