milestone update in basic_2, update in ground and static_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / jsx_jsx.ma

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 b53d0d6f7635520003569e6ec1c9eea749af5b0c..0b93e69ebd08d81a3dc0f0a44068b41df4d78a17 100644 (file)
--- 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