X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Funfold%2Fthin.ma;h=aaead6136c81d60f630a2da5e01f212c42ac7cb1;hb=db7ecce6c398a42f14557067bf18b61cf75da80e;hp=39d4d12c405f292063c49a67cb38ae2c3261b64b;hpb=fc5a0d62ece398d8547dda0f429b9f1e24bca306;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/thin.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/thin.ma
index 39d4d12c4..aaead6136 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/thin.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/thin.ma
@@ -14,12 +14,12 @@
 
 include "basic_2/unfold/ltpss.ma".
 
-(* LOCAL ENVIRONMENT THINNING ***********************************************)
+(* BASIC LOCAL ENVIRONMENT THINNING *****************************************)
 
 definition thin: nat → nat → relation lenv ≝
-                 λd,e,L1,L2. ∃∃L. L1 [d, e] ▶* L & ⇩[d, e] L ≡ L2.
+                 λd,e,L1,L2. ∃∃L. L1 ▶* [d, e] L & ⇩[d, e] L ≡ L2.
 
-interpretation "thinning (local environment)"
+interpretation "basic thinning (local environment)"
    'TSubst L1 d e L2 = (thin d e L1 L2).
 
 (* Basic properties *********************************************************)