[rocqua]

At this point, you start hitting a problem from fundamental computation. When are 2 programs equivalent? Is it when they behave equivalently in any implementation or is it when there is a chain of rewriting rules that change one to the other.

The issue with the first definition is 2-fold. What set of implementations are you qualifying over, and what to do with weird programs that crash occasionally. This is similar to what happens in the given example. The program is equivalent to 'return 1' when f is always false. Otherwise, it might crash.

In the second definition, 'return 1' and the given program are just different programs, until you actually substitute an f and continue reduction.