+\paragraph{Op2 expressions}
+Equation~\ref{eq:inferOp2} shows the inference rule for op2 expressions.
+\textit{op2type} is a function which takes an operator and returns the
+corresponding function type, i.e. $\textit{op2type}(\&\&) = Bool \rightarrow
+Bool \rightarrow Bool$.
+
+\begin{equation} \label{eq:inferOp2}
+ \infer[Op2]
+ {\Gamma \vdash e_1 \oplus e_2 \Rightarrow
+ (\Gamma^{\star}, \star, \alpha^\star, (e_1' \oplus 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')
+ &(\tau_1 \rightarrow \tau_2 \rightarrow \alpha) \unif
+ \textit{op2type}(\oplus) = \star_3
+ &\star = \star_3 \cdot \star_2 \cdot \star_1
+ }
+\end{equation}
+
+\paragraph{Op1 expressions}
+\begin{equation} \label{eq:inferOp1}
+ \infer[Op1]
+ {\Gamma \vdash \ominus e \Rightarrow
+ (\Gamma^{\star}, \star, \alpha^\star, (\ominus e')^\star)}
+ {\Gamma \vdash e \Rightarrow (\star_1, \tau, e_1')
+ &(\tau \rightarrow \alpha) \unif
+ \textit{op1type}(\ominus) = \star_2
+ &\star = \star_2 \cdot \star_1
+ }
+\end{equation}
+
+\paragraph{Tuples}
+\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{Literals}
+
+\begin{equation}
+ \infer[Int]{\Gamma \vdash n \Rightarrow (\Gamma, \star_0, Int, n)}{}
+\end{equation}
+
+\begin{equation}
+ \infer[Bool]{\Gamma \vdash b \Rightarrow (\Gamma, \star_0, Bool, b)}{}
+\end{equation}
+
+\begin{equation}
+ \infer[Char]{\Gamma \vdash c \Rightarrow (\Gamma, \star_0, Char, c)}{}
+\end{equation}
+
+\begin{equation}
+ \infer[\emptyset]
+ {\Gamma \vdash [] \Rightarrow (\Gamma, \star_0, \alpha, [])}{}
+\end{equation}
+
+\paragraph{If statements}
+\begin{equation}
+ \infer[If]
+ {\Gamma \vdash \underline{\textrm{if }} e
+ \underline{\textrm{ then }} s_1
+ \underline{\textrm{ else }} s_2
+ \Rightarrow
+ (\Gamma^\star, \star, \tau_e^\star, \underline{\textrm{if }} e'
+ \underline{\textrm{ then }} s_1'
+ \underline{\textrm{ else }} s_2')
+ }
+ {\Gamma \vdash e \Rightarrow (\Gamma^{\star_1}, \star_1, \tau_1, e')
+ &\tau_1 \unif \textrm{Bool} = \star_2
+ &\Gamma^{\star_2\cdot \star_1} \vdash s_1 \Rightarrow
+ (\Gamma^{\star_3}, \star_3, \tau_t, s_1')
+ &\Gamma^{\star_3} \vdash s_2 \Rightarrow
+ (\Gamma^{\star_4}, \star_4, \tau_e, s_2')
+ &\tau_t \unif \tau_e = \star_5
+ }
+\end{equation}
+
+\paragraph{While statements}
+\begin{equation}
+ \infer[While]
+ {\Gamma \vdash \underline{\textrm{while }} e \textrm{ } s
+ \Rightarrow
+ (\Gamma^\star, \star, \tau_s^\star,
+ \underline{\textrm{while }} e' \textrm{ } s_1')
+ }
+ {\Gamma \vdash e \Rightarrow (\Gamma^{\star_1}, \star_1, \tau_1, e')
+ &\tau_1 \unif \textrm{Bool} = \star_2
+ &\Gamma^{\star_2\cdot \star_1} \vdash s \Rightarrow
+ (\Gamma^{\star_3}, \star_3, \tau_t, s')
+ &\star = \star_3 \cdot \star_2 \cdot \star_1
+ }
+\end{equation}
+
+\paragraph{Function Statements}
+\begin{equation} \label{eq:inferStmtApp0}
+ \infer[Stmt App 0]
+ {\Gamma \vdash \textit{id}().\textit{fs}^* \Rightarrow
+ ((\Gamma^\star, \star, \textrm{Void},
+ \textit{id}().\textit{fs}^*)}
+ {\Gamma(id) = \lfloor \tau^e \rfloor
+ &\texttt{fold apfs } \tau \textit{ fs}^* = \tau^r
+ }
+\end{equation}
+
+\begin{equation} \label{eq:inferAppN}
+ \infer[Stmt AppN]
+ {\Gamma \vdash \textit{id}(e^*).\textit{fs}^* \Rightarrow
+ ((\Gamma^\star, \star, \textrm{Void},
+ \textit{id}({e^*}').\textit{fs}^*)}
+ {\Gamma(id) = \lfloor \tau^e \rfloor
+ &\Gamma \vdash e^* \Rightarrow
+ (\Gamma^{\star_1}, \star_1, \tau^*, {e^*}')
+ &(\texttt{fold } (\rightarrow) \texttt{ } \alpha \texttt{ } \tau^*)
+ \unif \tau^e = \star_2
+ &\star = \star_2 \cdot \star_1
+ &\texttt{fold apfs } \tau \textit{ fs}^* = \tau^e
+ }
+\end{equation}
\ No newline at end of file