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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lpxs.ma
index 79b41f785..aa13ac53a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lpxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lpxs.ma
@@ -18,9 +18,9 @@ include "basic_2/rt_computation/cpxs_lpx.ma".
 include "basic_2/rt_computation/lpxs.ma".
 include "basic_2/rt_computation/lfpxs.ma".
 
-(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ****)
+(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******)
 
-(* Properties with uncounted parallel rt-computation for local environments *)
+(* Properties with unbound parallel rt-computation for local environments ***)
 
 lemma lfpxs_lpxs: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2.
 /2 width=1 by tc_lfxs_lex/ qed.
@@ -29,7 +29,7 @@ lemma lfpxs_lpxs_lfeq: ∀h,G,L1,L. ⦃G, L1⦄ ⊢ ⬈*[h] L →
                        ∀L2,T. L ≡[T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2.
 /2 width=3 by tc_lfxs_lex_lfeq/ qed.
 
-(* Inversion lemmas with uncounted parallel rt-computation for local envs ***)
+(* Inversion lemmas with unbound parallel rt-computation for local envs *****)
 
 lemma lfpxs_inv_lpxs_lfeq: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 →
                            ∃∃L. ⦃G, L1⦄ ⊢ ⬈*[h] L & L ≡[T] L2.