Thanks to Guarrigue, code for Serializer functor simplified using

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / unfold / thin.ma

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 39d4d12c405f292063c49a67cb38ae2c3261b64b..aaead6136c81d60f630a2da5e01f212c42ac7cb1 100644 (file)
--- 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 *********************************************************)