update in basic_2

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

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 79b41f785807c24e5a94485bc426ce22da2fc5fe..aa13ac53a4b3458aaf3a1435bb899182b38be6c3 100644 (file)
--- 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.