Changed beta-reduction to computation rule and eta-expansion to uniqueness
principle everywhere.  Renamed the principle of surjective pairing, too.  It's
all indexed, too, so a convenient way to verify what I've done is to look at
the index entries for the two new terms.  Actually, there is also a third new
term: propositional uniqueness principle.  Now the two old terms only occur in
a pair of footnotes.

( #233, #94 )

I'll keep it open so people can verify it's okay.