X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Fdrops_weight.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Fdrops_weight.ma;h=f0c5f355ad34488a27ffaf3dac0afa6dbe58424b;hb=d3636c8688ec08cc39eb7ce6c1918b25bbccc349;hp=2df6d983230857dbfa16ab9a0a0053ca0de0f007;hpb=7fff13721f6e7040e76faad31583b1cb86693d2c;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_weight.ma
index 2df6d9832..f0c5f355a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_weight.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_weight.ma
@@ -16,9 +16,9 @@ include "basic_2/grammar/cl_restricted_weight.ma".
 include "basic_2/relocation/lifts_weight.ma".
 include "basic_2/relocation/drops.ma".
 
-(* GENERAL SLICING FOR LOCAL ENVIRONMENTS ***********************************)
+(* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************)
 
-(* Forward lemmas on weight for local environments **************************)
+(* Forward lemmas with weight for local environments ************************)
 
 (* Basic_2A1: includes: drop_fwd_lw *)
 lemma drops_fwd_lw: ∀L1,L2,c,f. ⬇*[c, f] L1 ≡ L2 → ♯{L2} ≤ ♯{L1}.
@@ -40,7 +40,7 @@ lemma drops_fwd_lw_lt: ∀L1,L2,f. ⬇*[Ⓣ, f] L1 ≡ L2 →
 ]
 qed-.
 
-(* Forward lemmas on restricted weight for closures *************************)
+(* Forward lemmas with restricted weight for closures ***********************)
 
 (* Basic_2A1: includes: drop_fwd_rfw *)
 lemma drops_pair2_fwd_rfw: ∀I,L,K,V,c,f. ⬇*[c, f] L ≡ K.ⓑ{I}V → ∀T. ♯{K, V} < ♯{L, T}.