fix

diff --git a/helm/papers/system_T/t.tex b/helm/papers/system_T/t.tex
index 77b159fffd59a0ea933a8e23fcfcbc47021118d8..14ead6b91ba2cf1713ff1d4991f9e1f60be1b2d6 100644 (file)
--- a/helm/papers/system_T/t.tex
+++ b/helm/papers/system_T/t.tex
@@ -453,9 +453,9 @@ realizes $\triUP\{C(X)_i, c_i\}$ by assumption and since we are in the base
 case $\triUP\{C(X)_i, c_i\}$ is of the form $\vec{\forall t:T}.Q(c_i~\vec{t})$.
 Thus $f_i~\vec{m} \R Q(c_i~\vec{m})$.
 \\ 
-In the induction step we have as induction hypothesis that each recursive
-argument $t_i$ of the head constructor $c_i$ is realized by $r_i\equiv
-\Rx~\vec{f}~t_i$. By the third rule of $\triDOWN$ we obtain the reduct
+In the induction step we have as induction hypothesis that for each recursive
+argument $t_i$ of the head constructor $c_i$, $r_i\equiv
+\Rx~\vec{f}~t_i \R Q(t_i)$. By the third rule of $\triDOWN$ we obtain the reduct
 $f_i~\vec{m}~\vec{t~r}$ (here we write first all the non recursive arguments,
 then all the recursive one. In general they can be mixed and the proof is
 exactly the same but the notation is really heavier). We know by hypothesis