The logical system you get when eta-reduction is added to the proof system has the following property:
> if `M`, `N` are normal forms with no free variables, then <code>M ≡ N</code> iff `M` and `N` behave the same with respect to every possible sequence of arguments.
The logical system you get when eta-reduction is added to the proof system has the following property:
> if `M`, `N` are normal forms with no free variables, then <code>M ≡ N</code> iff `M` and `N` behave the same with respect to every possible sequence of arguments.