X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Fgr_pat_lt.ma;h=8fc080ed62317516833515d565b5d0fe19467a37;hp=50b59ce89f2f59cfb3f1923f87b675ace875c54b;hb=2ed8d2abcc3b0687141b627061b63350a0b200bd;hpb=b367de0252e88d6b0476648d5ceac7e4aeffca27

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat_lt.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat_lt.ma
index 50b59ce89..8fc080ed6 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat_lt.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat_lt.ma
@@ -16,9 +16,9 @@ include "ground/arith/pnat_pred.ma".
 include "ground/arith/pnat_lt.ma".
 include "ground/relocation/gr_pat.ma".
 
-(* POSITIVE APPLICATION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* POSITIVE APPLICATION FOR GENERIC RELOCATION MAPS *************************)
 
-(* Forward lemmas with plt and ple *****************************************************)
+(* Destructions with plt and ple ********************************************)
 
 (*** at_increasing *)
 lemma gr_pat_increasing (i2) (i1) (f):
@@ -47,7 +47,7 @@ lemma gr_pat_des_id (f) (i): @❪i,f❫ ≘ i → ⫯⫱f = f.
 #H elim (plt_ge_false … H) -H //
 qed-.
 
-(* Properties with ple *********************************************************)
+(* Constructions with ple ***************************************************)
 
 (*** at_le_ex *)
 lemma gr_pat_le_ex (j2) (i2) (f):