\section{Soundness}

\newcommand{\CC}{\text{CC}}

\begin{theorem}\label{testenv-theorem}
Type inference produces a correctly typed program.
\begin{description}
    \item[If] $\fjtypeinference(\mv{\Pi}, \texttt{class}\ \exptype{C}{\ol{X}
    \triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M} \}) = \mtypeEnvironment{}'$
    \item[Then] $\texttt{class}\ \exptype{C}{\ol{X}
    \triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M} \} \text{ok}$,
    with $\ol{M} = $
\end{description}
\end{theorem}

\begin{lemma}{Well-formedness:}
TODO: 
\end{lemma}

\begin{lemma}{Soundness:}
    \unify{}'s type solutions for a constraint set generated by $\typeExpr{}$ are correct.
    \begin{description}
    \item[if] $\typeExpr{}(\mtypeEnvironment{}, \texttt{e}, \tv{a}) = C$
    and $(\Delta, \sigma) = \unify{}(\Delta', C)$
%    , 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] $\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.

%Unify needs to return S aswell and guarantee that the \Delta' environment are the wildcards
% only used inside the constraint the wildcard variable occurs
% should Unify also return the \Delta' environment? Otherwise the bounds of free wildcard variables are lost

% Or is it possible to deduct the right \ol{S} directly from the types in the normal TPHs?

