Cleanup and fixes

introduction.tex

@@ -63,7 +63,7 @@ Our type inference algorithm has to add let statements surrounding method invoca
       \begin{subfigure}[t]{0.49\linewidth}
 \begin{lstlisting}[style=tfgj]
 List<? super Integer> ls = ...;
-    ls.add(new Integer());
+let x : (*@ $\wctype{\wildcard{X}{\texttt{Object}}{\texttt{Integer}}}{List}{\rwildcard{X}}$ @*) = ls in ls.add(new Integer());
 \end{lstlisting}
         \caption{Capture Conversion by \texttt{let}-statement}
         \label{fig:intro-example-typed}

tRules.tex

@@ -21,8 +21,6 @@ $
 Each class type has a set of wildcard types $\overline{\Delta}$ attached to it.
 The type $\wctype{\overline{\Delta}}{C}{\ol{T}}$ defines a set of wildcards $\overline{\Delta}$,
 which can be used inside the type parameters $\ol{T}$.
-It is important that each wildcard declaration $\wildcard{X}{T}{L}$ is unique.
-
 
 \section{Type rules}