Fix S-Extends

constraints.tex

@@ -173,7 +173,7 @@ The ones to already typed methods and calls to untyped methods.
                   \end{array}\\
             & \ |\ 
             (\exptype{C}{\ol{X} \triangleleft \ol{N}}.\texttt{m} : \generics{\ol{Y} \triangleleft \ol{N'}}\overline{\type{T}} \to \type{T}) \in 
-                {\mtypeEnvironment}
+                {\mtypeEnvironment}, \, |\ol{T}| = |\ol{e}|
             , \, \overline{\wtv{a}} \text{ fresh}, \, \overline{\wtv{b}} \text{ fresh} }
         \end{array}\\
       \mathbf{in} & \consSet_R \cup \overline{\consSet} \cup \constraint

tRules.tex

@@ -95,12 +95,12 @@ $\begin{array}{l}
 $\begin{array}{l}
     \typerule{S-Extends}\\
     \begin{array}{@{}c}
-        \texttt{class}\ \exptype{C}{\overline{\type{X} \triangleleft \type{U}}} \triangleleft \exptype{D}{\ol{S}} \ \{ \ldots \} \\
+        \texttt{class}\ \exptype{C}{\overline{\type{X} \triangleleft \type{U}}} \triangleleft \type{N} \ \{ \ldots \} \\
         \ol{X} \cap \text{dom}(\Delta) = \emptyset
         \\
         \hline
     \vspace*{-0.3cm}\\
-        \Delta \vdash \wcNtype{\Delta'}{\type{N}} <: \wcNtype{\Delta'}{[\ol{T}/\ol{X}]\type{N}}
+        \Delta \vdash \wctype{\Delta'}{C}{\ol{T}} <: \wcNtype{\Delta'}{[\ol{T}/\ol{X}]\type{N}}
     \end{array}
 \end{array}$
 $\begin{array}{l}