diff --git a/paper/gtt.tex b/paper/gtt.tex
index d9c6f24d9a698f5e26397cb8f4e759ba57df66c9..117cafa508058753cb841e207f707b571d705b82 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -1045,8 +1045,8 @@ orderings on types and terms.
   \[
   \begin{array}{l}
   \begin{array}{rl|rl}
-    A ::= & \colorbox{lightgray}{$\dynv$} \mid U \u B \mid 0 \mid A_1 + A_2 \mid 1 \mid A_1 \times A_2 & 
-    \u B ::= & \colorbox{lightgray}{$\dync$} \mid \u F A \mid \top \mid \u B_1 \with \u B_2 \mid A \to \u B\\
+    A ::= & \colorbox{lightgray}{$\dynv$} \mid U \u B \mid 0 \mid A_1 + A_2 \mid 1 \mid A_1 \times A_2 & X \mid \mu X. A
+    \u B ::= & \colorbox{lightgray}{$\dync$} \mid \u F A \mid \top \mid \u B_1 \with \u B_2 \mid A \to \u B \mid \u Y \mid \u \nu \u Y. \u B\\
 
     V ::= & \begin{array}{l}
             \colorbox{lightgray}{$\upcast A {A'} V$} \mid x \mid \abort{V} \\
@@ -1502,6 +1502,10 @@ in the domain~\citep{newahmed18,newlicata2018-fscd}.
     
   \begin{mathpar}
     \framebox{$A \ltdyn A'$ and $\u B \ltdyn \u B'$}
+
+    \inferrule{}{A[\mu X.A/X] \ltdyn \mu X. A}
+
+    \inferrule{A[A'/X] \ltdyn A'}{\mu X. A \ltdyn A'}
     
     \inferrule*[lab=VTyRefl]{ }{A \ltdyn A}