Some/Any is Easy, Effective, and Necessary
  (A Formal Proof of the Decidability of alpha-Equivalence)

                    Rene Vestergaard


We account for the crucial role played by a Some/Any property in a
formally correct proof of decidability of alpha-equivalence in the
lambda-calculus. We do so to show-case the proof theory of
Some/Any-ness, which is related to extensionality, transitivity,
and computability concerns.