-\begin{equation} \label{eq:inferAppN}
- \infer[AppN]
- {\Gamma \vdash \textit{id}(e^*).\textit{fs}^* \Rightarrow
- ((\Gamma^\star, \star, \tau^r,
- \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
+\begin{equation}\label{eq:inferAppN}
+ \resizebox{\linewidth}{!}{%
+ \infer[AppN]
+ {\Gamma \vdash \textit{id}(e^*).\textit{fs}^* \Rightarrow
+ ((\Gamma^\star, \star, \tau^r,
+ \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