X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fjsx_jsx.ma;h=0b93e69ebd08d81a3dc0f0a44068b41df4d78a17;hb=3c7b4071a9ac096b02334c1d47468776b948e2de;hp=b53d0d6f7635520003569e6ec1c9eea749af5b0c;hpb=5b5dca0c118dfbe3ba8f0514ef07549544eb7810;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_jsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_jsx.ma
index b53d0d6f7..0b93e69eb 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_jsx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_jsx.ma
@@ -14,12 +14,12 @@
 
 include "basic_2/rt_computation/jsx_csx.ma".
 
-(* COMPATIBILITY OF STRONG NORMALIZATION FOR UNBOUND RT-TRANSITION **********)
+(* COMPATIBILITY OF STRONG NORMALIZATION FOR EXTENDED RT-TRANSITION *********)
 
 (* Main properties **********************************************************)
 
-theorem jsx_trans (h) (G): Transitive … (jsx h G).
-#h #G #L1 #L #H elim H -L1 -L
+theorem jsx_trans (G): Transitive … (jsx G).
+#G #L1 #L #H elim H -L1 -L
 [ #L2 #H
   >(jsx_inv_atom_sn … H) -L2 //
 | #I #K1 #K #_ #IH #L2 #H