From 437b0c42e713774e7a27ccdc1f08770e30aeacbd Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 19 Jun 2025 00:26:46 +0100
Subject: Fix missing character warning.

---
 sec/encoding.ltx | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'sec/encoding.ltx')

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index e88a628..0c58aea 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -118,7 +118,7 @@ Given a well-formedness derivation \(\jdgmnt{ty}{\Psi}{A}\), a type
 variable \(X \in \Psi\), a type environment \(\alpha\) and a type \(S\), we
 define a term \(\mathsf{distrib}\) of type
 \[
-\submult{A}{\sub{\alpha}{X/S \to S \times \alpha(X)}} \to S \to S \times \submult{A}{\alpha}
+\suball{A}{\sub{\alpha}{X/S \to S \times \alpha(X)}} \to S \to S \times \suball{A}{\alpha}
 \]
 that calls each accumulator within \(A\) in sequence.  The definition
 is by induction on the well-formedness derivation of \(A\). The
-- 
cgit v1.2.3

