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

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.