From eb05d04ae851e5d7eedb9684c37074e7d2cefa67 Mon Sep 17 00:00:00 2001
From: JanUlrich <andi@michlaustderaffe.de>
Date: Sun, 4 Aug 2024 22:06:02 +0200
Subject: [PATCH] Fix

---
 soundness.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/soundness.tex b/soundness.tex
index 3192f93..d4811d8 100644
--- a/soundness.tex
+++ b/soundness.tex
@@ -86,10 +86,10 @@ We have to show T-Let and T-Call which leaves us with:
 \begin{itemize}
     \item $\Delta | \Gamma \vdash \expr{e} : \sigma(\tv{e})$ and $\Delta | \Gamma \vdash \overline{\expr{e} : \sigma(\tv{e})}$ by assumption
     \item $\Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N}$ and $\Delta \vdash \overline{\type{T}_1 <: \wcNtype{\Delta'}{N}}$ by constraints $\tv{e} \lessdot \tv{x}$, $\overline{\tv{e} \lessdot \tv{x}}$ and lemma \ref{lemma:unifySoundness}
-    \item $\Delta, \Delta', \ol{\Delta'} | \Gamma, \expr{x} : \type{N}, \overline{\expr{x} : \type{N}} \vdash \expr{x}.\texttt{m}(\ol{x}) : \sigma(\tv{r})$ by T-Call, because the following promises are satisfied
+    \item $\Delta, \Delta', \overline{\Delta'} | \Gamma, \expr{x} : \type{N}, \overline{\expr{x} : \type{N}} \vdash \expr{x}.\texttt{m}(\ol{x}) : \sigma(\tv{r})$ by T-Call, because the following promises are satisfied
     \begin{itemize}
         \item $\generics{\ol{X} \triangleleft \ol{U'}} \ol{U} \to \type{U} \in \Pi(\texttt{m})$ is given, otherwise the program fails at the constraint generation step.
-        \item $\Delta \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}$ by constraints $\ol{\wtv{b}} \lessdot \ol{N}$ and lemma \ref{lemma:unifySoundness}
+        \item $\Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}$ by constraints $\ol{\wtv{b}} \lessdot [\ol{\wtv{b}}/\ol{X}]\ol{N}$ and lemma \ref{lemma:unifySoundness}
         TODO: does not work because left side is a wildcard variable (maybe just change lemma soundness a bit)
     \end{itemize}
 \end{itemize}