diff --git a/paper/main.tex b/paper/main.tex
index 1073bc8..d8eab57 100644
--- a/paper/main.tex
+++ b/paper/main.tex
@@ -387,30 +387,30 @@ Transitive closure over \(\rightarrow_\text{distribute}\), \(\rightarrow_\text{c
 
 \begin{mathpar}
 
-\inferrule[E-Refl]{
+\inferrule[T-Eq-Refl]{
 	\metavariable{\tau} \in \nonterm{T}
 }{
 	\metavariable{\tau} \equiv \metavariable{\tau}
 }\and
-\inferrule[E-Trans]{
+\inferrule[T-Eq-Trans]{
 	\metavariable{\tau_1} \equiv \metavariable{\tau_2}\\
 	\metavariable{\tau_2} \equiv \metavariable{\tau_3}
 }{
 	\metavariable{\tau_1} \equiv \metavariable{\tau_3}
 }
 
-\inferrule[E-Rename]{
+\inferrule[T-Eq-Alpha]{
 	\metavariable{\tau_1} \rightarrow_\alpha \metavariable{\tau_2}
 }{
 	\metavariable{\tau_1} \equiv \metavariable{\tau_2}
 }
 
-\inferrule[E-Distribute]{
+\inferrule[T-Eq-Distribute]{
 	\metavariable{\tau_1} \rightarrow_\text{distribute} \metavariable{\tau_2}
 }{
 	\metavariable{\tau_1} \equiv \metavariable{\tau_2}
 }\and
-\inferrule[E-Condense]{
+\inferrule[T-Eq-Condense]{
 	\metavariable{\tau_1} \rightarrow_\text{condense} \metavariable{\tau_2}
 }{
 	\metavariable{\tau_1} \equiv \metavariable{\tau_2}
@@ -425,7 +425,7 @@ See \hyperref[coq:type-equiv]{equiv.v:\ref{coq:type-equiv}}.
 \begin{lemma}[Symmetry of \(\equiv\)]
 
 \begin{mathpar}
-\inferrule[E-Symm]{
+\inferrule[T-Eq-Symm]{
 	\metavariable{\tau_1} \equiv \metavariable{\tau_2}
 }{
 	\metavariable{\tau_2} \equiv \metavariable{\tau_1}
@@ -450,17 +450,24 @@ PNF reached by exhaustive application of \(\rightarrow_\text{condense}\).
 
 \subsubsection{Subtype Relations}
 
-We define two relations: first the syntatic subtype relation \(\leq\) and second the semantic subtype relation \(\precsim\).
+We define two relations: first the representation subtype relation \(\leq\) and second the transformation subtype relation \(\precsim\).
 
-\begin{definition}[Syntactic Subtype (\(\tau_1\leq\tau_2\))]
+\begin{definition}[Representation Subtype (\(\tau_1\leq\tau_2\))]
 \begin{mathpar}
-\inferrule[S-Refl]{	
+\inferrule[TSubRepr-Refl]{	
 	\metavariable{\tau} \equiv \metavariable{\tau'}
 }{
 	\metavariable{\tau} \leq \metavariable{\tau'}
 }
 
-\inferrule[S-Syntactic]{
+\inferrule[TSubRepr-Trans]{	
+	\metavariable{\sigma} \leq \metavariable{\tau}\\
+	\metavariable{\tau} \leq \metavariable{\nu}
+}{
+	\metavariable{\sigma} \leq \metavariable{\nu}
+}
+
+\inferrule[TSubRepr-Ladder]{
 	\metavariable{\sigma} \leq \metavariable{\tau}
 }{
 	\metavariable{\sigma'} \typeterminal{\sim} \metavariable{\sigma} \leq \metavariable{\tau}
@@ -468,40 +475,44 @@ We define two relations: first the syntatic subtype relation \(\leq\) and second
 \end{mathpar}
 \end{definition}
 
-\begin{definition}[Semantic Subtype (\(\tau_1\precsim\tau_2\))]
+\begin{definition}[Transformation Subtype (\(\tau_1\precsim\tau_2\))]
 \begin{mathpar}
-
-\inferrule[S-Refl]{	
+\inferrule[TSub-Refl]{	
 	\metavariable{\tau} \equiv \metavariable{\tau'}
 }{
 	\metavariable{\tau} \precsim \metavariable{\tau'}
+}\and
+\inferrule[TSub-Trans]{	
+	\metavariable{\sigma} \precsim \metavariable{\tau}\\
+	\metavariable{\tau} \precsim \metavariable{\nu}
+}{
+	\metavariable{\sigma} \precsim \metavariable{\nu}
 }
 
-\inferrule[S-Syntactic]{
+\\
+
+\inferrule[TSub-Ladder]{
 	\metavariable{\sigma} \precsim \metavariable{\tau}
 }{
 	\metavariable{\sigma'} \typeterminal{\sim} \metavariable{\sigma} \precsim \metavariable{\tau}
-}
-
-\inferrule[S-Semantic]{
+}\and
+\inferrule[TSub-Morph]{
 	\metavariable{\sigma} \equiv \metavariable{\tau}
 }{
 	\metavariable{\sigma} \typeterminal{\sim} \metavariable{\sigma'} \precsim \metavariable{\tau} \typeterminal{\sim} \metavariable{\tau'}
 }
-
-
 \end{mathpar}
 \end{definition}
 
 
-\begin{example}[Syntactic \& Semantic Subtypes]$\\$
+\begin{example}[Representation \& Transformation Subtypes]$\\$
 
 \begin{enumerate}
 \item \typeterminal{ <Digit 10> \(\sim\) Char \( \quad \leq \quad \) Char }\\
-.. is a \emph{syntactic subtype}, because the representation of \typeterminal{<Digit 10>} is \emph{embedded} into \typeterminal{Char}.\\
+.. is a \emph{representation subtype}, because the representation of \typeterminal{<Digit 10>} is \emph{embedded} into \typeterminal{Char}.\\
 
 \item \typeterminal{ <Digit 10> \(\sim\) Char \( \quad \precsim \quad \) <Digit 10> \(\sim\) machine.UInt64}\\
-.. is a \emph{semantic subtype}, because the \typeterminal{Char} based representation can be transformed into a representation based on \typeterminal{machine.UInt64},
+.. is a \emph{transformation subtype}, because the \typeterminal{Char} based representation can be transformed into a representation based on \typeterminal{machine.UInt64},
 while preserving its semantics.
 \end{enumerate}
 \end{example}