\renewcommand\e{\DELTA{\scriptstyle\epsilon}}
\newcommand\infrulealigned[2]{
  \infrule{
    \vphantom{\G(\mx) = \mA}
    #1
  }{
    \vphantom{\G \vinf \vpair{\mValue_1}{\mValue_2} \of \mA_1\vprod\mA_2}
    #2
  }
}
\begin{gather*}
  \G \vinf \mconst \of \constType\mconst
\quad
\infrulealigned{
  \G(\mx) = \mA
}{
  \G \vinf \mx \of \mA
}
\quad
  \G \vinf \unitval \of \unittype
\quad
\infrulealigned{
  \G \vinf \mValue_1\of \mA_1 \quad
  \G \vinf \mValue_2 \of \mA_2
}{
  \G \vinf \vpair{\mValue_1}{\mValue_2} \of \mA_1\vprod\mA_2
}
\\\\
\infrule[\indx i = \indx 1, \indx 2]{
  \G \vinf \mValue \of \mA_i
}{
  \G \vinf \inject{\indx i}\mValue \of \mA_1+\mA_2
}
\qquad\qquad
\infrule{
  \G \cinf \mM \of \mB
}{
  \G \vinf \thunk \mM \of \sU\mB
}
\\\\
\DELTA{
\infrule{
  \G \cinf[\e_1] \mM \of \sF[\e_1]\mA
}{
  \G \cinf[\e_2] \coerce\mM \of \sF[\e_2]\mA
}}
\qquad\qquad
\infrule{
  \G \vinf \mValue \of \mA
}{
  \G \cinf \return\mValue \of \sF\mA
}
\\\\
\infrule{
  \G \cinf \mM \of \sF\mA \quad
  \G, \mx \of \mA \cinf \mN \of \mB
}{
  \G \cinf \sbind \mM\mx\mA\mN \of \mB
}
\\\\
\infrule{
  \G \cinf \mM_1 \of \mB_1 \quad
  \G \cinf \mM_2 \of \mB_2 \quad
}{
  \G \cinf \cpair{\mM_1}{\mM_2} \of {\mB_1}\cprod{\mB_2}
}
\qquad\qquad
\infrule[\indx i = \indx 1, \indx 2]{
  \G \cinf \mM \of \mB_1\cprod\mB_2
}{
  \G \cinf \apply{\indx i}\mM \of \mB_i
}
\\\\
\infrule{
  \G, \mx \of \mA \cinf \mM \of \mB
}{
  \G \cinf \abst \mx\mA\mM \of \funtype\mA\mB
}
\qquad\qquad
\infrule{
  \G \vinf \mValue \of \mA \quad
  \G \cinf \mM \of \funtype\mA\mB
}{
  \G \cinf \apply\mValue\mM \of \mB
}
\\\\
\infrule[\mx_1 \neq \mx_2]{
  \G \vinf \mValue \of \mA_1\vprod\mA_2 \quad
  \G, \mx_1 \of \mA_1, \my \of \mA_2 \cinf \mM \of \mB
}{
  \G \cinf \prodmatch \mValue{\mx_1}{\mA_1}{\mx_2}{\mA_2}\mM \of \mB
}
\\\\
\infrule{
  \G \vinf \mValue \of \zerotype
}{
  \G \cinf \zeromatch\mValue\mB \of \mB
}
\\\\
\infrule{
  \G                  \vinf \mValue \of \mA_1\vplus\mA_2 \quad
  \G, \mx_1 \of \mA_1 \cinf \mM_1 \of \mB \quad
  \G, \mx_2 \of \mA_2 \cinf \mM_2 \of \mB
}{
  \G \cinf \plusmatch \mValue{\mx_1}{\mA_1}{\mM_1}{\mx_2}{\mA_2}{\mM_2} \of \mB
}
\\\\
\infrule{
  \G \vinf \mValue \of \sU\mB
}{
  \G \cinf \force\mValue \of \mB
}
%% \qquad\qquad
%% \infrule[\sbot \in \e]{
%%   \G , \mx \of \sU\mB \cinf \mM \of \mB
%% }{
%%   \G \cinf \sfix \mx{\mB}\mM \of \mB
%% }
\\\\
\infrule[{\mop \of
\sarity{\sArity}{\sParam}}, \mop \in \DELTA{\epsilon}\UNDELTA{\Opset}]{
  \G \cinf \mValue \of \sParam \quad
  \G \cinf \mM \of \funtype{\sArity}\mB
}{
  \G \cinf \mop_{\mValue}^{\mB}\mM \of \mB
}
\end{gather*}
