diff --git a/relatedwork.tex b/relatedwork.tex
index b00b6bb..e7e2c25 100644
--- a/relatedwork.tex
+++ b/relatedwork.tex
@@ -63,14 +63,14 @@ indeed the transitiv closure of $\QMextends{\theta} \sub \theta'$ and $\theta' \
 algorithm for this type system, which he proved as sound and complete. 
 
 The problem of his type system is in the lossing reflexivity as shown in
-example \ref{intro-example1}. First approaches to solve this problem he gave in
+example \ref{lst:intro-example-typeless}. First approaches to solve this problem he gave in
 \cite{plue24_1}, where he fixes that no pairwise different nodes in the
 abstract syntax gets the same type variable and that no pairwise different type
 variables are equalized. In \cite{PH23} he showed how his type inference
 algorithm suffices theese properties.
 
-In Pl\"umicke's work there is indeed a formal definition of the subtying
-ordering and a correctness proof of the type unification algorithms but no
-soundness proof of the type system, itself. Therefore we choose for our type
-inference algorithms with wildcars the approach of ???????
+% In Pl\"umicke's work there is indeed a formal definition of the subtying
+% ordering and a correctness proof of the type unification algorithms but no
+% soundness proof of the type system, itself. Therefore we choose for our type
+% inference algorithms with wildcars the approach of ???????
 