\textit{Proof:}
By structural induction over the expression $\texttt{e}$.
\begin{description}
    \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}$
    
    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}.

    % X.List<X> <. List<a?>
    % $\sigma(\ol{\tv{r}}) = \overline{\wcNtype{\Delta}{N}}$,
    % $\ol{N} <: [\ol{S}/\ol{X}]\ol{U}$,
    % TODO: S ok? We could proof $\Delta, \Delta' \overline{\Delta} \vdash \ol{S} \ \ok$
    % by proofing every substitution in Unify is ok aslong as every type in the inputs is ok
    % S ok when all variables are in the environment and every L <: U and U <: Class-bound
    % This can be given by the constraints generated. We can proof if T ok and S <: T and T <: S' then S ok and S' ok

    % If S ok and T <. S , then Unify generates a T ok
    S typeinference:
    T <: [S/Y]U
    We apply the following lemma
    Lemma
    if T ok and T <: S then S ok

    until
    T = [S/Y]U

    and then we can say by 
    Lemma:
    If [S/Y]U ok then S ok (TODO: proof!)

    So we do not have to proof S ok (but T)

    % T_r <: C<T> (S is in T)
    % Is C<T> ok?
    % if every type environment \Delta supplied to Unify is ok (L <: U), then \sigma(a) = \Delta'.N implies \Delta' conforms to (L <: U)
    % this together with the X <. N constraints proofs T_r ok

    $\Delta \vdash \sigma(\tv{a}), \wcNtype{\Delta_c}{N} \ \ok$ %TODO
    %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}{N}}$ and $\sigma(\tv{r}) = \type{T}_r = \wcNtype{\Delta'}{N}$:
    \begin{gather}
        \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'} \\
        \Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok \\
        \label{sp:4}
        \Delta, \Delta' \vdash \ol{T} <: \ol{\wcNtype{\Delta}{N}}
    \end{gather}
    \ref{sp:1} is guaranteed by the constraints $\ol{r} \lessdot \ol{T}$.
    $\ol{\tv{r}} \lessdot \ol{T}$ says that there is a $\Delta'$ with 
    $\Delta, \Delta' \vdash CC(\sigma(\tv{r})) <: \type{T}$.

    If $\overline{\sigma(\tv{r}) = \wcNtype{\Delta}{N}}$
    then \ref{sp:1} due to lemma \ref{lemma:unifyCC}.
    Let $\sigma(\ol{\tv{r}}) = \ol{T} = \ol{\wcNtype{\Delta}{N}}$, then
    \ref{sp:4} by lemma \ref{lemma:unifySoundness} and \ref{lemma:tvsNoFV}.
    The environments $\overline{\Delta}$ are not needed,
    because none of the variables in $\text{dom}(\overline{\Delta})$ are used in $\ol{T}$ or $\Delta, \Delta'$.

\ref{sp:3}
%TODO: S is not in \sigma. They are generated by a local type inference algorithm

Method calls generate multiple constraints that share the same wildcard placeholders ($\ol{\wtv{a}}$, $\ol{\wtv{b}}$).
%TODO: show that only those wildcards in the parameters and receiver type are used ($\ol{\Delta}$)

    % X.List<X> <. List<a?>
    % set \sigma(r) = X.N
    % If there exists a subtype r <: T, then r <: X.N, N <: T with X.N == r
    % If  CC(X.N) <: T, then N <: T
    % R <: X.N due to S-Refl.
    % \Delta, X \vdash N <: T due to assumption and S-Exists.
    % What if X.N <: Y (where is this Y coming from?)
    % %TODO:
    % We have to show, that all constraints using the same wtv's C = X1.T1 <. X2.T2 ,...
    % with a? \in T1, T2, ....
    % then \Delta' \subseteq X1, X2, ... for \Delta, \Delta \vdash sigma(T1) <: sigma(X2.T2), ....

    % when only wildcards in the top level domain from the constraints involving the a? variables are involved
    % then they are all contained in $\Delta, \Delta', \overline{Delta}$, which makes S ok true! (does it?)
    % and due to r <. T, the judgements N <: [S/X]U and T_r <: \Delta.N are true!

    % If $\ol{\tv{r}} \lessdot \ol{T}$ how can we say that \Delta' only uses
\end{description}

% \begin{lemma} Unify does add free variables to types not containing free variables (or wildcard placeholders)
% \begin{description}
%     \item[If] $(\sigma, \Delta) = \unify{}( \Delta', C )$
%     \item[Then] $\forall x \in \set{\type{S} \mid \type{S} \in C, \text{fv}(\type{S}) = \emptyset }: \text{fv}(\sigma(\type{S})) \subseteq \text{dom}(\Delta)$
% \end{description}
% \end{lemma}
% \textit{Proof:} by induction over the \unify{} algorithm.
% A unifier $\sigma(\tv{a}) = \type{T}$, where the type variable $\tv{a}$ is not flagged as a wildcard will always hold
% $\text{fv}(\type{T}) \subseteq \text{dom}(\Delta)$.
% %UNIFY fails when there are free variables on the right side of a a =. T constraint

\begin{lemma}
\unify{} generates well-formed types as long as well-formed types are supplied.
\begin{description}
\item[If] $(\Delta, \sigma) = \unify{}(\Delta', C)$ and $\sigma(\tv{a}) = \wcNtype{\ol{\wildcard{X}{\type{U}}{\type{L}}}}{N}$
\item[and] $\forall \wcNtype{\Delta}{N} \in C: \ \Delta' \vdash \wcNtype{\Delta}{N} \ \ok$ 
\item[then] $\Delta \vdash \ol{L <: U}$ and $\Delta \vdash \ol{U <: U'}$ % (with U' being upper limit by class definition)
\end{description}
\end{lemma}
Only the \rulename{General} rule generates fresh wildcards.
By lemma \ref{lemma:unifySoundness} we get $\Delta \vdash $
By S-Exists and S-Trans 

% All types supplied to the Unify algorithm by TYPEs only contain ? extends or ? super wildcards. (X : [bot..T] or X : [T .. Object]).
% Both are well formed!

\begin{lemma}
    Well-formedness is hereditary
    \begin{description}
        \item[If] $\triangle \vdash \exptype{C}{\ol{X}} \ \ok$ and $\triangle \vdash \exptype{C}{\ol{X}} <: \type{S}$
        \item[Then] $\triangle \vdash \type{S} \ \ok$
    \end{description}
\end{lemma}
\textit{Proof:}

\begin{lemma}
    
    \begin{description}
        \item[If] $\Delta \vdash \wctype{\Delta'}{C}{\ol{T}} \ \ok$
        \item[Then] $\Delta, \Delta' \vdash \ok{T} \ \ok$
    \end{description}
\end{lemma}
\textit{Proof:} by definition of WF-Class


\begin{lemma} \label{lemma:tvsNoFV}
    \unify{} does not add free variables to types not containing free variables.
    \begin{description}
        \item[If] $(\sigma, \Delta) = \unify{} (\Delta', C)$
        \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}
\textit{Proof:}
Trivial. \unify{} fails when a constraint $\tv{a} \doteq \rwildcard{X}$ arises.

\begin{lemma} \label{lemma:unifyCC}
Free variables do not leave their scope. TODO
Wildcard variables are only substituted by wildcards inside the same constraint.

\begin{description}
    \item[If] $(\sigma, \Delta) = \unify{}( C \cup \set{ \type{T} \lessdot \type{S} } \cup \set{ \overline{\type{T} \lessdotCC \type{S} } } )$
    \item[and] $\text{fv}(\type{T}, \type{S}) \subseteq \text{fv}(\ol{T}, \ol{S})$, 
        $\sigma(\ol{T}) = \ol{\wcNtype{\Delta}{N}}$ and $\sigma(\type{T}) = \wcNtype{\Delta'}{N'}$
    \item[then] $ \Delta, \overline{\Delta}, \Delta' \vdash \sigma(\type{T}) <: \sigma(\type{S}) $

    % \item[If] $(\sigma, \Delta) = \unify{}( C \cup \set{ \overline{\wcNtype{\Delta}{N} \lessdot \type{T} } } )$
    % \item[and] $\text{fv}(\ol{T}) \notin C$, $\text{fv}(\ol{\wcNtype{\Delta}{N}}) \notin C$
    % \item[Then] $\Delta, \overline{\Delta} \vdash \overline{ \sigma(\type{N}) <: \sigma(\type{T}) }$
\end{description}

Their scope is the set of constraints, which contain the same free variable placeholders.

\end{lemma}
\textit{Proof:}
%TODO: is it true even?
The input set does not contain free variables, only free variable placeholders.
The only time \unify{} add a wildcard to the $\wildcardEnv$ is the \rulename{Capture} rule.
This rule is only applied for the outer wildcard environments for each type.

\begin{lemma}\label{lemma:unifySoundness}
The \unify{} algorithm only produces correct output.
\begin{description}
\item[If] $(\sigma, \Delta) = \unify{}( \Delta', \, \overline{ \type{S} \lessdot \type{T} } \cup \overline{ \type{S'} \lessdotCC \type{T'} } )$ %\cup \overline{ \type{S} \doteq \type{S'} })$
%\item[and] $fv(\overline{ \type{S} }) = \emptyset$, $fv(\overline{ \type{T} }) = \emptyset$
\item[Then] there exists a $\sigma'$ with:
$\sigma \subseteq \sigma'$ and
$\Delta, \Delta' \vdash \overline{\sigma'(\type{S}) <: \sigma'(\type{T})}$
and $\Delta, \Delta', \overline{\Delta} \vdash \overline{\type{N} <: \sigma'(\type{T'})}$ where $\overline{\sigma(\type{S'}) = \wcNtype{\Delta}{N}}$,
otherwise $\Delta, \Delta' \vdash \overline{\sigma'(\type{S'}) <: \sigma'(\type{T'})}$
% and $\sigma(\type{T'}) = \sigma(\type{T'})$.

% The function $\CC{}$ is given as $\CC{}(\wcNtype{\Delta}{N}) = \type{N}$

% Unify cannot guarantee that only wildcards declared on the left side are used. Example input:
% List<b?> <. List<b?>
% b? =. X
% but if the left side is a normal type (no fv's) then this can be guaranteed (maybe?)
%String <. X_String % here X is not in the environment

% What is the problem?
% a? can only use wildcards, which are declared in \Delta or on the left side 
% Otherwise constraints of the form a <. T cannot ensure soundness!

% We could say that a? only gets free variables hold by the constraints a? appears in

% a constraint a <. T means that there are free variables 
\end{description}
\end{lemma}

% \begin{lemma} % a lemma where we distinguis between free variable on the left or the right side of a constraint (not needed anymore)
%     The \unify{} algorithm only produces correct output for constraints not containing free variables.    
% \begin{description}
% \item[If] $(\sigma, \Delta) = \unify{}( \overline{ \type{S} \lessdot \type{T} } \cup \overline{ \wcNtype{\Delta'}{N} \lessdot \type{T'} } \cup \overline{ \type{S'} \lessdot \wcNtype{\Delta'}{N'} })$ 
% \item[and] $fv(\overline{ \type{S} }) = \emptyset, fv(\overline{ \type{T} }) = \emptyset, fv(\overline{ \type{T'} }) = \emptyset, fv(\overline{ \type{S'} }) = \emptyset$
% \item[Then] $\Delta \vdash \overline{\sigma(\type{S}) <: \sigma(\type{T})}$
% and $\Delta, \Delta' \vdash \overline{\sigma(\type{N}) <: \sigma(\type{T'})}, \overline{\sigma(\type{S'}) <: \sigma(\type{N'})}$
% %TODO: Rephrase (\Delta' is used three times!)
% %The function $\CC{}$ is given as $\CC{}(\wcNtype{\Delta}{N}) = \type{N}$
% \end{description}
% \end{lemma}
\textit{Proof:}
%(we are going backwards over the algorithm)
%first we have to determine the \Delta'' -> it's only the wildcards which are free in N
% during this proof we can use Delta'' as we like

For every step in the \unify{} algorithm:
Assuming the unifier $\sigma$ is correct for a constraint set $C'$, the unifier is also correct for the
constraint set $C$ before the transformation.
% \begin{description}
% \item[Assumption:] $\unify{}(C) = (\Delta, \sigma)$, with $\Delta \vdash \sigma(C)$
% \item[Induction step:] For every case $C'$ which can be transformed to $C$ we have to show $\Delta \vdash \sigma(C')$   
% \end{description}

\unify{} terminates with $C = \emptyset$ for which the preposition holds:
$\Delta \vdash \sigma(\emptyset)$

We now show that for every transformation of a constraint set $C$ to a constraint set $C'$
the preposition holds for $C$ using the assumption that it holds for $C'$ :
$\Delta \vdash  \sigma(C') \implies \Delta \vdash \sigma(C)$

\begin{description}
\item[AddDelta] $C$ is not changed
\item[GenDelta] by definition, S-Var-Left, and S-Trans %The generated type variable is unique due to the solved form property. %and the solved form property (no $\tv{a}$ in $C$)
\item[GenSigma] by definition and S-Refl.
% holds for $\set{\tv{a} \doteq \type{G}}$ by definition.
% Holds for $C$ by assumption and because $\tv{a} \notin C$ by solved form definition ($[\type{G}/\tv{a}]C = C$).
\item[Ground] Assumption and S-Bot
\item[Sub-Elim] Assumption and S-Refl
\item[Force] by assumption and $\rwildcard{X} = \type{U}$ %TODO: step 5 should remove all X^T_T with T (make wildcards with same upper and lower bounds to normal types)
\item[Raise] Assumption, S-Trans
\item[Settle] Assumption, S-Trans
\item[Super] S-Extends ($\vdash \wctype{\Delta}{C}{\ol{T}} <: \wctype{\Delta}{D}{[\ol{T}/\ol{X}]\ol{N}}$), S-Trans
\item[\generalizeRule{}] by Assumption, because $C \subset C'$
\item[Adapt] Assumption, S-Extends, S-Trans
\item[Adopt] Assumption, because $C \subset C'$
%\item[Capture, Reduce] are always applied together. We have to destinct between two cases:
\item[Prepare]
Given a $\wctype{\Delta_c}{C}{\ol{S}} \lessdot \wcNtype{\Delta''}{N}$
we get $\Delta, \Delta', \overline{\Delta} \vdash \exptype{C}{\ol{S}} <: \wcNtype{\Delta''}{N}$ with $\Delta_c \subseteq \overline{\Delta}$.

$\text{fv}(\sigma'(\wctype{\Delta_c}{C}{\ol{S}})) = \emptyset$ implies $\text{fv}(\ol{S})\subseteq \text{dom}(\Delta, \Delta_c)$
and $\text{fv}(\sigma'(\wcNtype{\Delta''}{N})) = \emptyset$ implies $\text{dom}(\Delta_c) \cap \text{fv}(\sigma'(\wcNtype{\Delta''}{N})) = \emptyset$.

No free variables on both sides also mean we do not need $\overline{\Delta}$.
Therefore we can say $\Delta, \Delta' \vdash \wctype{\Delta_c}{C}{\ol{S}} <: \wcNtype{\Delta''}{N}$.

\item[Capture]
Everytime the \rulename{Capture} rule is invoked we add the freshly generated free variables to the global environment $\wildcardEnv$.
We get a $\sigma'$ %and a $\Delta'$
with $\Delta, \Delta' \vdash \sigma'([\ol{\rwildcard{C}}/\ol{\rwildcard{B}}] \exptype{C}{\ol{S}}) <: \sigma'(\wctype{\Delta}{C}{\ol{T}})$
where $\sigma'(\ol{\wildcard{C}{U}{L}}) \subseteq \Delta'$ by assumption.
\unify{} performs a capture conversion only on $\lessdotCC$ constraints.
Therefore we can say that $\Delta, \Delta', \overline{\Delta} \vdash \sigma'(\exptype{C}{\ol{S}})
<: \sigma'(\wctype{\Delta}{C}{\ol{T}})$ with $\overline{\Delta}$ being all the fresh wildcards generated by \rulename{Capture}.

\item[Reduce]

%Assumption and S-Exists.
% Three different cases of the constraint $\exptype{C}{\ol{S}} \lessdot \wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}$:
% \begin{description} 
%     \item[$\text{fv}(\exptype{C}{\ol{S}}) = \emptyset, \text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}})$:]
%     the preposition holds by Assumption and S-Exists.
%     \item[$\text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) = \emptyset$:]
%     then $\text{fv}(\exptype{C}{\ol{S}}) \subseteq \Delta'$ with $\Delta' = \overline{\wildcard{A}{\type{U}}{\type{L}}}$ 
%     \item[$\text{fv}(\exptype{C}{\ol{S}}) = \emptyset$] $\Delta' = \emptyset$
% \end{description}
% List<X> <. Y.List<Y>, free variables are either in 
If $\text{fv}(\exptype{C}{\ol{S}}) = \text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) = \emptyset$ the preposition holds by Assumption and S-Exists.
Otherwise 
$\Delta' \vdash \CC{}(\sigma(\exptype{C}{\ol{S}})) <: \sigma(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}})$
holds with any $\Delta'$ so that $(\text{fv}(\exptype{C}{\ol{S}}) \cup \text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) ) \subseteq \text{dom}(\Delta') $.
\item[Match] Assumption, S-Trans
\item[Trim] Assumption and S-Exists
\item[Remove] $C$ is not changed
\item[Circle] S-Refl
\item[Swap] by definition
\item[Erase] S-Refl
\item[Equals] by definition
% \item[Reduce]
% The renaming from $\rwildcard{C}$ to $\rwildcard{B}$ is not a problem. It's allowed to rename wildcards inside a type.
% Removing $\rwildcard{C}$ from the environment does not change anything because it was freshly generated and is used nowhere.

% The rest follows directly from S-Exists.
% We can say: $\text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) = \emptyset$,
% because the input to the \unify{} algorithm has no free type variables and we never substitute a type with free type variables
% and none of the other steps of the algorithm generates a $\lessdot$ constraint containing free type variables on the right side. %TODO: proof

