-differently with respect to them (that is, no function can behave
-differently depending on whether its argument is `M` versus `\x. M
-x`). However, the logical system you get when eta-reduction is added
-to the proof theory is importantly different from the one where only
-beta-reduction is permitted.
+differently with respect to them (that is, no function can interact differently with further arguments depending on whether it has been applied to `M` versus `\x. M x`). However, the logical system you get when eta-reduction is added to the proof theory is importantly different from the one where only beta-reduction is permitted.