X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Flsubsx_lfsx.ma;h=511e62369c283ff57dd919168505966b09066a33;hb=f129bbbfda0e65a5f92ec086246f6e288376d4f9;hp=059cb1ece177dee1167068ee30d3f8c145d34bd2;hpb=54c4e854515cbcb1376881e9aedad006bf6545f2;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx_lfsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx_lfsx.ma
index 059cb1ece..511e62369 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx_lfsx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx_lfsx.ma
@@ -16,9 +16,9 @@ include "basic_2/rt_computation/lfsx_drops.ma".
 include "basic_2/rt_computation/lfsx_lfpxs.ma".
 include "basic_2/rt_computation/lsubsx.ma".
 
-(* CLEAR OF STRONGLY NORMALIZING ENTRIES FOR UNCOUNTED RT-TRANSITION ********)
+(* CLEAR OF STRONGLY NORMALIZING ENTRIES FOR UNBOUND RT-TRANSITION **********)
 
-(* Properties with strong normalizing env's for uncounted rt-transition *****)
+(* Properties with strong normalizing env's for unbound rt-transition *******)
 
 (* Basic_2A1: uses: lsx_cpx_trans_lcosx *)
 lemma lfsx_cpx_trans_lsubsx: ∀h,o,G,L0,T1,T2. ⦃G, L0⦄ ⊢ T1 ⬈[h] T2 →
@@ -63,7 +63,7 @@ lemma lfsx_cpx_trans: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 →
                       G ⊢ ⬈*[h, o, T1] 𝐒⦃L⦄ → G ⊢ ⬈*[h, o, T2] 𝐒⦃L⦄.
 /3 width=6 by lfsx_cpx_trans_lsubsx, lsubsx_refl/ qed-.
 
-(* Properties with strong normalizing env's for uncounted rt-computation ****)
+(* Properties with strong normalizing env's for unbound rt-computation ******)
 
 lemma lfsx_cpxs_trans: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 →
                        G ⊢ ⬈*[h, o, T1] 𝐒⦃L⦄ → G ⊢ ⬈*[h, o, T2] 𝐒⦃L⦄.