This is the best comment! I wondered this myself. I mean, I can test it and see that it appears to give the correct result, but how do I prove that it gives th

This is the best comment! I wondered this myself. I mean, I can test it and see that it appears to give the correct result, but how do I prove that it gives the correct result? I didn't include it, but you can do reductions, successively replacing the names with their expansions, and you see that it works out was we want. And in Combinatory Logic, there really is nothing else. If an expression has the correct "type," then it works. There's nothing except rearranging terms, duplicating terms, and erasing terms. But that being said, I don't know if that's a "proof," and I especially don't claim that a proof about Combinatory Logic would say anything at all about JavaScript.