2. The argument formerly used a direct port of the original
Diaconescu proof as presented in Beeson's "Foundations of
Constructive Mathematics". But in July 2009 I changed it to a
somewhat optimized variant shown to me by Mark Adams. This is
noted in the CHANGES fil
Thanks, John and Rob! The main problem I'm having is actually embarrassingly
simple: I don't understand the typed Lambda Calculus angle in Church's work or
HOL. Now I definitely see the point of having functions as well as sets, and
that means that the HOL type theory (sets are either types or
