$\beta$ laws:
\vspace{-1cm}
\begin{gather*}
  \prodmatch{\vpair{\mV}{\mV'}}{\mx}{\mA}{\my}{\mA'}\mM
  =
  \substituteDouble\mM{\mV}{\mx}{\mV'}{\my}
  \\
  \plusmatch{\inject{\indx
      i}\mV\!}{\mx_1\!}{\!\mA_1}{\mM_1}{\mx_2\!}{\!\mA_2}{\mM_2}
  \!=
  \substitute{\mM_i}{\mV\!}{\mx_i}
  \\
  \force{\parent{\thunk\mM}}
  =
  \mM
  \qquad
  \sbind{\parent{\return\mV}}\mx\mA\mM
  =
  \substitute\mM\mV\mx
  \\
  \apply{\indx i}{\cpair{\mM_1}{\mM_2}} = \mM_i
  \qquad
  \apply{\mV}{\abst\mx\mA\mM} = \substitute\mM\mV\mx
\end{gather*}

$\eta$ laws:
\vspace{-1cm}
\begin{gather*}
  \mV = \unitval
  \\
  \substitute\mM\mV\mz
  =
  \prodmatch\mV{\mx}{\mA}{\my}{\mA'}{\substitute\mM{\vpair\mx\my}{\mz}}
  \quad
  \fresh{\mx$, $\my}\mM
  \\
  \mM
  =
  \zeromatch\mV\mB
  \\
  \substitute\mM\mV\mz
  =
  \plusmatch*\mV{\mx}{\mA\hphantom{'}}{\substitute\mM{\inject[]1\mx}\mz}{\my}{\mA'}{\substitute\mM{\inject[]2\my}\mz}
  \quad
  \fresh{\mx$, $\my}\mM
  \\
  \mV = \thunk{\parent{\force \mV}}
  \qquad
  \mM = \sbind\mM\mx\mA{\return\mx}
  \\
  \mM
  =
  \cpair{\apply{\indx 1}\mM}{\apply{\indx 2}\mM}
  \qquad
  \mN = \abst\mx\mA{\apply \mx\mN} \qquad \fresh\mx\mN
\end{gather*}

Sequencing:
\begin{gather*}
  \sbind\mM{\mx\!}{\!\mA}{\parent{\sbind\mN{\my\!}{\!\mA'\!}{\mN'}}}
  \!=\!
  \sbind{\parent{\sbind\mM{\mx\!}{\!\mA}\mN}\!}{\my\!}{\!\mA'\!}{\mN'}
  \quad\!\!\!
  \fresh\mx{\mN'}
  \\
  \sbind\mM\mx\mA{\cpair{\mN_1}{\mN_2}}
  =
  \cpair*{\sbind\mM\mx\mA{\mN_1}}
         {\sbind\mM\mx\mA{\mN_2}}
  \\
  \sbind\mM\mx\mA{\abst\my{\mA'}\mN}
  =
  \abst\my{\mA'}{\parent{\sbind\mM\mx\mA\mN}}
  \quad\fresh\my\mM
\end{gather*}

Effects:
\vspace{-1.1cm}
\begin{gather*}
  \mop_{\mV}^{\mB}{\abst{\mx\!}{\!\sArity}{\parent{\sbind\mM{\my\!}{\!\mA'}\mN}}}
  =
  \sbind{\parent{\!\mop_{\mV}^{\sF{\mA'}}\!{\abst{\mx\!}{\!\sArity}\mM}\!}\!\!}{\my\!}{\!\mA'\!\!}\mN
  \ \,
  \fresh\mx\mN
  \\
  \mop_{\mV}^{\mB_1\cprod\mB_2}{\abst\mx\sArity{\cpair*{\mM_1}{\mM_2}}}
  =
  \cpair*{\mop_{\mV}^{\mB_1}\abst\mx\sArity{\mM_1}}
         {\mop_{\mV}^{\mB_2}\abst\mx\sArity{\mM_2}}
  \\
  \mop_{\mV}^{\funtype{\mA'}{\mB}}\abst\mx\sArity{\abst\my{\mA'}\mM }
  =
  \abst\my{\mA'}{\mop_{\mV}^{\mB}\abst\mx\sArity\mM}
  \quad \mx\neq\my
\end{gather*}

% Recursion: $\quad \sfix\mx\mB\mM = \substitute\mM{\thunk{\sfix\mx\mB\mM}}\mx$

Coercion:
\vspace{-1.05cm}
\begin{gather*}
  \coerce[\e_2\subset\e_3]{\parent{\coerce\mM}}
  =
  \coerce[\e_1\subset\e_3]\mM
  \\
  \coerce{\parent{\return[\e_1]\mM}} = \return[\e_2]\mM
  \\
  \coerce[\e\subset\e']{\parent{\sbind{\mM\!}{\mx\!}{\!\mA}\mN}}
  =
  \sbind{\parent{\coerce[\e\subset\e']\mM}\!}{\mx\!}{\!\mA}{\coerce[\e\subset\e']\mN}
  \\
  \coerce {\parent{{\mop_{\mV}^{\sF[\e_1]{\mA'}}\abst\mx\sArity\mM}}}
  =
  \mop_{\mV}^{\sF[\e_2]{\mA'}}\abst\mx\sArity{\coerce\mM}
\end{gather*}
