Proving the Equivalence of Higher-Order Terms by Means of Supercompilation