Remove unnecessary fv premisses

tRules.tex

@@ -3,6 +3,15 @@
 The input syntax for our algorithm is shown in figure \ref{fig:syntax}
 and the respective type rules in figure \ref{fig:expressionTyping} and \ref{fig:typing}.
 
+The algorithm presented in this paper is an extension of the \emph{Global Type Inference for Featherweight Generic Java}\cite{TIforFGJ} algorithm.
+Additional features like overriding methods and method overloading can be added by copying the respective parts from there.
+The input language is designed to showcase type inference involving existential types.
+We introduce the type rule T-Call which emulates a Java method call,
+where existential types are implicitly \textit{opened} and \textit{closed}.
+The T-Elvis rule mimics the type judgement of a branch expression like \texttt{if-else}
+and is solely used for examples.
+%Additional features can be easily added by generating the respective constraints (Plümicke hier zitieren)
+
 The type system in \cite{WildcardsNeedWitnessProtection} allows a method to \textit{override} an existing method declaration in one of its super classes,
 but only by a method with the exact same type.
 The type system presented here does not allow the \textit{overriding} of methods.

unify.tex

@@ -239,8 +239,8 @@ $
     \hline
     \vspace*{-0.4cm}\\
     \wildcardEnv \cup \set{\wildcard{A}{\type{U}}{\type{L}}, \wildcard{B}{U'}{L'}} \vdash C \cup \, \set{ \type{L} \doteq \type{U} , \type{U'} \doteq \type{L'}, \type{U} \doteq \type{U'}  }
-    \end{array} \quad
+    \end{array}
-    \text{fv}(\type{U}, \type{U'}, \type{L}, \type{L'}) \subseteq \Delta_in
+    % \quad \text{fv}(\type{U}, \type{U'}, \type{L}, \type{L'}) \subseteq \Delta_in
     $
     \\\\
 \rulename{Tame}
@@ -250,7 +250,7 @@ $
     \hline
     \vspace*{-0.4cm}\\
     \wildcardEnv \cup \set{\wildcard{A}{\type{U}}{\type{L}}} \vdash C \cup \, \set{ \type{L} \doteq \type{T}, \type{U} \doteq \type{T} }
-    \end{array} \quad \text{fv}(\type{U}, \type{L}) \subseteq \Delta_in
+    \end{array} %\quad \text{fv}(\type{U}, \type{L}) \subseteq \Delta_in
     $
     \\\\
 % \rulename{Equals} %TODO