diff --git a/spec/doc.tex b/spec/doc.tex
index 6f50f5d9807d4a74d3a5dd17b7c6de71c344696b..be140d5fb4e1d6b375ed1eccc550cc865201add9 100644
--- a/spec/doc.tex
+++ b/spec/doc.tex
@@ -832,8 +832,7 @@ is always \inlineAlethe{Int}.
 For example, in standard {\smtlib}, the term \inlineAlethe{(+ 5 3)}
 has the sort \inlineAlethe{Int} in the logic \texttt{QF\_LIA}, but
 has the sort \inlineAlethe{Real} in \texttt{QF\_LRA}.
-In Alethe, this term always has the sort \inlineAlethe{Int},
-and would not be well sorted in the logic \texttt{QF\_LRA}.
+In Alethe, this term always has the sort \inlineAlethe{Int}.
 
 \paragraph{Subproofs}
 The abstract notation denotes subproofs by marking them with a vertical