X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fcsx_reqx.ma;h=5d35690cc7ef19e42cab29dcd0060a700d838399;hb=b2cdc4abd9ac87e39bc51b0d9c38daea179adbd5;hp=59e5eb289b9a02b248ab631d61ce0f016618e7ba;hpb=57ae1762497a5f3ea75740e2908e04adb8642cc2;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_reqx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_reqx.ma
index 59e5eb289..5d35690cc 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_reqx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_reqx.ma
@@ -15,22 +15,22 @@
 include "basic_2/rt_transition/cpx_reqx.ma".
 include "basic_2/rt_computation/csx_csx.ma".
 
-(* STRONGLY NORMALIZING TERMS FOR UNBOUND PARALLEL RT-TRANSITION ************)
+(* STRONGLY NORMALIZING TERMS FOR EXTENDED PARALLEL RT-TRANSITION ***********)
 
 (* Properties with sort-irrelevant equivalence for local environments *******)
 
 (* Basic_2A1: uses: csx_lleq_conf *)
-lemma csx_reqx_conf (h) (G) (L1):
-      ∀T. ❪G,L1❫ ⊢ ⬈*𝐒[h] T →
-      ∀L2. L1 ≛[T] L2 → ❪G,L2❫ ⊢ ⬈*𝐒[h] T.
-#h #G #L1 #T #H
+lemma csx_reqx_conf (G) (L1):
+      ∀T. ❪G,L1❫ ⊢ ⬈*𝐒 T →
+      ∀L2. L1 ≛[T] L2 → ❪G,L2❫ ⊢ ⬈*𝐒 T.
+#G #L1 #T #H
 @(csx_ind … H) -T #T1 #_ #IH #L2 #HL12
 @csx_intro #T2 #HT12 #HnT12
-elim (reqx_cpx_trans … HL12 … HT12) -HT12
-/5 width=5 by cpx_reqx_conf_sn, csx_teqx_trans, teqx_trans/
+lapply (reqx_cpx_trans … HL12 … HT12) -HT12
+/3 width=4 by cpx_reqx_conf_sn/
 qed-.
 
 (* Basic_2A1: uses: csx_lleq_trans *)
-lemma csx_reqx_trans (h) (G) (L2):
-      ∀L1,T. L1 ≛[T] L2 → ❪G,L2❫ ⊢ ⬈*𝐒[h] T → ❪G,L1❫ ⊢ ⬈*𝐒[h] T.
+lemma csx_reqx_trans (G) (L2):
+      ∀L1,T. L1 ≛[T] L2 → ❪G,L2❫ ⊢ ⬈*𝐒 T → ❪G,L1❫ ⊢ ⬈*𝐒 T.
 /3 width=3 by csx_reqx_conf, reqx_sym/ qed-.