diff --git a/tRules.tex b/tRules.tex
index ff727c8..6cc565f 100644
--- a/tRules.tex
+++ b/tRules.tex
@@ -460,15 +460,18 @@ $\begin{array}{l}
 \end{array}$
 \\[1em]
 $\begin{array}{l}
+%TODO: why is dom(\Delta) subset of fv(N) a restriction. This excludes X,Y^X.Pair<X,Y>? 
+%TODO: we do not allow X.Pair<X,X> in the t-let (could we allow it? what about L and U being WTVs?)
     \typerule{T-Let}\\
     \begin{array}{@{}c}
         \Delta | \Gamma \vdash \expr{t}_1 : \type{T}_1 \quad \quad
-        \Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N}
+        %\Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N}
+        \Delta \vdash \type{T}_1 <: \wctype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{C}{\ol{X}}
         \\
-        \Delta, \Delta' | \Gamma, \expr{x} : \wcNtype{}{N} \vdash \expr{t}_2 : \type{T}_2 \quad \quad
+        \Delta, \Delta' | \Gamma, \expr{x} : \wctype{}{C}{\ol{X}} \vdash \expr{t}_2 : \type{T}_2 \quad \quad
         \Delta, \Delta' \vdash  \type{T}_2 <: \type{T} \quad \quad
-        \text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
-        \Delta \vdash \type{T}, \wcNtype{\Delta'}{N} \ \ok
+        % \text{dom}(\Delta') \subseteq \text{fv}(\type{N})  \quad \quad
+        \Delta \vdash \type{T}, \wctype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{C}{\ol{X}} \ \ok
         \\
         \hline
     \vspace*{-0.3cm}\\