From 67ce9e42a269b8793e5d58f33fc9b4c5023e0946 Mon Sep 17 00:00:00 2001
From: Andreas Stadelmeier <andi@paulus.haus>
Date: Fri, 2 Feb 2024 13:22:55 +0100
Subject: [PATCH] Fixes

---
 tRules.tex |  2 +-
 unify.tex  | 10 +++++-----
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/tRules.tex b/tRules.tex
index 9c0ec22..f047468 100644
--- a/tRules.tex
+++ b/tRules.tex
@@ -302,7 +302,7 @@ $\begin{array}{l}
         \Delta = \overline{\type{X} : \bot .. \type{U}} \quad \quad 
         \Delta \vdash \ol{U}, \ol{T} \ \ok \quad \quad
         \Delta \vdash \type{N} \ \ok \quad \quad
-        \Delta \vdash \ol{M} \ \ok \texttt{in C}
+        \Delta \vdash \ol{M} \ \ok \texttt{ in C}
         \\
         \hline
     \vspace*{-0.3cm}\\
diff --git a/unify.tex b/unify.tex
index 8b2c1e4..bdccc64 100644
--- a/unify.tex
+++ b/unify.tex
@@ -1003,13 +1003,13 @@ Otherwise the generation rules \rulename{GenSigma} and \rulename{GenDelta} will
           \rulename{GenDelta}
           & $
           \deduction{
-            \wildcardEnv \vdash C \cup \set{\tv{b} \lessdot \type{N} } \implies \Delta, \sigma
+            \wildcardEnv \vdash C \cup \set{\tv{b} \lessdot \type{T} } \implies \Delta, \sigma
             }{
-            \wildcardEnv \vdash [\type{B}/\tv{b}]C \implies \Delta \cup \set{\wildcard{B}{\type{N}}{\bot}}, \sigma \cup \set{\tv{b} \to \type{B}}
+            \wildcardEnv \vdash [\type{B}/\tv{b}]C \implies \Delta \cup \set{\wildcard{B}{\type{T}}{\bot}}, \sigma \cup \set{\tv{b} \to \type{B}}
             } \quad
             \begin{array}{l}
-            \tph(\type{N}) = \emptyset, \text{fv}(\type{N}) \subseteq \Delta \cup \Delta_in \\
-            \rwildcard{B} \ \text{fresh}, \tv{b} \notin \text{dom}(\sigma), \Delta \vdash \type{N} \ \ok
+            \tph(\type{T}) = \emptyset, \text{fv}(\type{T}) \subseteq \Delta \cup \Delta_{in} \\
+            \rwildcard{B} \ \text{fresh}, \tv{b} \notin \text{dom}(\sigma), \Delta, \Delta_{in} \vdash \type{T} \ \ok
             \end{array}
           $
         \\\\ 
@@ -1041,7 +1041,7 @@ Otherwise the generation rules \rulename{GenSigma} and \rulename{GenDelta} will
       } \quad 
       \begin{array}{l}
       \tph(\type{T}) = \emptyset \\ %,\, \text{fv}(\type{T}) \subseteq \Delta \\ % T ok implies that
-      \tv{a} \notin \text{dom}(\sigma),\, \Delta, \Delta_in \vdash \type{T} \ \ok
+      \tv{a} \notin \text{dom}(\sigma),\, \Delta, \Delta_{in} \vdash \type{T} \ \ok
       \end{array}
       $
     \\\\