Friedman showed in 1975 that this interpretation is complete for β η {\displaystyle \beta \eta } -equivalence, if the base types are interpreted by infinite sets.
Friedman 在 1975 年证明这种解释是对 β η {\displaystyle \beta \eta } -等价是完备的，如果基本类型被解释为无限集合。