Recursively enumerable fixed-point combinators
= Recursively enumerable fixed-point combinators
The set of <fixed-point combinator>[fixed-point combinators] is <recursively enumerable set>[recursively enumerable]. Enumerate closed lambda terms and finite proofs of <beta equivalence>, and output $Y$ whenever a proof of $Yf\equiv_\beta f(Yf)$ appears for a fresh variable $f$.