From 756ce77e5a6cbbc6e996c4eec66943d2c0639b3d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= <daniel.hillerstrom@ed.ac.uk>
Date: Wed, 3 Feb 2021 22:29:38 +0000
Subject: [PATCH] Edits

---
 thesis.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/thesis.tex b/thesis.tex
index f7fa591..2add0cf 100644
--- a/thesis.tex
+++ b/thesis.tex
@@ -7541,7 +7541,7 @@ the parameter $q$.
        H = \{\Return\;x \mapsto M\} \uplus \{ \OpCase{\ell_i}{p_i}{r_i} \mapsto N_i \}_i
        \el}\\\\
        \typ{\Delta;\Gamma, q : A', x : A}{M : D}\\\\
-       [\typ{\Delta;\Gamma,q : A', p_i : A_i, r_i : B_i \to D}{N_i : D}]_i
+       [\typ{\Delta;\Gamma,q : A', p_i : A_i, r_i : \Record{B_i;A'} \to D}{N_i : D}]_i
     }
     {\typ{\Delta;\Gamma}{(q^{A'} . H) : \Record{C;A'} \Harrow^\param D}}
 \end{mathpar}