diff --git a/doc/report/applications.tex b/doc/report/applications.tex
index 58c61198fe7bcd7ce7faa567c1b1761a230fec0f..f695798665d5f25fe00007ecd215b3d7347defa9 100644
--- a/doc/report/applications.tex
+++ b/doc/report/applications.tex
@@ -86,8 +86,8 @@ implementations.
 Our first query~$\mathcal{Q}_1$ illustrates how we can compute
 arithmetic scores for some nodes in our knowledge
 graph. Query~$\mathcal{Q}_1$ asks us to ``[f]ind theorems with
-non-elementary proofs.''.  Elementary proofs are those that are
-considered easy and obvious~\cite{elempro}. In
+non-elementary proofs.''.  Elementary proofs can be understood as
+those proof that are considered easy and obvious~\cite{elempro}. In
 consequence,~$\mathcal{Q}_1$ has to search for all proofs which are
 not trivial.  Of course, just like nay distinction between ``theorem''
 and ``corollary'' is going to be somewhat arbitrary, so is any