+\begin{equation} \label{eq:tuples}
+ \infer[Tuple]
+ {\Gamma \vdash (e_1, e_2) \Rightarrow
+ (\Gamma^{\star}, \star, (\tau_1, \tau_2)^\star,
+ (e_1', e_2')^\star)}
+ {\Gamma \vdash e_1 \Rightarrow (\Gamma^{\star_1},\star_1, \tau_1, e_1')
+ &\Gamma^{\star_1} \vdash e_2 \Rightarrow (\Gamma^{\star_2},
+ \star_2, \tau_2, e_2')
+ &\star = \star_3 \cdot \star_2 \cdot \star_1
+ }
+\end{equation}
+
+\paragraph{Variables}
+Inferring variable requires a bit of care. First of all the variable has to
+be present in $\Gamma$, secondly field selectors need to be respected. To apply
+the field selectors on a type the function \tt{apfs} is used, which maps a
+type and a field selector to a new type: $\texttt{apfs} : \tau \times
+\textit{fieldselector} \rightarrow \tau$.
+
+Note that the inference rule only checks if a field selector can be applied on
+a certain type, and does not use the field selector to infer the type. This means that a program: \tt{f(x)\{ return x.hd; \}} can not be typed, and instead
+\tt{f} must be explicitly typed as \tt{:: [a] -> a} (or something more
+specialised) by the programmer. This could be improved by
+changing the \tt{apfs} function to infer for type variables.
+
+\begin{equation}
+ \infer[Var]
+ {\Gamma \vdash \textit{id}.\textit{fs}^* \Rightarrow
+ (\Gamma, \star_0, \tau', \textit{id}.\textit{fs}^*)}
+ {\Gamma(id) = \lfloor \tau \rfloor
+ &\texttt{fold apfs } \tau \textit{ fs}^* = \tau'
+ }
+\end{equation}