 Undecidability of beta equivalence

Beta equivalence is semidecidable: enumerate finite conversion proofs. It is not decidable. A proposed total numeral-valued classifier of two nonempty disjoint beta equivalence classes can be reversed by a Church Boolean selector; a self-quoting fixed point of this reversal then belongs to the opposite class from the classifier output.