diff --git a/paper/gtt.tex b/paper/gtt.tex
index 71b5f5403311e8c3211f9277ab63d705c7a19077..f85c9eef53b2afa8c4955270f62f31b8102d10c0 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -1399,35 +1399,35 @@ domain~\cite{newahmed18,newlicata2018-fscd}.
   \begin{mathpar}
     \framebox{$A \ltdyn A'$ and $\u B \ltdyn \u B'$}
     
-    \inferrule{ }{A \ltdyn A}
+    \inferrule*[right=VTyRefl]{ }{A \ltdyn A}
 
-    \inferrule{A \ltdyn A' \and A' \ltdyn A''}
+    \inferrule*[right=VTyTrans]{A \ltdyn A' \and A' \ltdyn A''}
               {A \ltdyn A''}
 
-    \inferrule{ }{\u B \ltdyn \u B'}
+    \inferrule*[right=CTyRefl]{ }{\u B \ltdyn \u B'}
 
-    \inferrule{\u B \ltdyn \u B' \and \u B' \ltdyn \u B''}
+    \inferrule*[right=CTyTrans]{\u B \ltdyn \u B' \and \u B' \ltdyn \u B''}
               {\u B \ltdyn \u B''}
 
-    \inferrule{ }{A \ltdyn \dynv}
+    \inferrule*[right=VTyTop]{ }{A \ltdyn \dynv}
 
-    \inferrule{\u B \ltdyn \u B'}
+    \inferrule*[right=$U$Mon]{\u B \ltdyn \u B'}
               {U B \ltdyn U B'}
 
-    \inferrule{A_1 \ltdyn A_1' \and A_2 \ltdyn A_2' }
+    \inferrule*[right=$+$Mon]{A_1 \ltdyn A_1' \and A_2 \ltdyn A_2' }
               {A_1 + A_2 \ltdyn A_1' + A_2'}
 
-    \inferrule{A_1 \ltdyn A_1' \and A_2 \ltdyn A_2' }
+    \inferrule*[right=$\times$Mon]{A_1 \ltdyn A_1' \and A_2 \ltdyn A_2' }
               {A_1 \times A_2 \ltdyn A_1' \times A_2'}
 \\
-    \inferrule{ }{\u B \ltdyn \dync}
+    \inferrule*[right=CTyTop]{ }{\u B \ltdyn \dync}
 
-\inferrule{A \ltdyn A' }{ \u F A \ltdyn \u F A'}
+\inferrule*[right=$F$Mon]{A \ltdyn A' }{ \u F A \ltdyn \u F A'}
 
-\inferrule{\u B_1 \ltdyn \u B_1' \and \u B_2 \ltdyn \u B_2'}
+\inferrule*[right=$\with$Mon]{\u B_1 \ltdyn \u B_1' \and \u B_2 \ltdyn \u B_2'}
               {\u B_1 \with \u B_2 \ltdyn \u B_1' \with \u B_2'}
 
-\inferrule{A \ltdyn A' \and \u B \ltdyn \u B'}
+\inferrule*[right=$\to$Mon]{A \ltdyn A' \and \u B \ltdyn \u B'}
           {A \to \u B \ltdyn A' \to \u B'}
 \begin{longonly}
 \\