Statman showed in 1983 that β η {\displaystyle \beta \eta } -equivalence is the maximal equivalence which is typically ambiguous, i.e. closed under type substitutions (Statman's Typical Ambiguity Theorem).
Statman 在 1983 年证明 β η {\displaystyle \beta \eta } -等价是极大等价，它是典型歧义的，就是说，在类型替换下闭合(Statman's Typical Ambiguity Theorem)。