diff --git a/preliminaries.tex b/preliminaries.tex
index 9f37efce0..55ba08088 100644
--- a/preliminaries.tex
+++ b/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}%