+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.
+
+That is, when `M` and `N` are (closed normal forms that are) syntactically distinct, there will always be some sequences of arguments <code>L<sub>1</sub>, ..., L<sub>n</sub></code> such that:
+
+<pre><code>M L<sub>1</sub> ... L<sub>n</sub> x y ~~> x
+N L<sub>1</sub> ... L<sub>n</sub> x y ~~> y
+</code></pre>
+
+That is, closed normal forms that are not just beta-reduced but also fully eta-reduced, will be syntactically different iff they yield different values for some arguments. That is, iff their extensions differ.
+
+So the proof theory with eta-reduction added is called "extensional," because its notion of normal form makes syntactic identity of closed normal forms coincide with extensional equivalence.
+
+