+When we add eta-reduction to our proof system, we end up reconstruing the meaning of `~~>` and `<~~>` and "normal form", all in terms that permit eta-reduction as well. Sometimes these expressions will be annotated to indicate whether only beta-reduction is allowed (<code>~~><sub>β</sub></code>) or whether both beta- and eta-reduction is allowed (<code>~~><sub>βη</sub></code>).
+
+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.
+
+This implies that, 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>
+
+So closed beta-plus-eta-normal forms 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.
+
+See Hindley and Seldin, Chapters 7-8 and 14, for discussion of what should count as capturing the "extensionality" of these systems, and some outstanding issues.
+
+