]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma
- minor corrections
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / relocation / drops_lreq.ma
index cde181037742515e6c412a0703b8c0287a1629a9..56f2fbf85e084afaa116f26c532710f8e083dcad 100644 (file)
@@ -15,9 +15,9 @@
 include "basic_2/relocation/drops_ceq.ma".
 include "basic_2/relocation/drops_lexs.ma".
 
-(* GENERAL SLICING FOR LOCAL ENVIRONMENTS ***********************************)
+(* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************)
 
-(* Properties on ranged equivalence for local environments ******************)
+(* Properties with ranged equivalence for local environments ****************)
 
 lemma lreq_dedropable: dedropable_sn lreq.
 @lexs_liftable_dedropable