- minor corrections

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

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 f639424f4c3a68ebf01ae8d6c1892ac0cbd5c42e..9ebd8afe72d6a3105a23bb2762d33010e82b302d 100644 (file)
--- 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 →