X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Fdrops_lexs.ma;h=9ebd8afe72d6a3105a23bb2762d33010e82b302d;hb=9a023f554e56d6edbbb2eeaf17ce61e31857ef4a;hp=f639424f4c3a68ebf01ae8d6c1892ac0cbd5c42e;hpb=629687db8a55432e95c82f0c79e3f51c023e65a6;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lexs.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lexs.ma
index f639424f4..9ebd8afe7 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lexs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lexs.ma
@@ -14,9 +14,9 @@
 
 include "basic_2/relocation/drops.ma".
 
-(* GENERAL SLICING FOR LOCAL ENVIRONMENTS ***********************************)
+(* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************)
 
-(* Properties on general entrywise extension of context-sensitive relations *)
+(* Properties with entrywise extension of context-sensitive relations *******)
 
 (* Basic_2A1: includes: lpx_sn_deliftable_dropable *)
 lemma lexs_deliftable_dropable: ∀RN,RP. d_deliftable2_sn RN → d_deliftable2_sn RP →