diff --git a/soundness.tex b/soundness.tex
index 072287b..866cf53 100644
--- a/soundness.tex
+++ b/soundness.tex
@@ -388,6 +388,8 @@ $\Delta \vdash  \sigma(C') \implies \Delta \vdash \sigma(C)$
 \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[Same] by S-Exists
+\item[SameW] %TODO
 \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:
diff --git a/tRules.tex b/tRules.tex
index ff727c8..0459b75 100644
--- a/tRules.tex
+++ b/tRules.tex
@@ -132,7 +132,7 @@ $
 % \caption{Input Syntax}\label{fig:syntax}
 % \end{figure}
 
-\subsection{ANF transformation}
+\subsection{ANF transformation}\ref{sec:anfTransformation}
 \newcommand{\anf}[1]{\ensuremath{\tau}(#1)}
 %https://en.wikipedia.org/wiki/A-normal_form)
 Featherweight Java's syntax involves no \texttt{let} statement