update in ground

[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / gr_map.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_map.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_map.ma
index ac568e1f0e52ed71c9e425686a0c58d26b22aac2..53d0520629c3c3d9b61ed79d0a727e502e36ec1a 100644 (file)
--- 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.