diff --git a/introduction.tex b/introduction.tex
index 500a16b..fb61751 100644
--- a/introduction.tex
+++ b/introduction.tex
@@ -524,6 +524,20 @@ The main challenge was to find an algorithm which computes $\sigma(\wtv{a}) = \r
 The input is transformed to A-normal form.
 %TODO: describe ANF syntax (which is different then the one from the wiki: https://en.wikipedia.org/wiki/A-normal_form)
 
+$
+\begin{array}{lrcl}
+\hline
+\text{Terms} & t & ::= & v \\
+& & \ \ | & \texttt{let}\ x = v \ \texttt{in}\ x.f\\
+& & \ \ | & \texttt{let}\ x_1 = v \ \texttt{in}\ \texttt{let}\ \overline{x} = \overline{v} \ \texttt{in}\ x_1.\texttt{m}(\overline{x})\\
+& & \ \ | & t \elvis{} t\\
+\text{Var} & v & ::= & \expr{x} \\
+& & \ \ | & \texttt{new} \ \type{C}(\overline{t})\\
+\text{Variable contexts} & \Gamma & ::= & \overline{x:\type{T}}\\
+\hline
+\end{array}
+$
+
 \subsection{Capture Conversion}
 The input to our type inference algorithm does not contain let statements.
 Those are added after computing a type solution.
diff --git a/prolog.tex b/prolog.tex
index a60607e..27135fa 100755
--- a/prolog.tex
+++ b/prolog.tex
@@ -106,6 +106,8 @@
 \newcommand{\letfj}{\emph{LetFJ}}
 \newcommand{\tph}{\text{tph}}
 
+\newcommand{\expr}[1]{\texttt{#1}}
+
 \def\exptypett#1#2{\texttt{#1}\textrm{{\tt <#2}}\textrm{{\tt >}}\xspace}
 \def\exp#1#2{#1(\,#2\,)\xspace}
 \newcommand{\ldo}{, \ldots , }
diff --git a/tRules.tex b/tRules.tex
index 646994b..9428d96 100644
--- a/tRules.tex
+++ b/tRules.tex
@@ -249,6 +249,39 @@ $\begin{array}{l}
     \end{array}
 \end{array}$
 \\[1em]
+$\begin{array}{l}
+    \typerule{T-Call}\\
+    \begin{array}{@{}c}
+        \generics{\ol{X \triangleleft U'}} \ol{U} \to \type{U} \in \Pi(\texttt{m}) \quad \quad
+        \Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}
+        \\
+        \Delta \vdash \ol{S} \ \ok \quad \quad
+        \Delta | \Gamma \vdash  \texttt{e}, \ol{e} : \ol{T} \quad \quad
+        \Delta \vdash \ol{T} <: [\ol{S}/\ol{X}]\ol{U} 
+        \\
+        \hline
+    \vspace*{-0.3cm}\\
+        \Delta | \Gamma \vdash \texttt{e}.\texttt{m}(\ol{e}) : \type{T}
+    \end{array}
+\end{array}$
+\\[1em]
+$\begin{array}{l}
+    \typerule{T-Let}\\
+    \begin{array}{@{}c}
+        \Delta | \Gamma \vdash \expr{e}_1 : \type{T}_1 \quad \quad
+        \Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N}
+        \\
+        \Delta, \Delta' | \Gamma, \expr{x} : \wcNtype{}{N} \vdash \expr{t}_2 : \type{T}_2 \quad \quad
+        \Delta, \Delta' \vdash  \type{T}_2 <: \type{T} \quad \quad
+        \text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
+        \Delta \vdash \type{T}, \wcNtype{\Delta'}{N} \ \ok
+        \\
+        \hline
+    \vspace*{-0.3cm}\\
+        \Delta | \Gamma \vdash \texttt{let} \expr{x} : \wcNtype{\Delta'}{N} = \expr{e}_1 \ \texttt{in} \ \expr{e}_2 : \type{T}
+    \end{array}
+\end{array}$
+\\[1em]
 $\begin{array}{l}
     \typerule{T-Elvis}\\
     \begin{array}{@{}c}