From: Enrico Tassi Date: Tue, 8 Nov 2005 14:59:53 +0000 (+0000) Subject: fix X-Git-Tag: V_0_7_2_3~103 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c9b7cd573efcb687d5d0e225bf3990b656446dc6;p=helm.git fix --- diff --git a/helm/papers/system_T/t.tex b/helm/papers/system_T/t.tex index 77b159fff..14ead6b91 100644 --- 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