diff --git a/soundness.tex b/soundness.tex
index 7a5e547..5d0e224 100644
--- a/soundness.tex
+++ b/soundness.tex
@@ -95,21 +95,21 @@
     \unify{}'s type solutions for a constraint set generated by $\typeExpr{}$ are correct.
     \begin{description}
     \item[if] $\typeExpr{}(\mtypeEnvironment{}, \texttt{e}, \tv{a}) = (\Delta', C)$
-    and $(\Delta_u, \sigma) = \unify{}(\Delta', C)$ and let $\Delta= \Delta_u \cup \Delta'$
-    $\Delta, \Delta' \vdash $
+    and $(\Delta_u, \sigma) = \unify{}(\Delta', C)$ % and let $\Delta= \Delta_u \cup \Delta'$
+%    $\Delta, \Delta' \vdash $
 %    , with $C = \set{ \overline{ \type{S} \lessdot \type{T} } \cup \overline{ \type{S'} \lessdotCC \type{T'} } }$
 %    and $\vdash \ol{L} : \mtypeEnvironment{}$
 %    and $\Gamma \subseteq \mtypeEnvironment{}$
 %    \item[given] a $(\Delta, \sigma)$ with $\Delta \vdash \overline{\sigma(\type{S}) <: \sigma(\type{T})}$
 %    and there exists a $\Delta'$ with $\Delta, \Delta' \vdash \overline{\CC{}(\sigma(\type{S'})) <: \sigma(\type{T'})}$
     %\item[then] there is a completion $|\texttt{e}|$ with $\Delta|\Gamma  \vdash |\texttt{e}| : \sigma(\tv{a})$
-    \item[then] $\Delta|\Gamma  \vdash \texttt{e} : \sigma(\tv{a})$
+    \item[then] $\Delta,\Delta'|\Gamma  \vdash \texttt{e} : \sigma(\tv{a})$
     \end{description}
 \end{lemma}
-Regular type placeholders represent type annotations.
-These are the only types a \wildFJ{} program needs to be correctly typed.
-The type placeholders flagged as wildcard placeholders are intermediate types
-used in let statements and as type parameters for generic method calls.
+% Regular type placeholders represent type annotations.
+% These are the only types a \wildFJ{} program needs to be correctly typed.
+% The type placeholders flagged as wildcard placeholders are intermediate types
+% used in let statements and as type parameters for generic method calls.
 
 %Unify needs to return S aswell and guarantee that the \Delta' environment are the wildcards
 % only used inside the constraint the wildcard variable occurs
@@ -121,33 +121,44 @@ used in let statements and as type parameters for generic method calls.
 By structural induction over the expression $\texttt{e}$. 
 \begin{description}
     \item[$\texttt{let}\ \texttt{x} = \texttt{t}_1 \ \texttt{in}\ \expr{t}_2$]
-        $\Delta|\Gamma \vdash \expr{t}_1: \type{T}_1$ by assumption.
-        The body of the let statement will only use the free variables provided by $\Delta$ and $\Delta'$ (see lemma \ref{lemma:wildcardsStayInScope}).
+    $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$ by lemma \ref{lemma:wildcardWellFormedness}.
+    $\Delta \vdash \type{T}, \wcNtype{\Delta'}{N} \ \ok$ by lemma \ref{lemma:unifyWellFormedness}.
+        $\Delta|\Gamma \vdash \expr{t}_1: \sigma(\tv{e}_1)$ by assumption.
+        $\Delta \vdash \sigma(\tv{e}_1) <: \wcNtype{\Delta'}{N}$ by constraint $\tv{e}_1 \lessdot \tv{x}$ and lemma \ref{lemma:unifySoundness}.
+        The body of the let statement will only use the free variables provided by $\Delta$ and $\Delta'$.
+        We can prove this by lemma \ref{lemma:tvsNoFV} and the fact that the wildcard placeholders used generated the body of the let statement are not used outside of it.
+        Therefore we can say $\Delta,\Delta' | \Gamma, \expr{x}:\type{N} \vdash \expr{t}_2 : \sigma(\tv{e}_2)$ by assumption
+        and $\Delta, \Delta' \vdash  \sigma(\tv{e}_2) <: \sigma(\tv{a})$ by lemma \ref{lemma:unifySoundness}
+        given the constraint $\tv{e}_2 \lessdot \tv{a}$.
     \item[$\expr{v}.\texttt{f}$]
         We are alowwed to use capture conversion for $\expr{v}$ here.
-
-    \item[$\texttt{let}\ \texttt{x} = \texttt{e} \ \texttt{in} \ \texttt{x}.\texttt{f}$] 
-    $\Delta|\Gamma \vdash \expr{e}: \type{T}$ by assumption.
-    $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$ by lemma \ref{lemma:wildcardWellFormedness}.
-    $\Delta, \Delta' | \Gamma, \expr{x} : \type{T} \vdash \texttt{x}.\texttt{f}$
-    \item[$\texttt{e}.\texttt{f}$] Let $\sigma(\tv{r}) = \wcNtype{\Delta_c}{N}$,
-    then $\Delta|\Gamma  \vdash \texttt{e} : \wcNtype{\Delta_c}{N}$ by assumption.
-    $\Delta', \Delta, \Delta_c \vdash \type{N} <: \sigma(\exptype{C}{\overline{\wtv{a}}})$ by premise.
-    %Let $\sigma(\tv{r}) = \wcNtype{\Delta'}{N}$.
-    %Let $\sigma([\ol{\wtv{a}}/\ol{X}]\type{T}) = \wcNtype{\Delta_t}{N_t}$.
+        $\Delta \vdash \expr{v} : \sigma(\tv{a})$ by assumption.
+        $\Delta \vdash \sigma(\tv{a}) <: \sigma(\exptype{C}{\ol{\wtv{a}}})$ and
+        $\Delta \vdash \type{U}_i <: \sigma(\tv{a})$,
+    because of the constraints $[\overline{\wtv{a}}/\ol{X}]\type{T} \lessdot \tv{a}$, $\tv{r} \lessdotCC \exptype{C}{\ol{\wtv{a}}}$ and lemma \ref{lemma:unifySoundness}.
+    $\textit{fields}(\sigma(\exptype{C}{\overline{\wtv{a}}})) = \sigma([\overline{\wtv{a}}/\ol{X}]\type{T})$.
+    % \item[$\texttt{let}\ \texttt{x} = \texttt{e} \ \texttt{in} \ \texttt{x}.\texttt{f}$] 
+    % $\Delta|\Gamma \vdash \expr{e}: \type{T}$ by assumption.
+    % $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$ by lemma \ref{lemma:wildcardWellFormedness}.
+    % $\Delta, \Delta' | \Gamma, \expr{x} : \type{T} \vdash \texttt{x}.\texttt{f}$
+    % \item[$\texttt{e}.\texttt{f}$] Let $\sigma(\tv{r}) = \wcNtype{\Delta_c}{N}$,
+    % then $\Delta|\Gamma  \vdash \texttt{e} : \wcNtype{\Delta_c}{N}$ by assumption.
+    % $\Delta', \Delta, \Delta_c \vdash \type{N} <: \sigma(\exptype{C}{\overline{\wtv{a}}})$ by premise.
+    % %Let $\sigma(\tv{r}) = \wcNtype{\Delta'}{N}$.
+    % %Let $\sigma([\ol{\wtv{a}}/\ol{X}]\type{T}) = \wcNtype{\Delta_t}{N_t}$.
     
-    The completion of $|\texttt{e}.\texttt{f}|$ is $\texttt{let}\ \texttt{x} = \texttt{e} : \wcNtype{\Delta_c}{N}\ \texttt{in} \ \texttt{x}.\texttt{f}$
+    % The completion of $|\texttt{e}.\texttt{f}|$ is $\texttt{let}\ \texttt{x} = \texttt{e} : \wcNtype{\Delta_c}{N}\ \texttt{in} \ \texttt{x}.\texttt{f}$
     
-    We now show
-    $\Delta|\Gamma \vdash \texttt{let}\ \texttt{x} = \texttt{e} : \wcNtype{\Delta_c}{N}\ \texttt{in} \ \texttt{x}.\texttt{f} : \sigma(a)$
-    by the T-Field rule.
-    $\Delta \vdash \wcNtype{\Delta_c}{N} <: \wcNtype{\Delta_c}{N}$ by S-Refl.
-    $\Delta, \Delta_c \vdash \type{U}_i <: \sigma(\tv{a})$,
-    because of the constraint $[\overline{\wtv{a}}/\ol{X}]\type{T} \lessdot \tv{a}$ and lemma \ref{lemma:unifySoundness}.
-    $\textit{fields}(\sigma(\exptype{C}{\overline{\wtv{a}}})) = \sigma([\overline{\wtv{a}}/\ol{X}]\type{T})$
-    and $\text{fv}(\type{U}_i) \subseteq \text{fv}(\type{N})$ by definition of $\textit{fields}$.
+    % We now show
+    % $\Delta|\Gamma \vdash \texttt{let}\ \texttt{x} = \texttt{e} : \wcNtype{\Delta_c}{N}\ \texttt{in} \ \texttt{x}.\texttt{f} : \sigma(a)$
+    % by the T-Field rule.
+    % $\Delta \vdash \wcNtype{\Delta_c}{N} <: \wcNtype{\Delta_c}{N}$ by S-Refl.
+    % $\Delta, \Delta_c \vdash \type{U}_i <: \sigma(\tv{a})$,
+    % because of the constraint $[\overline{\wtv{a}}/\ol{X}]\type{T} \lessdot \tv{a}$ and lemma \ref{lemma:unifySoundness}.
+    % $\textit{fields}(\sigma(\exptype{C}{\overline{\wtv{a}}})) = \sigma([\overline{\wtv{a}}/\ol{X}]\type{T})$
+    % and $\text{fv}(\type{U}_i) \subseteq \text{fv}(\type{N})$ by definition of $\textit{fields}$.
 
-    $\text{dom}(\Delta_c) \subseteq \text{fv}{\type{N}}$ by lemma \ref{lemma:tvsNoFV}.
+    % $\text{dom}(\Delta_c) \subseteq \text{fv}{\type{N}}$ by lemma \ref{lemma:tvsNoFV}.
 
     % X.List<X> <. List<a?>
     % $\sigma(\ol{\tv{r}}) = \overline{\wcNtype{\Delta}{N}}$,
@@ -183,55 +194,65 @@ By structural induction over the expression $\texttt{e}$.
     % %Easy, because unify only generates substitutions for normal type placeholders which are OK
 
     \item[$\texttt{e}.\texttt{m}(\ol{e})$]
-Lets have a look at the case where the receiver and parameter types are all named types.
-So $\sigma(\ol{\tv{r}}) = \ol{T} = \ol{\wcNtype{\Delta_u}{N}}$ and $\sigma(\tv{r}) = \type{T}_r = \wcNtype{\Delta_u}{N}$
-and a $\Delta'$, $\overline{\Delta}$ where $\Delta' \subseteq \Delta_u$, $\overline{\Delta \subseteq \Delta_u}$
-and $\text{dom}(\Delta') = (\text{fv}(\type{N})/\Delta)$, $\overline{\text{dom}(\Delta) = (\text{fv}(\type{N})/\Delta)}$  in
+    Proof is analog to field access, except the $\Delta \vdash \ol{S}\ \ok$ premise.
+    We know that $\unify{}(\Delta, [\overline{\wtv{b}}/\ol{Y}]\set{
+        \ol{\tv{e}} \lessdotCC \ol{T}, \type{T} \lessdot \tv{a}, 
+        \ol{Y} \lessdot \ol{N} } \cup C) = (\Delta', \sigma)$
+        and if we assume $\sigma(\ol{\tv{e}}) = \ol{\wcNtype{\Delta}{N'}}$
+        then the call to $\unify{}(\Delta \cup \overline{\Delta}, [\overline{\ntv{b}}/\ol{Y}]\set{
+            \ol{N'} \lessdot \ol{T}, \type{T} \lessdot \tv{a}, 
+            \ol{Y} \lessdot \ol{N} } \cup C)$ succeeds with $\overline{\ntv{b}}$ being normal placeholders this time,
+            which proofs $\Delta \vdash \ol{S}\ \ok$ via lemma \ref{lemma:unifyWellFormedness}.
+            %TODO: why does this call succeed?
+% Lets have a look at the case where the receiver and parameter types are all named types.
+% So $\sigma(\ol{\tv{r}}) = \ol{T} = \ol{\wcNtype{\Delta_u}{N}}$ and $\sigma(\tv{r}) = \type{T}_r = \wcNtype{\Delta_u}{N}$
+% and a $\Delta'$, $\overline{\Delta}$ where $\Delta' \subseteq \Delta_u$, $\overline{\Delta \subseteq \Delta_u}$
+% and $\text{dom}(\Delta') = (\text{fv}(\type{N})/\Delta)$, $\overline{\text{dom}(\Delta) = (\text{fv}(\type{N})/\Delta)}$  in
 
-$\texttt{let}\ \texttt{x} : \wcNtype{\Delta'}{N} = \texttt{e} \ \texttt{in}\ 
-\texttt{let}\ \ol{x} : \overline{\wcNtype{\Delta'}{N}} = \ol{e} \ \texttt{in}\ \texttt{x}.\texttt{m}(\ol{x})$
+% $\texttt{let}\ \texttt{x} : \wcNtype{\Delta'}{N} = \texttt{e} \ \texttt{in}\ 
+% \texttt{let}\ \ol{x} : \overline{\wcNtype{\Delta'}{N}} = \ol{e} \ \texttt{in}\ \texttt{x}.\texttt{m}(\ol{x})$
 
-%TODO: show that this type exists \wcNtype{\Delta'}{N} (a \Delta' which only contains free variables of the type N)
-% and which is a supertype of T_r (so no free variables in T_r)
-% Solution: Make this a lemma and guarantee that Unify does only create types Delta.T with \Delta subset fv(T)
-% This is possible because free variables (except those in \Delta_in) are never used in wildcard environments
+% %TODO: show that this type exists \wcNtype{\Delta'}{N} (a \Delta' which only contains free variables of the type N)
+% % and which is a supertype of T_r (so no free variables in T_r)
+% % Solution: Make this a lemma and guarantee that Unify does only create types Delta.T with \Delta subset fv(T)
+% % This is possible because free variables (except those in \Delta_in) are never used in wildcard environments
 
-%By lemma \ref{lemma:unifyWeakening}
-We know that 
-$\unify{}(\Delta, [\ol{\tv{a}}/\ol{X}][\ol{\tv{b}}/\ol{Y}]\set{ \overline{\wcNtype{\Delta}{N}} \lessdotCC \ol{T}, \wcNtype{\Delta'}{N} \lessdotCC \exptype{C}{\ol{X}}})$
-has a solution.
-Also $\overline{\wcNtype{\Delta}{N}} \lessdot \ol{T}$ and $\wcNtype{\Delta'}{N} \lessdotCC \exptype{C}{\ol{X}}$ will be converted to 
-$\ol{N} \lessdot \ol{T}$ and $\type{N} \lessdot \exptype{C}{\ol{X}}$ by the \rulename{Capture} rule.
-Which then results in the same as calling $\unify{}((\Delta, \Delta', \overline{\Delta}), [\ol{\tv{a}}/\ol{X}][\ol{\tv{b}}/\ol{Y}]\set{\ol{N} \lessdot \ol{T}, \type{N} \lessdot \exptype{C}{\ol{X}}})$,
-which shows $\Delta, \Delta', \overline{\Delta} \vdash \overline{N} <: [\ol{S}/\ol{X}]\overline{U}$.
+% %By lemma \ref{lemma:unifyWeakening}
+% We know that 
+% $\unify{}(\Delta, [\ol{\tv{a}}/\ol{X}][\ol{\tv{b}}/\ol{Y}]\set{ \overline{\wcNtype{\Delta}{N}} \lessdotCC \ol{T}, \wcNtype{\Delta'}{N} \lessdotCC \exptype{C}{\ol{X}}})$
+% has a solution.
+% Also $\overline{\wcNtype{\Delta}{N}} \lessdot \ol{T}$ and $\wcNtype{\Delta'}{N} \lessdotCC \exptype{C}{\ol{X}}$ will be converted to 
+% $\ol{N} \lessdot \ol{T}$ and $\type{N} \lessdot \exptype{C}{\ol{X}}$ by the \rulename{Capture} rule.
+% Which then results in the same as calling $\unify{}((\Delta, \Delta', \overline{\Delta}), [\ol{\tv{a}}/\ol{X}][\ol{\tv{b}}/\ol{Y}]\set{\ol{N} \lessdot \ol{T}, \type{N} \lessdot \exptype{C}{\ol{X}}})$,
+% which shows $\Delta, \Delta', \overline{\Delta} \vdash \overline{N} <: [\ol{S}/\ol{X}]\overline{U}$.
 
-    This implies $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$ and $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$
-    $\Delta, \Delta', \overline{\Delta} \vdash [\ol{S}/\ol{X}]\type{U} \type{T}$,
-    $\Delta, \Delta', \overline{\Delta} \vdash \ol{N} <: [\ol{S}/\ol{X}]\ol{U}$,
-    and $\Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}$
-    are guaranteed by the generated constraints and lemma \ref{lemma:unifySoundness}.% and \ref{lemma:unifyCC}.
-    $\Delta, \Delta' \vdash \ol{T} <: \ol{\wcNtype{\Delta}{N}}$ due to $\ol{T} = \ol{\wcNtype{\Delta}{N}}$ and S-Refl. $\Delta, \Delta' \vdash \type{T}_r <: \wcNtype{\Delta'}{N}$ accordingly.
-    $\Delta|\Gamma \vdash \texttt{t}_r : \type{T}_r$ and $\Delta|\Gamma \vdash \ol{t} : \ol{T}_r$ by assumption.
-    $\Delta, \Delta' \vdash \ol{\wcNtype{\Delta}{N}} \ \ok$ by lemma \ref{lemma:unifyWellFormedness},
-    therefore $\Delta, \Delta', \overline{\Delta} \vdash \ol{N} \ \ok$, which implies $\Delta, \Delta', \overline{\Delta} \vdash \ol{U} \ \ok$
-    %by lemma \ref{lemma:wfHereditary}
-    and $\Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok $ by premise of WF-Class.
-    The same goes for $\wcNtype{\Delta'}{N}$.
+%     This implies $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$ and $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$
+%     $\Delta, \Delta', \overline{\Delta} \vdash [\ol{S}/\ol{X}]\type{U} \type{T}$,
+%     $\Delta, \Delta', \overline{\Delta} \vdash \ol{N} <: [\ol{S}/\ol{X}]\ol{U}$,
+%     and $\Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}$
+%     are guaranteed by the generated constraints and lemma \ref{lemma:unifySoundness}.% and \ref{lemma:unifyCC}.
+%     $\Delta, \Delta' \vdash \ol{T} <: \ol{\wcNtype{\Delta}{N}}$ due to $\ol{T} = \ol{\wcNtype{\Delta}{N}}$ and S-Refl. $\Delta, \Delta' \vdash \type{T}_r <: \wcNtype{\Delta'}{N}$ accordingly.
+%     $\Delta|\Gamma \vdash \texttt{t}_r : \type{T}_r$ and $\Delta|\Gamma \vdash \ol{t} : \ol{T}_r$ by assumption.
+%     $\Delta, \Delta' \vdash \ol{\wcNtype{\Delta}{N}} \ \ok$ by lemma \ref{lemma:unifyWellFormedness},
+%     therefore $\Delta, \Delta', \overline{\Delta} \vdash \ol{N} \ \ok$, which implies $\Delta, \Delta', \overline{\Delta} \vdash \ol{U} \ \ok$
+%     %by lemma \ref{lemma:wfHereditary}
+%     and $\Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok $ by premise of WF-Class.
+%     The same goes for $\wcNtype{\Delta'}{N}$.
 
-    % \begin{gather}
-%         \label{sp:0}
-%         \Delta, \Delta', \overline{\Delta} \vdash [\ol{S}/\ol{X}]\type{U} \type{T} \\
-%         \label{sp:1}
-%         \Delta, \Delta', \overline{\Delta} \vdash \ol{N} <: [\ol{S}/\ol{X}]\ol{U} \\
-%         \label{sp:2}
-%         \Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'} \\
-%         \label{sp:3}
-%         \Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok \\
-%         \label{sp:4}
-%         \Delta, \Delta' \vdash \ol{T} <: \ol{\wcNtype{\Delta}{N}}
-%     \end{gather}
+%     % \begin{gather}
+% %         \label{sp:0}
+% %         \Delta, \Delta', \overline{\Delta} \vdash [\ol{S}/\ol{X}]\type{U} \type{T} \\
+% %         \label{sp:1}
+% %         \Delta, \Delta', \overline{\Delta} \vdash \ol{N} <: [\ol{S}/\ol{X}]\ol{U} \\
+% %         \label{sp:2}
+% %         \Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'} \\
+% %         \label{sp:3}
+% %         \Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok \\
+% %         \label{sp:4}
+% %         \Delta, \Delta' \vdash \ol{T} <: \ol{\wcNtype{\Delta}{N}}
+% %     \end{gather}
 
-Method calls generate multiple constraints that share the same wildcard placeholders ($\ol{\wtv{a}}$, $\ol{\wtv{b}}$).
+% Method calls generate multiple constraints that share the same wildcard placeholders ($\ol{\wtv{a}}$, $\ol{\wtv{b}}$).
 
 \end{description}
 
@@ -333,15 +354,14 @@ Trivial. \unify{} fails when a constraint $\tv{a} \doteq \rwildcard{X}$ arises.
 % Delta |-  N <. T
 % \end{lemma}
 
-\begin{lemma}\label{lemma:wildcardsStayInScope}
-Free variables can only hop to another constraint if they share the same wildcard placeholder.
-\begin{description}
-    \item[If] $(\sigma, \Delta) = \unify{} (\Delta', C \cup \set{\wcNtype{\Delta'}{N} \lessdot \tv{a}})$
-    \item[and] $\tv{a}$ being a type placeholders used in $C$
-    \item[then] $\text{fv}(\sigma(\tv{a})) \subseteq \Delta, \Delta'$
-\end{description}
-If $\wcNtype{\Delta'}{N} \lessdot \tv{a}$
-\end{lemma}
+% \begin{lemma}\label{lemma:wildcardsStayInScope}
+% Free variables can only hop to another constraint if they share the same wildcard placeholder.
+% \begin{description}
+%     \item[If] $(\sigma, \Delta) = \unify{} (\Delta', C \cup \set{\wcNtype{\Delta'}{N} \lessdot \tv{a}})$
+%     \item[and] $\tv{a}$ being a type placeholders used in $C$
+%     \item[then] $\text{fv}(\sigma(\tv{a})) \subseteq \Delta, \Delta'$
+% \end{description}
+% \end{lemma}