Undecidability of equivalence

https://en.wikipedia.org/wiki/Lambda_calculus#Undecidability_of_equivalence - it's been there all along...

There is no algorithm that takes as input two lambda expressions and outputs TRUE or FALSE depending on whether or not the two expressions are equivalent. This was historically the first problem for which undecidability could be proven.
...Building on earlier work by Kleene and constructing a Gödel numbering for lambda expressions, [Church] constructs a lambda expression e that closely follows the proof of Gödel's first incompleteness theorem. If e is applied to its own Gödel number, a contradiction results.
(Now the entire discussion about equality in lambda calculus looks pretty funny)