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

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_map.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_map.ma
index ac568e1f0..53d052062 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_map.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_map.ma
@@ -36,7 +36,7 @@ interpretation
   "next (generic relocation maps)"
   'UpArrow f = (gr_next f).
 
-(* Basic properties (specific) **********************************************)
+(* Basic constructions (specific) *******************************************)
 
 (*** push_rew *)
 lemma gr_push_unfold (f): Ⓕ⨮f = ⫯f.
@@ -46,7 +46,7 @@ lemma gr_push_unfold (f): Ⓕ⨮f = ⫯f.
 lemma gr_next_unfold (f): Ⓣ⨮f = ↑f.
 // qed.
 
-(* Basic inversion lemmas ***************************************************)
+(* Basic inversions *********************************************************)
 
 (*** injective_push *)
 lemma eq_inv_gr_push_bi: injective ? ? gr_push.