- minor corrections

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / relocation / drops_weight.ma

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 2df6d983230857dbfa16ab9a0a0053ca0de0f007..f0c5f355ad34488a27ffaf3dac0afa6dbe58424b 100644 (file)
--- 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}.