-[Fussy note: the justification for counting `(\x. x y) z` as
-equivalent to `(\z. z y) z` is that when a lambda binds a set of
-occurrences, it doesn't matter which variable serves to carry out the
-binding. Either way, the function does the same thing and means the
-same thing.
-Linguistic trivia: some linguistic discussions suppose that alphabetic variance
-has important linguistic consequences (notably Ivan Sag's dissertation).
-Look in the standard treatments for discussions of alpha
-equivalence for more detail. Also, as mentioned below, one of the intriguing
-properties of Combinatory Logic is that alpha equivalence is not an issue.]
-