Merge branch '1.11-inclusive' of https://github.com/ThePuzzlemaker/Ho…

…TT-book into ThePuzzlemaker-1.11-inclusive

preliminaries.tex

@@ -1360,7 +1360,7 @@ \section{Propositions as types}
 \end{equation}
 so we should be able to translate the above proof into an element of this type.
 
-As an example of how such a translation works, let us describe how a mathematician reading the above English proof might simultaneously construct, in his or her head, an element of~\eqref{eq:tautology2}.
+As an example of how such a translation works, let us describe how a mathematician reading the English proof above might mentally construct an element of~\eqref{eq:tautology2}.
 The introductory phrase ``Suppose not $A$ and not $B$'' translates into defining a function, with an implicit application of the recursion principle for the cartesian product in its domain $(A\to\emptyt)\times (B\to\emptyt)$.
 This introduces unnamed variables
 \index{variable}%