Fix 88--90.

1 files changed, 2 insertions, 1 deletions

diff --git a/sec/systemt.ltx b/sec/systemt.ltx
index 309de0f..a1141ab 100644
--- a/sec/systemt.ltx
+++ b/sec/systemt.ltx
@@ -75,7 +75,8 @@ argument form \(\epsilon\) (the empty list), and the type \(\nat \to \nat \to
 
 All System~T types are inhabited.\@ \nat{} is inhabited by zero, and
 any function type is inhabited when its codomain is inhabited by
-taking the constant function.
+taking the constant function. \textcite{syst-sn} proves all System~T
+terms are strongly normalising.
 
 \subsection{Strategies for Encoding Inductive Types}%
 \label{subsec:encoding-strategies}