\section{Appendix for Sect.~\ref{sect:preliminaries}}
\label{sect:app-preliminaries}

Equality axioms:
\[
 \begin{array}{rl}
\refl & \forall x . x = x \\
\symm & \forall x, y. (x = y \limp y = x )\\
\trans & \forall x , y , z . ( x = y \limp y = z \limp x = z ) \\
\subst_f & \forall \vec x , \vec y . (\vec x = \vec y \limp f(\vec x) = f(\vec y) ) \\
\subst_P & \forall \vec x , \vec y. (\vec x = \vec y \limp P(\vec x) \limp P(\vec y)  )
 \end{array}
 \]