I'm going to repeat my comment from last time this came up-- this is a really neat way of getting around the use of dummy variables, but why does he only talk about beta reduction and never mention eta reduction? Describing eta reduction in this notation is still easy.