Typed lambda-calculus in classical Zermelo-Fraenkel set theory (Q5945009)

In this paper the author introduces ``\(\text{ZF}_\varepsilon\) set theory'' which, he claims, includes all of ZF + AF. However, his proof of the substitutivity for equality is not complete, so it is not clear whether his claim is justified. He then develops \(\text{ZF}_\varepsilon\) set theory within a classical extension of lambda calculus.