% $\text{fv}(\ol{T}) \subseteq \text{dom}(\wildcardEnv \cup \overline{\wildcard{B}{\type{U'}}{\type{L'}}})$
% TODO: The capture conversion has to be when substituting a $\wtv{a}$ variable. Then we have to rename!
% %Lets first try it without the capture conversion. And involve the wtvs in the second step
% % The algorithm works by never substituting wildcards



% \unify{} cannot guarantee the premise $\text{dom}(\Delta, \Delta') \cap \text{fv}(\wcNtype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{N}) = \emptyset$.
% We loosen the soundness requirements and allow a arbitrary environment $\Delta''$ to be added to the right side of the subtype relation.
% This is still sufficient to proof soundness for the whole algorithm.
% We show that the need for the additional environment $\Delta''$ can be satisfied by a let statement.

% \begin{itemize}
% \item $\Delta, \Delta' \vdash [\ol{T}/\ol{X}]\ol{L} <: \ol{T}$: S-Exists 
% \item $\Delta, \Delta' \vdash \ol{T} <: [\ol{T}/\ol{X}]\ol{U}$: S-Exists
% \item $\textit{fv}(\ol{T}) \subseteq \text{dom}{\Delta, \Delta'}$: $\wildcardEnv$ holds all variables %TODO: Proof
% \end{itemize}
\item[Normalize] Assumption and lemma 5 \emph{substitution preserves subtyping}.%\ref{lemma:wildcardReplacement}. (Or Lemma 5 from the wildcard paper. \emph{substitution preserves subtyping})
% The GenSigma step replaces both sides of $\rwildcard{A} \doteq \rwildcard{B}$ with the upper bound $\type{U}$.
% This works for every constraint, whether it contains free variables or not.
% It does not add to free variables of constraints because the upper bound does not contain any.
The GenSigma and Gen Delta steps remove Wildcards which have the same upper and lower bound.
$\rwildcard{A},\rwildcard{B} \notin \sigma(C)$

% sigma(T) = sigma(U) we have to show that T = U means \Delta \vdash [T/U]C \implies \Delta \vdash [U/T]C 
% the constraints L <. U, U <. L lead to L =. U
%If L is List<X> with X being free wildcard
%then U <. L will fail if U is type variable




% this is because bounds never contain free variables (is that true?)

%This type contains free variables when A is replaced by an CC wildcard

%This must fail:
\begin{verbatim}
<A> A m(List<? extends List<A>> l, A)

m(List<List<? super String>> l, "hi") 
\end{verbatim}
%This fails because of Equals rule (TODO: proof)

\item[Tame] same reasoning as Normalize
\item[Bot] S-Bot
\item[Pit] S-Bot
\item[Upper] S-Trans and S-VarLeft
\item[Lower] S-Trans and S-VerRight
\item[Subst-WC] by S-Refl
\item[Subst]
$\sigma(C \cup \set{\tv{a} \doteq \type{T}}) = \sigma([\type{T}/\tv{a}]C \cup \set{\tv{a} \doteq \type{T}})$
and
$\sigma(\wildcardEnv) = \sigma([\type{T}/\tv{a}]\wildcardEnv)$
\item[Subst-WC]
%Proof by Lemma 5 \emph{Type substitution preserves subtyping} from \cite{WildcardsNeedWitnessProtection}.
Same as Subst
\end{description}