Your intuition is probably driven by the fact that the theorem isn't true in any popular programming language. The added feature that the proof relies on is tha

Your intuition is probably driven by the fact that the theorem isn't true in any popular programming language. The added feature that the proof relies on is that "truthy" conditionals allow the programmer to distinguish a function from a falsy value (such as false). Many other features might provide this capability as well: the ability to compare a function to a boolean directly, a typeof function provided you have the ability to compare its results, an "is function" query, or the ability to try arithmetic on the value or call it as a function and trap an error if that doesn't work. So Shriram's enumeration of possible things you might do to the function, which is required to show the two expressions are equivalent in the starting language, is much shorter than it would be in a practical language, and as a result the proof wouldn't hold. On the other hand, I can attest that if you design a very minimal language and don't consider the question of how to tell what type a value has, you may well end up with a language that doesn't have that capability!