From 57e743e3e48508bafb145c8922f0416b21a55989 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Tue, 24 Jun 2025 18:06:02 +0100
Subject: Fix 88--90.

---
 sec/systemt.ltx | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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}
-- 
cgit v1.2.3