diff --git a/9-type-aliases-redux/latex/kind-judgements.pdf b/9-type-aliases-redux/latex/kind-judgements.pdf
index 79c56e8..62a8a19 100644
Binary files a/9-type-aliases-redux/latex/kind-judgements.pdf and b/9-type-aliases-redux/latex/kind-judgements.pdf differ
diff --git a/9-type-aliases-redux/latex/kind-judgements.tex b/9-type-aliases-redux/latex/kind-judgements.tex
index 6b13958..1c11238 100644
--- a/9-type-aliases-redux/latex/kind-judgements.tex
+++ b/9-type-aliases-redux/latex/kind-judgements.tex
@@ -104,9 +104,9 @@
 		}
 		\and
 		\inferrule[KCSubsumption]{
-			\kindAna{\Delta;\hPhi}{\dtau}{\Ty}
+			\kindAna{\Delta;\hPhi}{\dtau}{\hkappa}
 		} {
-                        \kconsubkind{\Delta;\hPhi}{\SKind[\Ty]{\dtau}}{\Ty}
+                        \kconsubkind{\Delta;\hPhi}{\SKind{\dtau}}{\hkappa}
 		}
 	\end{mathpar}
 \end{minipage}
@@ -173,7 +173,7 @@
 		}
                 \and
                 \inferrule[KESingReduc]{
-                    \kindAna{\Delta;\hPhi}{\dtau}{\SKind{\dtau'}}
+                    \kcequiv{\Delta;\hPhi}{\dtau'}{\dtau}
                 }{
                 \kequiv{\Delta;\hPhi}{\SKind[\SKind{\dtau'}]{\dtau}}{\SKind{\dtau'}}
                 }
@@ -260,7 +260,7 @@
 \begin{minipage}{\linewidth}
 	\judgbox
 	{\kcequiv{\Delta;\hPhi}{\dtau_1}{\dtau_2}}
-	{$\dtau_1$ is equivalent to $\dtau_2$} \;\\
+	{$\dtau_1$ is equivalent to $\dtau_2$ at kind $\Ty$} \;\\
 	\begin{mathpar}
 		\inferrule[KCESymm]{
 			\kcequiv{\Delta;\hPhi}{\dtau_1}{\dtau_2}
@@ -276,7 +276,7 @@
 		}
 		\and
 		\inferrule[KCESingEquiv]{
-			\kindAna{\Delta;\hPhi}{\dtau_1}{\SKind{\dtau_2}}
+                        \kindAna{\Delta;\hPhi}{\dtau_1}{\SKind[\Ty]{\dtau_2}}
 		} {
 			\kcequiv{\Delta;\hPhi}{\dtau_1}{\dtau_2}
 		}
@@ -327,20 +327,20 @@
 	{$\htau$ synthesizes kind $\hkappa$ and elaborates to $\dtau$}
 	\begin{mathpar}
 		\inferrule[TElabSConst]{ }{
-			\elabSyn{\hPhi}{c}{\SKind{c}}{c}{\EmptyDelta}
+                        \elabSyn{\hPhi}{c}{\SKind[\Ty]{c}}{c}{\EmptyDelta}
 		}
 		\and
 		\inferrule[TElabSBinOp]{
 			\elabAna{\hPhi}{\htau_1}{\Ty}{\dtau_1}{\Delta_1} \\
 			\elabAna{\hPhi}{\htau_2}{\Ty}{\dtau_2}{\Delta_2}
 		}{
-			\elabSyn{\hPhi}{\htau_1 \oplus \htau_2}{\SKind{\dtau_1 \oplus \dtau_2}}{\dtau_1 \oplus \dtau_2}{\Delta_1 \cup \Delta_2}
+                        \elabSyn{\hPhi}{\htau_1 \oplus \htau_2}{\SKind[\Ty]{\dtau_1 \oplus \dtau_2}}{\dtau_1 \oplus \dtau_2}{\Delta_1 \cup \Delta_2}
 		}
 		\and
 		\inferrule[TElabSList]{
 			\elabAna{\hPhi}{\htau}{\Ty}{\dtau}{\Delta}
 		} {
-			\elabSyn{\hPhi}{\hlist{\htau}}{\SKind{\hlist{\dtau}}}{\hlist{\dtau}}{\Delta}
+                        \elabSyn{\hPhi}{\hlist{\htau}}{\SKind[\Ty]{\hlist{\dtau}}}{\hlist{\dtau}}{\Delta}
 		}
 		\and
 		\inferrule[TElabSVar]{