From 2ed8d2abcc3b0687141b627061b63350a0b200bd Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sat, 29 May 2021 19:46:15 +0200
Subject: [PATCH] update in ground

+ comments restyled
---
 .../contribs/lambdadelta/bin/recomm/bGroundArith.mrc |  5 +++++
 .../contribs/lambdadelta/bin/recomm/pGroundArith.mrc |  1 +
 .../contribs/lambdadelta/bin/recomm/rGroundArith.mrc |  1 +
 .../lambdadelta/bin/recomm/recommGcbGroundArith.ml   |  6 ++++++
 .../lambdadelta/bin/recomm/recommGcpGroundArith.ml   |  1 +
 .../lambdadelta/bin/recomm/recommGcrGroundArith.ml   |  1 +
 .../lambdadelta/ground/arith/nat_plus_rplus.ma       |  4 ++--
 .../contribs/lambdadelta/ground/lib/stream_tls_eq.ma |  2 +-
 .../lambdadelta/ground/relocation/fr2_append.ma      |  4 ++--
 .../lambdadelta/ground/relocation/fr2_minus.ma       |  4 ++--
 .../lambdadelta/ground/relocation/fr2_nat.ma         |  4 ++--
 .../lambdadelta/ground/relocation/fr2_nat_nat.ma     |  4 ++--
 .../lambdadelta/ground/relocation/fr2_plus.ma        |  6 +++---
 .../lambdadelta/ground/relocation/gr_after.ma        |  6 +++---
 .../lambdadelta/ground/relocation/gr_after_after.ma  |  6 +++---
 .../ground/relocation/gr_after_after_ist.ma          |  4 ++--
 .../lambdadelta/ground/relocation/gr_after_basic.ma  |  4 ++--
 .../lambdadelta/ground/relocation/gr_after_eq.ma     |  4 ++--
 .../lambdadelta/ground/relocation/gr_after_isi.ma    |  6 +++---
 .../lambdadelta/ground/relocation/gr_after_ist.ma    |  6 +++---
 .../ground/relocation/gr_after_ist_isi.ma            |  4 ++--
 .../lambdadelta/ground/relocation/gr_after_isu.ma    |  4 ++--
 .../ground/relocation/gr_after_nat_uni_tls.ma        |  4 ++--
 .../lambdadelta/ground/relocation/gr_after_pat.ma    |  4 ++--
 .../ground/relocation/gr_after_pat_tls.ma            |  4 ++--
 .../ground/relocation/gr_after_pat_uni_tls.ma        |  8 ++++----
 .../lambdadelta/ground/relocation/gr_after_uni.ma    |  6 +++---
 .../lambdadelta/ground/relocation/gr_basic.ma        |  4 ++--
 .../lambdadelta/ground/relocation/gr_coafter.ma      | 12 ++++++------
 .../ground/relocation/gr_coafter_coafter.ma          |  4 ++--
 .../ground/relocation/gr_coafter_coafter_ist.ma      |  4 ++--
 .../lambdadelta/ground/relocation/gr_coafter_eq.ma   |  4 ++--
 .../lambdadelta/ground/relocation/gr_coafter_isi.ma  |  6 +++---
 .../ground/relocation/gr_coafter_ist_isf.ma          |  6 +++---
 .../ground/relocation/gr_coafter_ist_isi.ma          |  6 +++---
 .../lambdadelta/ground/relocation/gr_coafter_isu.ma  |  4 ++--
 .../ground/relocation/gr_coafter_nat_tls.ma          |  4 ++--
 .../ground/relocation/gr_coafter_nat_tls_pushs.ma    |  4 ++--
 .../ground/relocation/gr_coafter_pat_tls.ma          |  4 ++--
 .../ground/relocation/gr_coafter_uni_pushs.ma        |  6 +++---
 .../contribs/lambdadelta/ground/relocation/gr_eq.ma  |  4 ++--
 .../lambdadelta/ground/relocation/gr_fcla.ma         |  6 +++---
 .../lambdadelta/ground/relocation/gr_fcla_eq.ma      |  4 ++--
 .../lambdadelta/ground/relocation/gr_fcla_fcla.ma    |  4 ++--
 .../lambdadelta/ground/relocation/gr_fcla_uni.ma     |  4 ++--
 .../contribs/lambdadelta/ground/relocation/gr_id.ma  |  4 ++--
 .../lambdadelta/ground/relocation/gr_id_eq.ma        |  6 +++---
 .../contribs/lambdadelta/ground/relocation/gr_isd.ma |  6 +++---
 .../lambdadelta/ground/relocation/gr_isd_eq.ma       |  8 ++++----
 .../lambdadelta/ground/relocation/gr_isd_nexts.ma    |  6 +++---
 .../lambdadelta/ground/relocation/gr_isd_tl.ma       |  4 ++--
 .../lambdadelta/ground/relocation/gr_isd_tls.ma      |  4 ++--
 .../contribs/lambdadelta/ground/relocation/gr_isf.ma |  8 ++++----
 .../lambdadelta/ground/relocation/gr_isf_eq.ma       |  4 ++--
 .../lambdadelta/ground/relocation/gr_isf_isu.ma      |  4 ++--
 .../lambdadelta/ground/relocation/gr_isf_pushs.ma    |  6 +++---
 .../lambdadelta/ground/relocation/gr_isf_tl.ma       |  6 +++---
 .../lambdadelta/ground/relocation/gr_isf_tls.ma      |  6 +++---
 .../lambdadelta/ground/relocation/gr_isf_uni.ma      |  4 ++--
 .../contribs/lambdadelta/ground/relocation/gr_isi.ma |  6 +++---
 .../lambdadelta/ground/relocation/gr_isi_eq.ma       |  8 ++++----
 .../lambdadelta/ground/relocation/gr_isi_id.ma       |  6 +++---
 .../lambdadelta/ground/relocation/gr_isi_pat.ma      |  8 ++++----
 .../lambdadelta/ground/relocation/gr_isi_pushs.ma    |  6 +++---
 .../lambdadelta/ground/relocation/gr_isi_tl.ma       |  4 ++--
 .../lambdadelta/ground/relocation/gr_isi_tls.ma      |  4 ++--
 .../lambdadelta/ground/relocation/gr_isi_uni.ma      |  6 +++---
 .../contribs/lambdadelta/ground/relocation/gr_ist.ma |  6 +++---
 .../lambdadelta/ground/relocation/gr_ist_isi.ma      |  4 ++--
 .../lambdadelta/ground/relocation/gr_ist_ist.ma      |  6 +++---
 .../lambdadelta/ground/relocation/gr_ist_tls.ma      |  4 ++--
 .../contribs/lambdadelta/ground/relocation/gr_isu.ma |  6 +++---
 .../lambdadelta/ground/relocation/gr_isu_tl.ma       |  6 +++---
 .../lambdadelta/ground/relocation/gr_isu_uni.ma      |  6 +++---
 .../contribs/lambdadelta/ground/relocation/gr_map.ma |  4 ++--
 .../contribs/lambdadelta/ground/relocation/gr_nat.ma |  8 ++++----
 .../lambdadelta/ground/relocation/gr_nat_basic.ma    |  6 +++---
 .../lambdadelta/ground/relocation/gr_nat_uni.ma      |  6 +++---
 .../lambdadelta/ground/relocation/gr_nexts.ma        |  4 ++--
 .../lambdadelta/ground/relocation/gr_nexts_eq.ma     |  4 ++--
 .../contribs/lambdadelta/ground/relocation/gr_pat.ma |  6 +++---
 .../lambdadelta/ground/relocation/gr_pat_basic.ma    |  6 +++---
 .../lambdadelta/ground/relocation/gr_pat_eq.ma       |  6 +++---
 .../lambdadelta/ground/relocation/gr_pat_id.ma       |  6 +++---
 .../lambdadelta/ground/relocation/gr_pat_lt.ma       |  6 +++---
 .../lambdadelta/ground/relocation/gr_pat_pat.ma      |  4 ++--
 .../lambdadelta/ground/relocation/gr_pat_pat_id.ma   |  6 +++---
 .../lambdadelta/ground/relocation/gr_pat_tls.ma      |  6 +++---
 .../lambdadelta/ground/relocation/gr_pat_uni.ma      |  6 +++---
 .../lambdadelta/ground/relocation/gr_pushs.ma        |  4 ++--
 .../lambdadelta/ground/relocation/gr_pushs_eq.ma     |  4 ++--
 .../lambdadelta/ground/relocation/gr_sand.ma         |  6 +++---
 .../lambdadelta/ground/relocation/gr_sand_eq.ma      |  4 ++--
 .../contribs/lambdadelta/ground/relocation/gr_sdj.ma |  8 ++++----
 .../lambdadelta/ground/relocation/gr_sdj_eq.ma       |  4 ++--
 .../lambdadelta/ground/relocation/gr_sdj_isi.ma      |  6 +++---
 .../contribs/lambdadelta/ground/relocation/gr_sle.ma | 12 ++++++------
 .../lambdadelta/ground/relocation/gr_sle_eq.ma       |  6 +++---
 .../lambdadelta/ground/relocation/gr_sle_isd.ma      |  6 +++---
 .../lambdadelta/ground/relocation/gr_sle_isi.ma      |  6 +++---
 .../lambdadelta/ground/relocation/gr_sle_pushs.ma    |  4 ++--
 .../lambdadelta/ground/relocation/gr_sle_sle.ma      |  4 ++--
 .../lambdadelta/ground/relocation/gr_sle_tls.ma      |  4 ++--
 .../contribs/lambdadelta/ground/relocation/gr_sor.ma | 12 ++++++------
 .../ground/relocation/gr_sor_coafter_ist_isf.ma      |  4 ++--
 .../lambdadelta/ground/relocation/gr_sor_eq.ma       |  4 ++--
 .../lambdadelta/ground/relocation/gr_sor_fcla.ma     | 10 +++++-----
 .../lambdadelta/ground/relocation/gr_sor_isf.ma      |  8 ++++----
 .../lambdadelta/ground/relocation/gr_sor_isi.ma      |  8 ++++----
 .../lambdadelta/ground/relocation/gr_sor_sle.ma      |  6 +++---
 .../lambdadelta/ground/relocation/gr_sor_sor.ma      |  6 +++---
 .../lambdadelta/ground/relocation/gr_sor_sor_sle.ma  |  4 ++--
 .../lambdadelta/ground/relocation/gr_sor_tls.ma      |  4 ++--
 .../contribs/lambdadelta/ground/relocation/gr_tl.ma  |  6 +++---
 .../lambdadelta/ground/relocation/gr_tl_eq.ma        |  8 ++++----
 .../lambdadelta/ground/relocation/gr_tl_eq_eq.ma     |  4 ++--
 .../contribs/lambdadelta/ground/relocation/gr_tls.ma |  4 ++--
 .../lambdadelta/ground/relocation/gr_tls_eq.ma       |  4 ++--
 .../lambdadelta/ground/relocation/gr_tls_nexts_eq.ma |  4 ++--
 .../lambdadelta/ground/relocation/gr_tls_pushs.ma    |  4 ++--
 .../lambdadelta/ground/relocation/gr_tls_pushs_eq.ma |  4 ++--
 .../contribs/lambdadelta/ground/relocation/gr_uni.ma |  4 ++--
 .../lambdadelta/ground/relocation/gr_uni_eq.ma       |  6 +++---
 123 files changed, 328 insertions(+), 313 deletions(-)

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/bGroundArith.mrc b/matita/matita/contribs/lambdadelta/bin/recomm/bGroundArith.mrc
index 6cb885931..6b41617bd 100644
--- a/matita/matita/contribs/lambdadelta/bin/recomm/bGroundArith.mrc
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/bGroundArith.mrc
@@ -1,10 +1,15 @@
 PcsAnd b "" true false
+psucc
+ppred
+pplus
 ple
 plt
 niter
 ntri
+npsucc
 nsucc
 npred
+nrplus, rplus
 nplus
 nminus
 nmax
diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/pGroundArith.mrc b/matita/matita/contribs/lambdadelta/bin/recomm/pGroundArith.mrc
index 226e772f3..89e9878c2 100644
--- a/matita/matita/contribs/lambdadelta/bin/recomm/pGroundArith.mrc
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/pGroundArith.mrc
@@ -1,2 +1,3 @@
 PcsPar p "" true false
 (semigroup properties)
+(decidability)
diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/rGroundArith.mrc b/matita/matita/contribs/lambdadelta/bin/recomm/rGroundArith.mrc
index ac34215e1..f57774784 100644
--- a/matita/matita/contribs/lambdadelta/bin/recomm/rGroundArith.mrc
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/rGroundArith.mrc
@@ -5,6 +5,7 @@ TRICHOTOMY OPERATOR
 NAT-INJECTION
 SUCCESSOR
 PREDECESSOR
+RIGHT ADDITION
 ADDITION
 SUBTRACTION
 LEFT SUBTRACTION
diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundArith.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundArith.ml
index d9f7a0d10..c2f448113 100644
--- a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundArith.ml
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundArith.ml
@@ -16,12 +16,18 @@ let step k st outs ins =
   | "nmax" :: tl -> k T.OK ("nmax" :: outs) tl
   | "nminus" :: tl -> k T.OK ("nminus" :: outs) tl
   | "nplus" :: tl -> k T.OK ("nplus" :: outs) tl
+  | "nrplus" :: tl -> k T.OK ("nrplus" :: outs) tl
+  | "rplus" :: tl -> k T.OK ("nrplus" :: outs) tl
   | "npred" :: tl -> k T.OK ("npred" :: outs) tl
   | "nsucc" :: tl -> k T.OK ("nsucc" :: outs) tl
+  | "npsucc" :: tl -> k T.OK ("npsucc" :: outs) tl
   | "ntri" :: tl -> k T.OK ("ntri" :: outs) tl
   | "niter" :: tl -> k T.OK ("niter" :: outs) tl
   | "plt" :: tl -> k T.OK ("plt" :: outs) tl
   | "ple" :: tl -> k T.OK ("ple" :: outs) tl
+  | "pplus" :: tl -> k T.OK ("pplus" :: outs) tl
+  | "ppred" :: tl -> k T.OK ("ppred" :: outs) tl
+  | "psucc" :: tl -> k T.OK ("psucc" :: outs) tl
   | _ -> k T.OO outs ins
 
 let main =
diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcpGroundArith.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcpGroundArith.ml
index 7005e5c20..dfefb2f54 100644
--- a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcpGroundArith.ml
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcpGroundArith.ml
@@ -4,6 +4,7 @@ module R = RecommPcsPar
 let step k st outs ins =
   if st <> T.OO then k st outs ins else
   match ins with
+  | "(decidability)" :: tl -> k T.OK ("(decidability)" :: outs) tl
   | "(semigroup" :: "properties)" :: tl -> k T.OK ("properties)" :: "(semigroup" :: outs) tl
   | _ -> k T.OO outs ins
 
diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundArith.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundArith.ml
index 136681a29..03f6c1ed0 100644
--- a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundArith.ml
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundArith.ml
@@ -11,6 +11,7 @@ let step k st outs ins =
   | "LEFT" :: "SUBTRACTION" :: tl -> k T.OK ("SUBTRACTION" :: "LEFT" :: outs) tl
   | "SUBTRACTION" :: tl -> k T.OK ("SUBTRACTION" :: outs) tl
   | "ADDITION" :: tl -> k T.OK ("ADDITION" :: outs) tl
+  | "RIGHT" :: "ADDITION" :: tl -> k T.OK ("ADDITION" :: "RIGHT" :: outs) tl
   | "PREDECESSOR" :: tl -> k T.OK ("PREDECESSOR" :: outs) tl
   | "SUCCESSOR" :: tl -> k T.OK ("SUCCESSOR" :: outs) tl
   | "NAT-INJECTION" :: tl -> k T.OK ("NAT-INJECTION" :: outs) tl
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_plus_rplus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_plus_rplus.ma
index e80e2414f..b799fc15d 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_plus_rplus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_plus_rplus.ma
@@ -17,7 +17,7 @@ include "ground/arith/nat_plus.ma".
 
 (* ADDITION FOR NON-NEGATIVE INTEGERS ***************************************)
 
-(* Constructions with rplus *************************************************)
+(* Constructions with nrplus ************************************************)
 
 lemma nrplus_inj_sn (p) (n):
       ninj (p + n) = ninj p + n.
@@ -25,7 +25,7 @@ lemma nrplus_inj_sn (p) (n):
 #n #IH <nplus_succ_dx <IH //
 qed.
 
-(* Constructions with rplus and npsucc **************************************)
+(* Constructions with nrplus and npsucc *************************************)
 
 lemma nrplus_npsucc_sn (m) (n):
       npsucc (m + n) = npsucc m + n.
diff --git a/matita/matita/contribs/lambdadelta/ground/lib/stream_tls_eq.ma b/matita/matita/contribs/lambdadelta/ground/lib/stream_tls_eq.ma
index ee230d2b6..0f65086e5 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/stream_tls_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/stream_tls_eq.ma
@@ -17,7 +17,7 @@ include "ground/lib/stream_tls.ma".
 
 (* ITERATED TAIL FOR STREAMS ************************************************)
 
-(* Properties with stream_eq *)
+(* Constructions with stream_eq *********************************************)
 
 lemma stream_tls_eq_repl (A) (n):
       stream_eq_repl A (λt1,t2. ⫰*[n] t1 ≗ ⫰*[n] t2).
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_append.ma b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_append.ma
index 184540728..c2d7b9ed7 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_append.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_append.ma
@@ -15,7 +15,7 @@
 include "ground/notation/functions/append_2.ma".
 include "ground/relocation/fr2_map.ma".
 
-(* APPEND FOR FINITE RELOCATION MAPS WITH PAIRS *******************************************)
+(* CONCATENATION FOR FINITE RELOCATION MAPS WITH PAIRS **********************)
 
 (* Note: this is compose *)
 (*** fr2_append *)
@@ -28,7 +28,7 @@ interpretation
   "append (finite relocation maps with pairs)" 
   'Append f1 f2 = (fr2_append f1 f2).
 
-(* Basic properties *********************************************************)
+(* Basic constructions ******************************************************)
 
 (*** mr2_append_nil *)
 lemma fr2_append_nil (f2):
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_minus.ma b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_minus.ma
index a97d13067..edc241fc0 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_minus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_minus.ma
@@ -19,7 +19,7 @@ include "ground/arith/nat_minus.ma".
 include "ground/arith/nat_lt.ma".
 include "ground/relocation/fr2_map.ma".
 
-(* RELATIONAL SUBTRACTION FOR FINITE RELOCATION MAPS WITH PAIRS *******************************************)
+(* RELATIONAL SUBTRACTION FOR FINITE RELOCATION MAPS WITH PAIRS *************)
 
 (*** minuss *)
 inductive fr2_minus: nat → relation fr2_map ≝
@@ -38,7 +38,7 @@ interpretation
   "minus (finite relocation maps with pairs)"
   'RMinus f1 i f2 = (fr2_minus i f1 f2).
 
-(* Basic inversion lemmas ***************************************************)
+(* Basic inversions *********************************************************)
 
 (*** minuss_inv_nil1 *)
 lemma fr2_minus_inv_nil_sn (f2) (i):
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat.ma b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat.ma
index d71dc8fb4..67fd827ad 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat.ma
@@ -17,7 +17,7 @@ include "ground/arith/nat_plus.ma".
 include "ground/arith/nat_lt.ma".
 include "ground/relocation/fr2_map.ma".
 
-(* NON-NEGATIVE APPLICATION FOR FINITE RELOCATION MAPS WITH PAIRS *******************************************)
+(* NON-NEGATIVE APPLICATION FOR FINITE RELOCATION MAPS WITH PAIRS ***********)
 
 (*** at *)
 inductive fr2_nat: fr2_map → relation nat ≝
@@ -36,7 +36,7 @@ interpretation
   "non-negative relational application (finite relocation maps with pairs)"
   'RAt l1 f l2 = (fr2_nat f l1 l2).
 
-(* Basic inversion lemmas ***************************************************)
+(* Basic inversions *********************************************************)
 
 (*** at_inv_nil *)
 lemma fr2_nat_inv_nil (l1) (l2):
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat_nat.ma b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat_nat.ma
index 1dd3cd9a6..a40ac35c1 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat_nat.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat_nat.ma
@@ -14,9 +14,9 @@
 
 include "ground/relocation/fr2_nat.ma".
 
-(* NON-NEGATIVE APPLICATION FOR FINITE RELOCATION MAPS WITH PAIRS *******************************************)
+(* NON-NEGATIVE APPLICATION FOR FINITE RELOCATION MAPS WITH PAIRS ***********)
 
-(* Main properties **********************************************************)
+(* Main constructions *******************************************************)
 
 (*** at_mono *)
 theorem fr2_nat_mono (f) (l):
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_plus.ma b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_plus.ma
index 0297be7bd..459560035 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_plus.ma
@@ -15,7 +15,7 @@
 include "ground/arith/nat_minus_plus.ma".
 include "ground/relocation/fr2_map.ma".
 
-(* ADDITION FOR FINITE RELOCATION MAPS WITH PAIRS ******************************)
+(* ADDITION FOR FINITE RELOCATION MAPS WITH PAIRS ***************************)
 
 (* Note: this is pushs *)
 (*** pluss *)
@@ -28,14 +28,14 @@ interpretation
   "plus (finite relocation maps with pairs)"
   'plus f n = (fr2_plus f n).
 
-(* Basic properties *********************************************************)
+(* Basic constructions ******************************************************)
 
 (*** pluss_SO2 *)
 lemma fr2_plus_cons_unit (d) (h) (f):
       ((❨d,h❩;f)+𝟏) = ❨↑d,h❩;f+𝟏.
 normalize // qed.
 
-(* Basic inversion lemmas ***************************************************)
+(* Basic inversions *********************************************************)
 
 (*** pluss_inv_nil2 *)
 lemma fr2_plus_inv_nil_dx (n) (f):
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after.ma
index 3dcc718bf..a5afa31e6 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after.ma
@@ -16,7 +16,7 @@ include "ground/notation/relations/rafter_3.ma".
 include "ground/xoa/ex_3_2.ma". 
 include "ground/relocation/gr_tl.ma".
 
-(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************)
 
 (*** after *)
 coinductive gr_after: relation3 gr_map gr_map gr_map ≝
@@ -35,7 +35,7 @@ interpretation
   "relational composition (generic relocation maps)"
   'RAfter f1 f2 f = (gr_after f1 f2 f).
 
-(* Basic inversion lemmas ***************************************************)
+(* Basic inversions *********************************************************)
 
 (*** after_inv_ppx *)
 lemma gr_after_inv_push_bi:
@@ -82,7 +82,7 @@ lemma gr_after_inv_next_sn:
 ]
 qed-.
 
-(* Advanced inversion lemmas ************************************************)
+(* Advanced inversions ******************************************************)
 
 (*** after_inv_ppp *)
 lemma gr_after_inv_push_bi_push:
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_after.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_after.ma
index 7ee5239b1..ad71eeac2 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_after.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_after.ma
@@ -14,9 +14,9 @@
 
 include "ground/relocation/gr_after_eq.ma".
 
-(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************)
 
-(* Main properties **********************************************************)
+(* Main constructions *******************************************************)
 
 (*** after_trans1 *)
 corec theorem gr_after_trans_sn:
@@ -70,7 +70,7 @@ corec theorem gr_after_trans_dx:
 ]
 qed-.
 
-(* Main inversion lemmas ****************************************************)
+(* Main inversions **********************************************************)
 
 (*** after_mono *)
 corec theorem gr_after_mono:
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_after_ist.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_after_ist.ma
index a3c13ff76..c8051078a 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_after_ist.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_after_ist.ma
@@ -17,14 +17,14 @@ include "ground/relocation/gr_pat_tls.ma".
 include "ground/relocation/gr_ist_tls.ma".
 include "ground/relocation/gr_after_pat_tls.ma".
 
-(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************)
 
 (*** H_after_inj *)
 definition H_gr_after_inj: predicate gr_map ≝
            λf1. 𝐓❪f1❫ →
            ∀f,f21,f22. f1 ⊚ f21 ≘ f → f1 ⊚ f22 ≘ f → f21 ≡ f22.
 
-(* Main forward lemmas on istot **************************************************)
+(* Main destructions with gr_ist ********************************************)
 
 (*** after_inj_O_aux *)
 corec fact gr_after_inj_unit_aux:
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_basic.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_basic.ma
index fa15b0d5a..00c0672c8 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_basic.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_basic.ma
@@ -16,9 +16,9 @@ include "ground/arith/nat_le_pred.ma".
 include "ground/relocation/gr_basic.ma".
 include "ground/relocation/gr_after_uni.ma".
 
-(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************)
 
-(* Properties with gr_basic **********************************************)
+(* Constructions with gr_basic **********************************************)
 
 (*** after_basic_rc *)
 lemma after_basic_rc (d2) (d1):
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_eq.ma
index 71ed20657..095c4adbb 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_eq.ma
@@ -15,9 +15,9 @@
 include "ground/relocation/gr_tl_eq.ma".
 include "ground/relocation/gr_after.ma".
 
-(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************)
 
-(* Properties with gr_eq *)
+(* Constructions with gr_eq *************************************************)
 
 (*** after_eq_repl_back2 *)
 corec lemma gr_after_eq_repl_back_sn:
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_isi.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_isi.ma
index fbe70c17f..189c67562 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_isi.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_isi.ma
@@ -15,9 +15,9 @@
 include "ground/relocation/gr_isi.ma".
 include "ground/relocation/gr_after_after.ma".
 
-(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************)
 
-(* Properties on isid *******************************************************)
+(* Constructions with gr_isi ************************************************)
 
 (*** after_isid_sn *)
 corec lemma gr_after_isi_sn:
@@ -37,7 +37,7 @@ corec lemma gr_after_isi_dx:
 ]
 qed.
 
-(* Destructions on isid *************************************************)
+(* Destructions with gr_isi *************************************************)
 
 (*** after_isid_inv_sn *)
 lemma gr_after_isi_inv_sn:
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_ist.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_ist.ma
index 97780f1c6..466df35ed 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_ist.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_ist.ma
@@ -16,9 +16,9 @@ include "ground/relocation/gr_pat_lt.ma".
 include "ground/relocation/gr_ist.ma".
 include "ground/relocation/gr_after_pat.ma".
 
-(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************)
 
-(* Forward lemmas on istot **************************************************)
+(* Destructions with gr_ist *************************************************)
 
 (*** after_istot_fwd *)
 lemma gr_after_ist_des:
@@ -52,7 +52,7 @@ lemma gr_after_des_ist_pat:
 /3 width=8 by gr_after_des_pat, ex2_intro/
 qed-.
 
-(* Inversions with gr_ist *)
+(* Inversions with gr_ist ***************************************************)
 
 (*** after_inv_istot *)
 lemma gr_after_inv_ist:
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_ist_isi.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_ist_isi.ma
index fd325b4d7..9a08ba373 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_ist_isi.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_ist_isi.ma
@@ -15,9 +15,9 @@
 include "ground/relocation/gr_ist_isi.ma".
 include "ground/relocation/gr_after_ist.ma".
 
-(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************)
 
-(* Forward lemmas on istot and isid **************************************************)
+(* Destructions with gr_ist and gr_isi **************************************)
 
 (*** after_fwd_isid_sn *)
 lemma gr_after_des_ist_eq_sn:
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_isu.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_isu.ma
index 0707a3d76..f1c8df12f 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_isu.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_isu.ma
@@ -15,9 +15,9 @@
 include "ground/relocation/gr_isu_uni.ma".
 include "ground/relocation/gr_after_uni.ma".
 
-(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************)
 
-(* Properties on isuni ******************************************************)
+(* Constructions with gr_isu ************************************************)
 
 (*** after_isid_isuni *)
 lemma gr_after_isu_isi_next:
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_nat_uni_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_nat_uni_tls.ma
index 04be0911d..cef9bd7e4 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_nat_uni_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_nat_uni_tls.ma
@@ -17,9 +17,9 @@ include "ground/relocation/gr_nat.ma".
 include "ground/relocation/gr_isi_uni.ma".
 include "ground/relocation/gr_after_isi.ma".
 
-(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************)
 
-(* Properties with gr_nat and uni *)
+(* Constructions with gr_nat and gr_uni *************************************)
 
 (*** after_uni_dx *)
 lemma gr_after_nat_uni (l2) (l1):
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_pat.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_pat.ma
index aa63c415e..2892b20d9 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_pat.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_pat.ma
@@ -15,9 +15,9 @@
 include "ground/relocation/gr_pat_pat.ma".
 include "ground/relocation/gr_after.ma".
 
-(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************)
 
-(* Forward lemmas on pat *****************************************************)
+(* Destructions with gr_pat *************************************************)
 
 (*** after_at_fwd *)
 lemma gr_after_pat_des (i) (i1):
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_pat_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_pat_tls.ma
index 4968977cf..b7b5fc7fb 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_pat_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_pat_tls.ma
@@ -16,9 +16,9 @@ include "ground/relocation/gr_tls.ma".
 include "ground/relocation/gr_pat.ma".
 include "ground/relocation/gr_after.ma".
 
-(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************)
 
-(* Properties on pat and tls ********************************************************)
+(* Constructions with gr_pat and gr_tls *************************************)
 
 (* Note: this requires ↑ on first n *)
 (*** after_tls *)
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_pat_uni_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_pat_uni_tls.ma
index e8104fd3e..40853b262 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_pat_uni_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_pat_uni_tls.ma
@@ -14,13 +14,13 @@
 
 include "ground/relocation/gr_tls.ma".
 include "ground/relocation/gr_pat.ma".
-(**) (* it should not depend on gr_isi *)
+(* * it should not depend on gr_isi *)
 include "ground/relocation/gr_isi_uni.ma".
 include "ground/relocation/gr_after_isi.ma".
 
-(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************)
 
-(* Properties with pat and uni and tls *******************************************************)
+(* Constructions with gr_pat and gr_uni and gr_tls **************************)
 
 (*** after_uni_succ_dx *)
 lemma gr_after_pat_uni (i2) (i1):
@@ -63,7 +63,7 @@ lemma gr_pat_after_uni_tls (i2) (i1):
 ]
 qed-.
 
-(* Advanced properties with uni *)
+(* Advanced constructions with gr_uni ***************************************)
 
 (*** after_uni_one_dx *)
 lemma gr_after_push_unit:
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_uni.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_uni.ma
index 254c99857..41f35ee39 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_uni.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_uni.ma
@@ -13,13 +13,13 @@
 (**************************************************************************)
 
 include "ground/arith/nat_plus.ma".
-(**) (* it should not depend on gr_isi *)
+(* * it should not depend on gr_isi *)
 include "ground/relocation/gr_isi_uni.ma".
 include "ground/relocation/gr_after_isi.ma".
 
-(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************)
 
-(* Properties on uni ********************************************************)
+(* Constructions with gr_uni ************************************************)
 
 (*** after_uni *)
 lemma gr_after_uni (h1) (h2): 𝐮❨h1❩ ⊚ 𝐮❨h2❩ ≘ 𝐮❨h2+h1❩.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_basic.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_basic.ma
index 75230b5fd..50f6e2770 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_basic.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_basic.ma
@@ -16,7 +16,7 @@ include "ground/notation/functions/element_b_2.ma".
 include "ground/relocation/gr_pushs.ma".
 include "ground/relocation/gr_uni.ma".
 
-(* BASIC ELEMENTS FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* BASIC ELEMENTS FOR GENERIC RELOCATION MAPS *******************************)
 
 definition basic (d) (h): gr_map ≝ ⫯*[d] 𝐮❨h❩.
 
@@ -24,7 +24,7 @@ interpretation
   "basic elements (generic relocation maps)"
   'ElementB d h = (basic d h).
 
-(* Basic properties *********************************************************)
+(* Basic constructions ******************************************************)
 
 (*** at_basic_succ_sn *)
 lemma gr_basic_succ_sn (d) (h): ⫯𝐛❨d,h❩ = 𝐛❨↑d,h❩.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter.ma
index 8c730547f..bbac0036c 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter.ma
@@ -16,7 +16,7 @@ include "ground/notation/relations/rcoafter_3.ma".
 include "ground/xoa/ex_3_2.ma".
 include "ground/relocation/gr_tl.ma".
 
-(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ********************)
 
 (*** coafter *)
 coinductive gr_coafter: relation3 gr_map gr_map gr_map ≝
@@ -35,7 +35,7 @@ interpretation
   "relational co-composition (generic relocation maps)"
   'RCoAfter f1 f2 f = (gr_coafter f1 f2 f).
 
-(* Basic inversion lemmas ***************************************************)
+(* Basic inversions *********************************************************)
 
 (*** coafter_inv_ppx *)
 lemma gr_coafter_inv_push_bi:
@@ -82,7 +82,7 @@ lemma gr_coafter_inv_next_sn:
 ]
 qed-.
 
-(* Advanced inversion lemmas ************************************************)
+(* Advanced inversions ******************************************************)
 
 (*** coafter_inv_ppp *)
 lemma gr_coafter_inv_push_bi_push:
@@ -213,7 +213,7 @@ elim (gr_map_split_tl g2) #H2
 ]
 qed-.
 
-(* Inversion lemmas with tail ***********************************************)
+(* Inversions with gr_tl ****************************************************)
 
 (*** coafter_inv_tl1 *)
 lemma gr_coafter_inv_tl_dx:
@@ -222,7 +222,7 @@ lemma gr_coafter_inv_tl_dx:
 #g2 #g1 #g
 elim (gr_map_split_tl g1) #H1 #H2
 [ /3 width=7 by gr_coafter_refl, ex2_intro/
-| @(ex2_intro … (↑g)) /2 width=7 by gr_coafter_push/ (**) (* full auto fails *)
+| @(ex2_intro … (↑g)) /2 width=7 by gr_coafter_push/ (* * full auto fails *)
 ]
 qed-.
 
@@ -233,6 +233,6 @@ lemma gr_coafter_inv_tl:
 #g2 #g1 #g
 elim (gr_map_split_tl g) #H1 #H2
 [ /3 width=7 by gr_coafter_refl, ex2_intro/
-| @(ex2_intro … (↑g1)) /2 width=7 by gr_coafter_push/ (**) (* full auto fails *)
+| @(ex2_intro … (↑g1)) /2 width=7 by gr_coafter_push/ (* * full auto fails *)
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_coafter.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_coafter.ma
index 7bbc18f19..6fd545fc5 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_coafter.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_coafter.ma
@@ -14,9 +14,9 @@
 
 include "ground/relocation/gr_coafter_eq.ma".
 
-(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ********************)
 
-(* Main inversion lemmas ****************************************************)
+(* Main inversions **********************************************************)
 
 (*** coafter_mono *)
 corec theorem gr_coafter_mono:
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_coafter_ist.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_coafter_ist.ma
index 7161e78f0..f1e633463 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_coafter_ist.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_coafter_ist.ma
@@ -16,14 +16,14 @@ include "ground/relocation/gr_pat_tls.ma".
 include "ground/relocation/gr_ist_tls.ma".
 include "ground/relocation/gr_coafter_nat_tls.ma".
 
-(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ********************)
 
 (*** H_coafter_inj *)
 definition H_gr_coafter_inj: predicate gr_map ≝
            λf1. 𝐓❪f1❫ →
            ∀f,f21,f22. f1 ~⊚ f21 ≘ f → f1 ~⊚ f22 ≘ f → f21 ≡ f22.
 
-(* Main Forward lemmas with istot ************************************************)
+(* Main destructions with gr_ist ********************************************)
 
 (*** coafter_inj_O_aux *)
 corec fact gr_coafter_inj_unit_aux:
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_eq.ma
index bf0e47d4d..3d0b3c440 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_eq.ma
@@ -15,9 +15,9 @@
 include "ground/relocation/gr_tl_eq.ma".
 include "ground/relocation/gr_coafter.ma".
 
-(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ********************)
 
-(* Properties with gr_eq *)
+(* Constructions with gr_eq *************************************************)
 
 (*** coafter_eq_repl_back2 *)
 corec lemma gr_coafter_eq_repl_back_sn:
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_isi.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_isi.ma
index 94b080c5c..0464b905c 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_isi.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_isi.ma
@@ -15,9 +15,9 @@
 include "ground/relocation/gr_isi_id.ma".
 include "ground/relocation/gr_coafter_coafter.ma".
 
-(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ********************)
 
-(* Properties with test for identity ****************************************)
+(* Constructions with gr_isi ************************************************)
 
 (*** coafter_isid_sn *)
 corec lemma gr_coafter_isi_sn:
@@ -37,7 +37,7 @@ cases (gr_map_split_tl f1) #H1
 ]
 qed.
 
-(* Inversion lemmas with test for identity **********************************)
+(* Inversions with gr_isi ***************************************************)
 
 (*** coafter_isid_inv_sn *)
 lemma gr_coafter_isi_inv_sn:
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_ist_isf.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_ist_isf.ma
index ebd461dcf..20d861a48 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_ist_isf.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_ist_isf.ma
@@ -18,13 +18,13 @@ include "ground/relocation/gr_ist_tls.ma".
 include "ground/relocation/gr_coafter_nat_tls.ma".
 include "ground/relocation/gr_coafter_isi.ma".
 
-(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ********************)
 
 (*** H_coafter_isfin2_fwd *)
 definition H_gr_coafter_des_ist_isf: predicate gr_map ≝
            λf1. ∀f2. 𝐅❪f2❫ → 𝐓❪f1❫ → ∀f. f1 ~⊚ f2 ≘ f →  𝐅❪f❫.
 
-(* Forward lemmas with ist and isf *)
+(* Destructions with gr_ist and gr_isf **************************************)
 
 (*** coafter_isfin2_fwd_O_aux *)
 fact gr_coafter_des_ist_isf_unit_aux:
@@ -51,7 +51,7 @@ fact gr_coafter_des_ist_isf_aux:
 elim (gr_pat_inv_unit_succ … H1f1) -H1f1 [ |*: // ] #g1 #Hg1 #H1
 elim (gr_coafter_inv_next_sn … Hf … H1) -Hf #g #Hg #H0
 lapply (IH … Hg1 … Hg) -i2 -Hg
-/2 width=4 by gr_ist_inv_next, gr_isf_push/ (**) (* full auto fails *)
+/2 width=4 by gr_ist_inv_next, gr_isf_push/ (* * full auto fails *)
 qed-.
 
 (*** coafter_isfin2_fwd *)
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_ist_isi.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_ist_isi.ma
index 871158d80..a73cfa216 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_ist_isi.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_ist_isi.ma
@@ -17,13 +17,13 @@ include "ground/relocation/gr_isi_tls.ma".
 include "ground/relocation/gr_ist_tls.ma".
 include "ground/relocation/gr_coafter_nat_tls.ma".
 
-(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ********************)
 
 (*** H_coafter_fwd_isid2 *)
 definition H_gr_coafter_des_ist_sn_isi: predicate gr_map ≝
            λf1. ∀f2,f. f1 ~⊚ f2 ≘ f → 𝐓❪f1❫ → 𝐈❪f❫ → 𝐈❪f2❫.
 
-(* Forward lemmas with ist and isi *)
+(* Destructions with gr_ist and gr_isi **************************************)
 
 (*** coafter_fwd_isid2_O_aux *)
 corec fact gr_coafter_des_ist_sn_isi_unit_aux:
@@ -48,7 +48,7 @@ fact gr_coafter_des_ist_sn_isi_aux:
 #i2 #IH #f1 #H1f1 #f2 #f #H #H2f1 #Hf
 elim (gr_pat_inv_unit_succ … H1f1) -H1f1 [ |*: // ] #g1 #Hg1 #H1
 elim (gr_coafter_inv_next_sn … H … H1) -H #g #Hg #H0
-@(IH … Hg1 … Hg) /2 width=3 by gr_ist_inv_next, gr_isi_inv_push/ (**) (* full auto fails *)
+@(IH … Hg1 … Hg) /2 width=3 by gr_ist_inv_next, gr_isi_inv_push/ (* * full auto fails *)
 qed-.
 
 (*** coafter_fwd_isid2 *)
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_isu.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_isu.ma
index e74ed1854..8c94f6a70 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_isu.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_isu.ma
@@ -16,9 +16,9 @@ include "ground/relocation/gr_isi_pushs.ma".
 include "ground/relocation/gr_isu_uni.ma".
 include "ground/relocation/gr_coafter_uni_pushs.ma".
 
-(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ********************)
 
-(* Properties with test for uniform relocations and isi *****************************)
+(* Constructions with gr_isu and gr_isi *************************************)
 
 (*** coafter_isuni_isid *)
 lemma gr_coafter_isu_isi:
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_nat_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_nat_tls.ma
index f297468f9..6d953f203 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_nat_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_nat_tls.ma
@@ -16,9 +16,9 @@ include "ground/relocation/gr_tls.ma".
 include "ground/relocation/gr_nat.ma".
 include "ground/relocation/gr_coafter.ma".
 
-(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ********************)
 
-(* Properties with nat and iterated tail ********************************************)
+(* Constructions with gr_nat and gr_tls *************************************)
 
 (*** coafter_tls *)
 lemma gr_coafter_tls_bi_tls (n2) (n1):
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_nat_tls_pushs.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_nat_tls_pushs.ma
index cc5d28489..524e1d881 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_nat_tls_pushs.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_nat_tls_pushs.ma
@@ -17,9 +17,9 @@ include "ground/relocation/gr_tls.ma".
 include "ground/relocation/gr_nat.ma".
 include "ground/relocation/gr_coafter.ma".
 
-(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ********************)
 
-(* Forward lemmas with nat and iterated tail and pushs ************************************************)
+(* Destructions with gr_nat and gr_tls and gr_pushs *************************)
 
 (*** coafter_fwd_pushs *)
 lemma gr_coafter_des_pushs_dx (n) (m):
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_pat_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_pat_tls.ma
index 13f801e1c..a2c00145b 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_pat_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_pat_tls.ma
@@ -15,9 +15,9 @@
 include "ground/relocation/gr_pat_tls.ma".
 include "ground/relocation/gr_coafter_nat_tls.ma".
 
-(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ********************)
 
-(* Properties with pat and iterated tail ********************************************)
+(* Constructions with gr_pat and gr_tls *************************************)
 
 (* Note: this does not require ↑ first and second j *)
 (*** coafter_tls_succ *)
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_uni_pushs.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_uni_pushs.ma
index f0f401095..9c903a6b3 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_uni_pushs.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_uni_pushs.ma
@@ -14,12 +14,12 @@
 
 include "ground/relocation/gr_pushs.ma".
 include "ground/relocation/gr_uni.ma".
-(**) (* it should not depend on gr_isi *)
+(* * it should not depend on gr_isi *)
 include "ground/relocation/gr_coafter_isi.ma".
 
-(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ********************)
 
-(* Properties with uniform relocations and pushs **************************************)
+(* Constructions with gr_uni and gr_pushs ***********************************)
 
 (*** coafter_uni_sn *)
 lemma gr_coafter_uni_sn_pushs (n):
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_eq.ma
index d908f7033..c5d58eaf6 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_eq.ma
@@ -45,7 +45,7 @@ definition gr_eq_repl_back (R:predicate …) ≝
 definition gr_eq_repl_fwd (R:predicate …) ≝
            ∀f1. R f1 → ∀f2. f2 ≡ f1 → R f2.
 
-(* Basic properties *********************************************************)
+(* Basic constructions ******************************************************)
 
 (*** eq_sym *)
 corec lemma gr_eq_sym: symmetric … gr_eq.
@@ -59,7 +59,7 @@ lemma gr_eq_repl_sym (R):
       gr_eq_repl_back R → gr_eq_repl_fwd R.
 /3 width=3 by gr_eq_sym/ qed-.
 
-(* Alternative definition with stream_eq (specific) ***************************************************)
+(* Alternative definition with stream_eq (specific) *************************)
 
 alias symbol "subseteq" (instance 1) = "relation inclusion".
 
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_fcla.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_fcla.ma
index 8a533cbe1..5ab8b1dec 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_fcla.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_fcla.ma
@@ -16,7 +16,7 @@ include "ground/notation/relations/rfun_c_2.ma".
 include "ground/arith/nat_succ.ma".
 include "ground/relocation/gr_isi.ma".
 
-(* FINITE COLENGTH ASSIGNMENT FOR GENERIC RELOCATION MAPS  ***********************************************************)
+(* FINITE COLENGTH ASSIGNMENT FOR GENERIC RELOCATION MAPS *******************)
 
 (*** fcla *)
 inductive gr_fcla: relation2 gr_map nat ≝
@@ -32,7 +32,7 @@ interpretation
   "finite colength assignment (generic relocation maps)"
   'RFunC f n = (gr_fcla f n).
 
-(* Basic inversion lemmas ***************************************************)
+(* Basic inversions *********************************************************)
 
 (*** fcla_inv_px *)
 lemma gr_fcla_inv_push (g) (m): 𝐂❪g❫ ≘ m → ∀f. ⫯f = g → 𝐂❪f❫ ≘ m.
@@ -54,7 +54,7 @@ lemma gr_fcla_inv_next (g) (m): 𝐂❪g❫ ≘ m → ∀f. ↑f = g → ∃∃n
 ]
 qed-.
 
-(* Advanced inversion lemmas ************************************************)
+(* Advanced inversions ******************************************************)
 
 (*** cla_inv_nn *)
 lemma gr_cla_inv_next_succ (g) (m): 𝐂❪g❫ ≘ m → ∀f,n. ↑f = g → ↑n = m → 𝐂❪f❫ ≘ n.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_fcla_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_fcla_eq.ma
index 59013d57a..3e8a9c9dd 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_fcla_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_fcla_eq.ma
@@ -15,9 +15,9 @@
 include "ground/relocation/gr_isi_eq.ma".
 include "ground/relocation/gr_fcla.ma".
 
-(* FINITE COLENGTH ASSIGNMENT FOR GENERIC RELOCATION MAPS  ***********************************************************)
+(* FINITE COLENGTH ASSIGNMENT FOR GENERIC RELOCATION MAPS *******************)
 
-(* Properties with gr_eq *********************************************************)
+(* Constructions with gr_eq *************************************************)
 
 (*** fcla_eq_repl_back *)
 lemma gr_fcla_eq_repl_back (n):
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_fcla_fcla.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_fcla_fcla.ma
index fe6098108..34c640e3e 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_fcla_fcla.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_fcla_fcla.ma
@@ -14,9 +14,9 @@
 
 include "ground/relocation/gr_fcla.ma".
 
-(* FINITE COLENGTH ASSIGNMENT FOR GENERIC RELOCATION MAPS  ***********************************************************)
+(* FINITE COLENGTH ASSIGNMENT FOR GENERIC RELOCATION MAPS *******************)
 
-(* Main forward lemmas ******************************************************)
+(* Main destructions ********************************************************)
 
 (*** fcla_mono *)
 theorem gr_fcla_mono (f):
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_fcla_uni.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_fcla_uni.ma
index bbae04602..8bd26d8ed 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_fcla_uni.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_fcla_uni.ma
@@ -15,9 +15,9 @@
 include "ground/relocation/gr_isi_uni.ma".
 include "ground/relocation/gr_fcla.ma".
 
-(* FINITE COLENGTH ASSIGNMENT FOR GENERIC RELOCATION MAPS  ***********************************************************)
+(* FINITE COLENGTH ASSIGNMENT FOR GENERIC RELOCATION MAPS *******************)
 
-(* Properties with gr_uni ***************************)
+(* Constructions with gr_uni ************************************************)
 
 (*** fcla_uni *)
 lemma gr_fcla_uni (n): 𝐂❪𝐮❨n❩❫ ≘ n.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_id.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_id.ma
index 783215f49..e292db157 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_id.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_id.ma
@@ -15,7 +15,7 @@
 include "ground/notation/functions/element_i_0.ma".
 include "ground/relocation/gr_map.ma".
 
-(* IDENTITY ELEMENT FOR GENERIC RELOCATION MAPS  ******************************************************)
+(* IDENTITY ELEMENT FOR GENERIC RELOCATION MAPS *****************************)
 
 (*** id *)
 corec definition gr_id: gr_map ≝ ⫯gr_id.
@@ -24,7 +24,7 @@ interpretation
   "identity element (generic relocation streams)"
   'ElementI = (gr_id).
 
-(* Basic properties (specific) *********************************************************)
+(* Basic constructions (specific) *******************************************)
 
 (*** id_rew *)
 lemma gr_id_unfold: ⫯𝐢 = 𝐢.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_id_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_id_eq.ma
index 00a4d3691..f79aa988c 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_id_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_id_eq.ma
@@ -15,9 +15,9 @@
 include "ground/relocation/gr_tl_eq.ma".
 include "ground/relocation/gr_id.ma".
 
-(* IDENTITY ELEMENT FOR GENERIC RELOCATION MAPS  ******************************************************)
+(* IDENTITY ELEMENT FOR GENERIC RELOCATION MAPS *****************************)
 
-(* Properties with gr_eq *)
+(* Constructions with gr_eq *************************************************)
 
 corec lemma gr_id_eq (f): ⫯f ≡ f → 𝐢 ≡ f.
 cases gr_id_unfold #Hf
@@ -27,7 +27,7 @@ cases H in Hf; -H #Hf
 /3 width=5 by gr_eq_inv_push_bi/
 qed.
 
-(* Inversions with gr_eq *)
+(* Inversions with gr_eq ****************************************************)
 
 (* Note: this has the same proof of the previous *)
 corec lemma gr_id_inv_eq (f): 𝐢 ≡ f → ⫯f ≡ f.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isd.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isd.ma
index aa5404adb..7ebdf864a 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isd.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isd.ma
@@ -15,7 +15,7 @@
 include "ground/notation/relations/predicate_omega_1.ma".
 include "ground/relocation/gr_map.ma".
 
-(* DIVERGENCE CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* DIVERGENCE CONDITION FOR GENERIC RELOCATION MAPS *************************)
 
 (*** isdiv *)
 coinductive gr_isd: predicate gr_map ≝
@@ -28,7 +28,7 @@ interpretation
   "divergence condition (generic relocation maps)"
   'PredicateOmega f = (gr_isd f).
 
-(* Basic inversion lemmas ***************************************************)
+(* Basic inversions *********************************************************)
 
 (*** isdiv_inv_gen *)
 lemma gr_isd_inv_gen (g): 𝛀❪g❫ → ∃∃f. 𝛀❪f❫ & ↑f = g.
@@ -36,7 +36,7 @@ lemma gr_isd_inv_gen (g): 𝛀❪g❫ → ∃∃f. 𝛀❪f❫ & ↑f = g.
 #f #g #Hf * /2 width=3 by ex2_intro/
 qed-.
 
-(* Advanced inversion lemmas ************************************************)
+(* Advanced inversions ******************************************************)
 
 (*** isdiv_inv_next *)
 lemma gr_isd_inv_next (g): 𝛀❪g❫ → ∀f. ↑f = g → 𝛀❪f❫.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isd_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isd_eq.ma
index 9aeb37fce..37b1e3542 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isd_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isd_eq.ma
@@ -15,9 +15,9 @@
 include "ground/relocation/gr_tl_eq_eq.ma".
 include "ground/relocation/gr_isd.ma".
 
-(* DIVERGENCE CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* DIVERGENCE CONDITION FOR GENERIC RELOCATION MAPS *************************)
 
-(* Properties with gr_eq *********************************************************)
+(* Constructions with gr_eq *************************************************)
 
 (*** isdiv_eq_repl_back *)
 corec lemma gr_isd_eq_repl_back:
@@ -32,7 +32,7 @@ lemma gr_isd_eq_repl_fwd:
       gr_eq_repl_fwd … gr_isd.
 /3 width=3 by gr_isd_eq_repl_back, gr_eq_repl_sym/ qed-.
 
-(* Main inversion lemmas with gr_eq ***************)
+(* Main inversions with gr_eq ***********************************************)
 
 (*** isdiv_inv_eq_repl *)
 corec theorem gr_isd_inv_eq_repl (g1) (g2): 𝛀❪g1❫ → 𝛀❪g2❫ → g1 ≡ g2.
@@ -42,7 +42,7 @@ cases (gr_isd_inv_gen … H2) -H2
 /3 width=5 by gr_eq_next/
 qed-.
 
-(* Alternative definition with gr_eq ***************************************************)
+(* Alternative definition with gr_eq ****************************************)
 
 (*** eq_next_isdiv *)
 corec lemma gr_eq_next_isd (f): ↑f ≡ f → 𝛀❪f❫.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isd_nexts.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isd_nexts.ma
index 71c39b335..99a7cf37d 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isd_nexts.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isd_nexts.ma
@@ -15,16 +15,16 @@
 include "ground/relocation/gr_nexts.ma".
 include "ground/relocation/gr_isd.ma".
 
-(* DIVERGENCE CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* DIVERGENCE CONDITION FOR GENERIC RELOCATION MAPS *************************)
 
-(* Properties with iterated next ********************************************)
+(* Constructions with gr_nexts **********************************************)
 
 (*** isdiv_nexts *)
 lemma gr_isd_nexts (n) (f): 𝛀❪f❫ → 𝛀❪↑*[n]f❫.
 #n @(nat_ind_succ … n) -n /3 width=3 by gr_isd_next/
 qed.
 
-(* Inversion lemmas with iterated next **************************************)
+(* Inversions with gr_nexts *************************************************)
 
 (*** isdiv_inv_nexts *)
 lemma gr_isd_inv_nexts (n) (g): 𝛀❪↑*[n]g❫ → 𝛀❪g❫.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isd_tl.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isd_tl.ma
index cd5cc230e..05a3505e1 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isd_tl.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isd_tl.ma
@@ -15,9 +15,9 @@
 include "ground/relocation/gr_tl.ma".
 include "ground/relocation/gr_isd.ma".
 
-(* DIVERGENCE CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* DIVERGENCE CONDITION FOR GENERIC RELOCATION MAPS *************************)
 
-(* Properties with tail *****************************************************)
+(* Constructions with gr_tl *************************************************)
 
 (*** isdiv_tl *)
 lemma gr_isd_tl (f): 𝛀❪f❫ → 𝛀❪⫱f❫.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isd_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isd_tls.ma
index 71375b463..3bea6fb18 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isd_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isd_tls.ma
@@ -15,9 +15,9 @@
 include "ground/relocation/gr_tls.ma".
 include "ground/relocation/gr_isd_tl.ma".
 
-(* DIVERGENCE CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* DIVERGENCE CONDITION FOR GENERIC RELOCATION MAPS *************************)
 
-(* Properties with iterated tail ********************************************)
+(* Constructions with gr_tls ************************************************)
 
 (*** isdiv_tls *)
 lemma gr_isd_tls (n) (g): 𝛀❪g❫ → 𝛀❪⫱*[n]g❫.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isf.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isf.ma
index 4a5c13534..23292e2f1 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isf.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isf.ma
@@ -15,7 +15,7 @@
 include "ground/notation/relations/predicate_f_1.ma".
 include "ground/relocation/gr_fcla.ma".
 
-(* FINITE COLENGTH CONDITION FOR GENERIC RELOCATION MAPS *)
+(* FINITE COLENGTH CONDITION FOR GENERIC RELOCATION MAPS ********************)
 
 (*** isfin *)
 definition gr_isf: predicate gr_map ≝
@@ -25,7 +25,7 @@ interpretation
   "finite colength condition (generic relocation maps)"
   'PredicateF f = (gr_isf f).
 
-(* Basic eliminators ********************************************************)
+(* Basic eliminations *******************************************************)
 
 (*** isfin_ind *)
 lemma gr_isf_ind (Q:predicate …):
@@ -37,7 +37,7 @@ lemma gr_isf_ind (Q:predicate …):
 #n #H elim H -f -n /3 width=2 by ex_intro/
 qed-.
 
-(* Basic inversion lemmas ***************************************************)
+(* Basic inversions *********************************************************)
 
 (*** isfin_inv_push *)
 lemma gr_isf_inv_push (g): 𝐅❪g❫ → ∀f. ⫯f = g → 𝐅❪f❫.
@@ -50,7 +50,7 @@ lemma gr_isf_inv_next (g): 𝐅❪g❫ → ∀f. ↑f = g → 𝐅❪f❫.
 /2 width=2 by ex_intro/
 qed-.
 
-(* Basic properties *********************************************************)
+(* Basic constructions ******************************************************)
 
 (*** isfin_isid *)
 lemma gr_isf_isi (f): 𝐈❪f❫ → 𝐅❪f❫.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isf_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isf_eq.ma
index 123c59bd3..7b70b7828 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isf_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isf_eq.ma
@@ -15,9 +15,9 @@
 include "ground/relocation/gr_fcla_eq.ma".
 include "ground/relocation/gr_isf.ma".
 
-(* FINITE COLENGTH CONDITION FOR GENERIC RELOCATION MAPS *)
+(* FINITE COLENGTH CONDITION FOR GENERIC RELOCATION MAPS ********************)
 
-(* Properties with gr_eq *)
+(* Constructions with gr_eq *************************************************)
 
 (*** isfin_eq_repl_back *)
 lemma gr_isf_eq_repl_back:
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isf_isu.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isf_isu.ma
index 29a14f8b5..ab1c16f11 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isf_isu.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isf_isu.ma
@@ -15,9 +15,9 @@
 include "ground/relocation/gr_isu.ma".
 include "ground/relocation/gr_isf.ma".
 
-(* FINITE COLENGTH CONDITION FOR GENERIC RELOCATION MAPS *)
+(* FINITE COLENGTH CONDITION FOR GENERIC RELOCATION MAPS ********************)
 
-(* Properties with gr_isu *)
+(* Constructions with gr_isu ************************************************)
 
 (*** isuni_fwd_isfin *)
 lemma gr_isf_isu (f): 𝐔❪f❫ → 𝐅❪f❫.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isf_pushs.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isf_pushs.ma
index 014d0b3a5..4e8e1d2b1 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isf_pushs.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isf_pushs.ma
@@ -15,16 +15,16 @@
 include "ground/relocation/gr_pushs.ma".
 include "ground/relocation/gr_isf.ma".
 
-(* FINITE COLENGTH CONDITION FOR GENERIC RELOCATION MAPS *)
+(* FINITE COLENGTH CONDITION FOR GENERIC RELOCATION MAPS ********************)
 
-(* Properties with iterated push ********************************************)
+(* Constructions with gr_pushs **********************************************)
 
 (*** isfin_pushs *)
 lemma gr_isf_pushs (n) (f): 𝐅❪f❫ → 𝐅❪⫯*[n]f❫.
 #n @(nat_ind_succ … n) -n /3 width=3 by gr_isf_push/
 qed.
 
-(* Inversion lemmas with iterated push **************************************)
+(* Inversions with gr_pushs *************************************************)
 
 (*** isfin_inv_pushs *)
 lemma gr_isf_inv_pushs (n) (g): 𝐅❪⫯*[n]g❫ → 𝐅❪g❫.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isf_tl.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isf_tl.ma
index da0992aa0..52bc146fe 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isf_tl.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isf_tl.ma
@@ -15,9 +15,9 @@
 include "ground/relocation/gr_tl.ma".
 include "ground/relocation/gr_isf.ma".
 
-(* FINITE COLENGTH CONDITION FOR GENERIC RELOCATION MAPS *)
+(* FINITE COLENGTH CONDITION FOR GENERIC RELOCATION MAPS ********************)
 
-(* Properties with tail *****************************************************)
+(* Constructions with gr_tl *************************************************)
 
 (*** isfin_tl *)
 lemma gr_isf_tl (f): 𝐅❪f❫ → 𝐅❪⫱f❫.
@@ -25,7 +25,7 @@ lemma gr_isf_tl (f): 𝐅❪f❫ → 𝐅❪⫱f❫.
 /3 width=3 by gr_isf_inv_push, gr_isf_inv_next/
 qed.
 
-(* Inversion lemmas with tail ***********************************************)
+(* Inversions with gr_tl ****************************************************)
 
 (*** isfin_inv_tl *)
 lemma gr_isf_inv_tl (g): 𝐅❪⫱g❫ → 𝐅❪g❫.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isf_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isf_tls.ma
index 4f817a9a2..ebd7a36e2 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isf_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isf_tls.ma
@@ -15,15 +15,15 @@
 include "ground/relocation/gr_tls.ma".
 include "ground/relocation/gr_isf_tl.ma".
 
-(* FINITE COLENGTH CONDITION FOR GENERIC RELOCATION MAPS *)
+(* FINITE COLENGTH CONDITION FOR GENERIC RELOCATION MAPS ********************)
 
-(* Properties with iterated tail **************************************)
+(* Constructions with gr_tls ************************************************)
 
 lemma gr_isf_tls (n) (f): 𝐅❪f❫ → 𝐅❪⫱*[n]f❫.
 #n @(nat_ind_succ … n) -n /3 width=1 by gr_isf_tl/
 qed.
 
-(* Inversion lemmas with iterated tail **************************************)
+(* Inversions with gr_tls ***************************************************)
 
 (*** isfin_inv_tls *)
 lemma gr_isf_inv_tls (n) (g): 𝐅❪⫱*[n]g❫ → 𝐅❪g❫.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isf_uni.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isf_uni.ma
index a74076620..816500b63 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isf_uni.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isf_uni.ma
@@ -15,9 +15,9 @@
 include "ground/relocation/gr_fcla_uni.ma".
 include "ground/relocation/gr_isf.ma".
 
-(* FINITE COLENGTH CONDITION FOR GENERIC RELOCATION MAPS *)
+(* FINITE COLENGTH CONDITION FOR GENERIC RELOCATION MAPS ********************)
 
-(* Properties with gr_uni ***************************)
+(* Constructions with gr_uni ************************************************)
 
 (*** isfin_uni *)
 lemma gr_isf_uni (n): 𝐅❪𝐮❨n❩❫.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isi.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isi.ma
index 464c72bc7..e9a41cfab 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isi.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isi.ma
@@ -15,7 +15,7 @@
 include "ground/notation/relations/predicate_i_1.ma".
 include "ground/relocation/gr_map.ma".
 
-(* IDENTITY CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* IDENTITY CONDITION FOR GENERIC RELOCATION MAPS ***************************)
 
 (*** isid *)
 coinductive gr_isi: predicate gr_map ≝
@@ -28,7 +28,7 @@ interpretation
   "identity condition (generic relocation maps)"
   'PredicateI f = (gr_isi f).
 
-(* Basic inversion lemmas ***************************************************)
+(* Basic inversions *********************************************************)
 
 (*** isid_inv_gen *)
 lemma gr_isi_inv_gen (g): 𝐈❪g❫ → ∃∃f. 𝐈❪f❫ & ⫯f = g.
@@ -36,7 +36,7 @@ lemma gr_isi_inv_gen (g): 𝐈❪g❫ → ∃∃f. 𝐈❪f❫ & ⫯f = g.
 #f #g #Hf /2 width=3 by ex2_intro/
 qed-.
 
-(* Advanced inversion lemmas ************************************************)
+(* Advanced inversions ******************************************************)
 
 (*** isid_inv_push *)
 lemma gr_isi_inv_push (g): 𝐈❪g❫ → ∀f. ⫯f = g → 𝐈❪f❫.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isi_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isi_eq.ma
index fd631c333..7a1967d00 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isi_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isi_eq.ma
@@ -15,9 +15,9 @@
 include "ground/relocation/gr_tl_eq_eq.ma".
 include "ground/relocation/gr_isi.ma".
 
-(* IDENTITY CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* IDENTITY CONDITION FOR GENERIC RELOCATION MAPS ***************************)
 
-(* Properties with gr_eq *********************************************************)
+(* Constructions with gr_eq *************************************************)
 
 (*** isid_eq_repl_back *)
 corec lemma gr_isi_eq_repl_back:
@@ -33,7 +33,7 @@ lemma gr_isi_eq_repl_fwd:
       gr_eq_repl_fwd … gr_isi.
 /3 width=3 by gr_isi_eq_repl_back, gr_eq_repl_sym/ qed-.
 
-(* Main inversion lemmas with gr_eq ****************************************************)
+(* Main inversions with gr_eq ***********************************************)
 
 (*** isid_inv_eq_repl *)
 corec theorem gr_isi_inv_eq_repl (g1) (g2): 𝐈❪g1❫ → 𝐈❪g2❫ → g1 ≡ g2.
@@ -43,7 +43,7 @@ cases (gr_isi_inv_gen … H2) -H2
 /3 width=5 by gr_eq_push/
 qed-.
 
-(* Alternative definition with gr_eq ***************************************************)
+(* Alternative definition with gr_eq ****************************************)
 
 (*** eq_push_isid *)
 corec lemma gr_eq_push_isi (f): ⫯f ≡ f → 𝐈❪f❫.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isi_id.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isi_id.ma
index f2d1efe1e..c496762e4 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isi_id.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isi_id.ma
@@ -15,15 +15,15 @@
 include "ground/relocation/gr_id.ma".
 include "ground/relocation/gr_isi_eq.ma".
 
-(* IDENTITY CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* IDENTITY CONDITION FOR GENERIC RELOCATION MAPS ***************************)
 
-(* Properties with gr_id *********************************************************)
+(* Constructions with gr_id *************************************************)
 
 (*** id_isid *)
 lemma gr_isi_id: 𝐈❪𝐢❫.
 /2 width=1 by gr_eq_push_isi/ qed.
 
-(* Alternative definition with gr_id and gr_eq *******************************************)
+(* Alternative definition with gr_id and gr_eq ******************************)
 
 (*** eq_id_isid *)
 lemma gr_eq_id_isi (f): 𝐢 ≡ f → 𝐈❪f❫.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isi_pat.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isi_pat.ma
index 95b57f5ee..a8c35fe0a 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isi_pat.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isi_pat.ma
@@ -15,23 +15,23 @@
 include "ground/relocation/gr_isi_id.ma".
 include "ground/relocation/gr_pat_pat_id.ma".
 
-(* IDENTITY CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* IDENTITY CONDITION FOR GENERIC RELOCATION MAPS ***************************)
 
-(* Advanced properties on isid **********************************************)
+(* Advanced constructions with gr_isi ***************************************)
 
 (*** isid_at *)
 lemma gr_isi_pat (f): (∀i. @❪i,f❫ ≘ i) → 𝐈❪f❫.
 /3 width=1 by gr_eq_id_isi, gr_pat_inv_id/
 qed.
 
-(* Inversion lemmas on pat ****************************************)
+(* Inversions with gr_pat ***************************************************)
 
 (*** isid_inv_at *)
 lemma gr_isi_inv_pat (f) (i): 𝐈❪f❫ → @❪i,f❫ ≘ i.
 /3 width=3 by gr_isi_inv_eq_id, gr_pat_id, gr_pat_eq_repl_back/
 qed-.
 
-(* Destructions with pat *)
+(* Destructions with gr_pat *************************************************)
 
 (*** isid_inv_at_mono *)
 lemma gr_isi_pat_des (f) (i1) (i2): 𝐈❪f❫ → @❪i1,f❫ ≘ i2 → i1 = i2.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isi_pushs.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isi_pushs.ma
index bf245e978..e9b3cf054 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isi_pushs.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isi_pushs.ma
@@ -15,16 +15,16 @@
 include "ground/relocation/gr_pushs.ma".
 include "ground/relocation/gr_isi.ma".
 
-(* IDENTITY CONDITION FOR GENERIC RELOCATION MAPS  ******************************************************)
+(* IDENTITY CONDITION FOR GENERIC RELOCATION MAPS ***************************)
 
-(* Properties with gr_pushs *)
+(* Constructions with gr_pushs **********************************************)
 
 (*** isid_pushs *)
 lemma gr_isi_pushs (n) (f): 𝐈❪f❫ → 𝐈❪⫯*[n]f❫.
 #n @(nat_ind_succ … n) -n /3 width=3 by gr_isi_push/
 qed.
 
-(* Inversion lemmas with iterated push **************************************)
+(* Inversions with gr_pushs *************************************************)
 
 (*** isid_inv_pushs *)
 lemma gr_isi_inv_pushs (n) (g): 𝐈❪⫯*[n]g❫ → 𝐈❪g❫.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isi_tl.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isi_tl.ma
index 4a80d36e4..abf089d54 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isi_tl.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isi_tl.ma
@@ -15,9 +15,9 @@
 include "ground/relocation/gr_tl.ma".
 include "ground/relocation/gr_isi.ma".
 
-(* IDENTITY CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* IDENTITY CONDITION FOR GENERIC RELOCATION MAPS ***************************)
 
-(* Properties with tail *****************************************************)
+(* Constructions with gr_tl *************************************************)
 
 (*** isid_tl *)
 lemma gr_isi_tl (f): 𝐈❪f❫ → 𝐈❪⫱f❫.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isi_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isi_tls.ma
index a1cc29b90..cdef65ddb 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isi_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isi_tls.ma
@@ -15,9 +15,9 @@
 include "ground/relocation/gr_tls.ma".
 include "ground/relocation/gr_isi_tl.ma".
 
-(* IDENTITY CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* IDENTITY CONDITION FOR GENERIC RELOCATION MAPS ***************************)
 
-(* Properties with iterated tail ********************************************)
+(* Constructions with gr_tls ************************************************)
 
 (*** isid_tls *)
 lemma gr_isi_tls (n) (f): 𝐈❪f❫ → 𝐈❪⫱*[n]f❫.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isi_uni.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isi_uni.ma
index 34421d67a..2763d9a40 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isi_uni.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isi_uni.ma
@@ -15,15 +15,15 @@
 include "ground/relocation/gr_uni.ma".
 include "ground/relocation/gr_isi_id.ma".
 
-(* IDENTITY CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* IDENTITY CONDITION FOR GENERIC RELOCATION MAPS ***************************)
 
-(* Properties with test for identity ****************************************)
+(* Constructions with gr_isi ************************************************)
 
 (*** uni_inv_isid uni_isi *)
 lemma gr_uni_isi (f): 𝐮❨𝟎❩ ≡ f → 𝐈❪f❫.
 /2 width=1 by gr_eq_id_isi/ qed.
 
-(* Inversion lemmas with test for identity **********************************)
+(* Inversions with gr_isi ***************************************************)
 
 (*** uni_isid isi_inv_uni *)
 lemma gr_isi_inv_uni (f): 𝐈❪f❫ → 𝐮❨𝟎❩ ≡ f.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_ist.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_ist.ma
index c20743e1a..8a3636574 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_ist.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_ist.ma
@@ -15,7 +15,7 @@
 include "ground/notation/relations/predicate_t_1.ma".
 include "ground/relocation/gr_pat.ma".
 
-(* TOTALITY CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* TOTALITY CONDITION FOR GENERIC RELOCATION MAPS ***************************)
 
 (*** istot *)
 definition gr_ist: predicate gr_map ≝
@@ -25,7 +25,7 @@ interpretation
   "totality condition (generic relocation maps)"
   'PredicateT f = (gr_ist f).
 
-(* Basic inversion lemmas ***************************************************)
+(* Basic inversions *********************************************************)
 
 (*** istot_inv_push *)
 lemma gr_ist_inv_push (g): 𝐓❪g❫ → ∀f. ⫯f = g → 𝐓❪f❫.
@@ -39,7 +39,7 @@ lemma gr_ist_inv_next (g): 𝐓❪g❫ → ∀f. ↑f = g → 𝐓❪f❫.
 #j #Hg elim (gr_pat_inv_next … Hg … H) -Hg -H /2 width=2 by ex_intro/
 qed-.
 
-(* Properties on tl *********************************************************)
+(* Constructions with gr_tl *************************************************)
 
 (*** istot_tl *)
 lemma gr_ist_tl (f): 𝐓❪f❫ → 𝐓❪⫱f❫.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_ist_isi.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_ist_isi.ma
index 593d63e79..90e8f4852 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_ist_isi.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_ist_isi.ma
@@ -15,9 +15,9 @@
 include "ground/relocation/gr_isi_pat.ma".
 include "ground/relocation/gr_ist.ma".
 
-(* TOTALITY CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* TOTALITY CONDITION FOR GENERIC RELOCATION MAPS ***************************)
 
-(* Advanced properties on isid **********************************************)
+(* Advanced constructions with gr_isi ***************************************)
 
 (*** isid_at_total *)
 lemma gr_isi_pat_total: ∀f. 𝐓❪f❫ → (∀i1,i2. @❪i1,f❫ ≘ i2 → i1 = i2) → 𝐈❪f❫.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_ist_ist.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_ist_ist.ma
index f80e08496..cfa6aaa91 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_ist_ist.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_ist_ist.ma
@@ -17,9 +17,9 @@ include "ground/relocation/gr_pat_lt.ma".
 include "ground/relocation/gr_pat_pat.ma".
 include "ground/relocation/gr_ist.ma".
 
-(* TOTALITY CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* TOTALITY CONDITION FOR GENERIC RELOCATION MAPS ***************************)
 
-(* Advanced properties on at ************************************************)
+(* Advanced constructions with gr_pat ***************************************)
 
 (*** at_dec *)
 lemma gr_pat_dec (f) (i1) (i2): 𝐓❪f❫ → Decidable (@❪i1,f❫ ≘ i2).
@@ -41,7 +41,7 @@ lapply (dec_plt (λi1.@❪i1,f❫ ≘ i2) … (↑i2)) [| * ]
 ]
 qed-.
 
-(* Main forward lemmas on at ************************************************)
+(* Main destructions with gr_pat ********************************************)
 
 (*** at_ext *)
 corec theorem gr_eq_ext_pat (f1) (f2): 𝐓❪f1❫ → 𝐓❪f2❫ →
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_ist_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_ist_tls.ma
index 1dcf5c5cf..e1c04930a 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_ist_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_ist_tls.ma
@@ -15,9 +15,9 @@
 include "ground/relocation/gr_tls.ma".
 include "ground/relocation/gr_ist.ma".
 
-(* TOTALITY CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* TOTALITY CONDITION FOR GENERIC RELOCATION MAPS ***************************)
 
-(* Properties on tls ********************************************************)
+(* Constructions with gr_tls ************************************************)
 
 (*** istot_tls *)
 lemma gr_ist_tls (n) (f): 𝐓❪f❫ → 𝐓❪⫱*[n]f❫.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isu.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isu.ma
index e731efcfc..2a81141fa 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isu.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isu.ma
@@ -15,7 +15,7 @@
 include "ground/notation/relations/predicate_u_1.ma".
 include "ground/relocation/gr_isi.ma".
 
-(* UNIFORMITY CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* UNIFORMITY CONDITION FOR GENERIC RELOCATION MAPS *************************)
 
 (*** isuni *)
 inductive gr_isu: predicate gr_map ≝
@@ -29,7 +29,7 @@ interpretation
   "uniformity condition (generic relocation maps)"
   'PredicateU f = (gr_isu f).
 
-(* Basic inversion lemmas ***************************************************)
+(* Basic inversions *********************************************************)
 
 (*** isuni_inv_push *)
 lemma gr_isu_inv_push (g): 𝐔❪g❫ → ∀f. ⫯f = g → 𝐈❪f❫.
@@ -49,7 +49,7 @@ lemma gr_isu_inv_next (g): 𝐔❪g❫ → ∀f. ↑f = g → 𝐔❪f❫.
 ]
 qed-.
 
-(* Basic forward lemmas *****************************************************)
+(* Basic destructions *******************************************************)
 
 (*** isuni_fwd_push *)
 lemma gr_isu_fwd_push (g): 𝐔❪g❫ → ∀f. ⫯f = g → 𝐔❪f❫.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isu_tl.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isu_tl.ma
index a0cb8dbb9..73fa585b7 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isu_tl.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isu_tl.ma
@@ -15,9 +15,9 @@
 include "ground/relocation/gr_tl.ma".
 include "ground/relocation/gr_isu.ma".
 
-(* UNIFORMITY CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* UNIFORMITY CONDITION FOR GENERIC RELOCATION MAPS *************************)
 
-(* Properties with tail *****************************************************)
+(* Constructions with gr_tl *************************************************)
 
 lemma gr_isu_tl (f): 𝐔❪f❫ → 𝐔❪⫱f❫.
 #f cases (gr_map_split_tl f) * #H
@@ -26,7 +26,7 @@ lemma gr_isu_tl (f): 𝐔❪f❫ → 𝐔❪⫱f❫.
 ]
 qed.
 
-(* Advanced inversion lemmas ***************************************************)
+(* Advanced inversions ******************************************************)
 
 (*** isuni_split *)
 lemma gr_isu_split (g): 𝐔❪g❫ → ∨∨ (∃∃f. 𝐈❪f❫ & ⫯f = g) | (∃∃f.𝐔❪f❫ & ↑f = g).
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isu_uni.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isu_uni.ma
index e8b2c439a..e3fc67281 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isu_uni.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isu_uni.ma
@@ -15,9 +15,9 @@
 include "ground/relocation/gr_isi_uni.ma".
 include "ground/relocation/gr_isu.ma".
 
-(* UNIFORMITY CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* UNIFORMITY CONDITION FOR GENERIC RELOCATION MAPS *************************)
 
-(* Properties with gr_uni **************************************)
+(* Constructions with gr_uni ************************************************)
 
 (*** isuni_uni *)
 lemma gr_isu_uni (n): 𝐔❪𝐮❨n❩❫.
@@ -40,7 +40,7 @@ lemma gr_isu_eq_repl_fwd:
       gr_eq_repl_fwd … gr_isu.
 /3 width=3 by gr_isu_eq_repl_back, gr_eq_repl_sym/ qed-.
 
-(* Inversion lemmas with gr_uni ********************************)
+(* Inversions with gr_uni ***************************************************)
 
 (*** uni_isuni *)
 lemma gr_isu_inv_uni (f): 𝐔❪f❫ → ∃n. 𝐮❨n❩ ≡ f.
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.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_nat.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_nat.ma
index 612022cbe..754ef8b69 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_nat.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_nat.ma
@@ -16,7 +16,7 @@ include "ground/notation/relations/ratsucc_3.ma".
 include "ground/arith/nat_pred_succ.ma".
 include "ground/relocation/gr_pat.ma".
 
-(* NON-NEGATIVE APPLICATION FOR GENERIC RELOCATION MAPS *****************************)
+(* NON-NEGATIVE APPLICATION FOR GENERIC RELOCATION MAPS *********************)
 
 definition gr_nat: relation3 gr_map nat nat ≝
            λf,l1,l2. @❪↑l1,f❫ ≘ ↑l2.
@@ -25,7 +25,7 @@ interpretation
   "relational non-negative application (generic relocation maps)"
   'RAtSucc l1 f l2 = (gr_nat f l1 l2).
 
-(* Basic properties *********************************************************)
+(* Basic constructions ******************************************************)
 
 lemma gr_nat_refl (f) (g) (k1) (k2):
       (⫯f) = g → 𝟎 = k1 → 𝟎 = k2 → @↑❪k1,g❫ ≘ k2.
@@ -52,7 +52,7 @@ lemma gr_nat_pred_bi (f) (i1) (i2):
 //
 qed.
 
-(* Basic inversion lemmas ***************************************************)
+(* Basic inversions *********************************************************)
 
 (*** gr_nat_inv_ppx *)
 lemma gr_nat_inv_zero_push (f) (l1) (l2):
@@ -82,7 +82,7 @@ elim (gr_pat_inv_next … H) -H [|*: // ] #k2
 @(ex2_intro … (↓k2)) //
 qed-.
 
-(* Advanced inversion lemmas ************************************************)
+(* Advanced inversions ******************************************************)
 
 (*** gr_nat_inv_ppn *)
 lemma gr_nat_inv_zero_push_succ (f) (l1) (l2):
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_nat_basic.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_nat_basic.ma
index 77ed0ed6d..a9c9cae2a 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_nat_basic.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_nat_basic.ma
@@ -15,9 +15,9 @@
 include "ground/relocation/gr_basic.ma".
 include "ground/relocation/gr_nat_uni.ma".
 
-(* NON-NEGATIVE APPLICATION FOR GENERIC RELOCATION MAPS *****************************)
+(* NON-NEGATIVE APPLICATION FOR GENERIC RELOCATION MAPS *********************)
 
-(* Properties with gr_basic **********************************************)
+(* Constructions with gr_basic **********************************************)
 
 lemma gr_nat_basic_lt (m) (n) (l):
       l < m → @↑❪l, 𝐛❨m,n❩❫ ≘ l.
@@ -40,7 +40,7 @@ elim (nle_inv_succ_sn … H) -H #Hml #H >H -H
 /3 width=7 by gr_nat_push/
 qed.
 
-(* Inversion lemmas with gr_basic ****************************************)
+(* Inversions with gr_basic *************************************************)
 
 lemma gr_nat_basic_inv_lt (m) (n) (l) (k):
       l < m → @↑❪l, 𝐛❨m,n❩❫ ≘ k → l = k.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_nat_uni.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_nat_uni.ma
index 0a79bbc18..0812fab2e 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_nat_uni.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_nat_uni.ma
@@ -16,16 +16,16 @@ include "ground/arith/nat_plus_rplus.ma".
 include "ground/relocation/gr_pat_uni.ma".
 include "ground/relocation/gr_nat_nat.ma".
 
-(* NON-NEGATIVE APPLICATION FOR GENERIC RELOCATION MAPS *****************************)
+(* NON-NEGATIVE APPLICATION FOR GENERIC RELOCATION MAPS *********************)
 
-(* Properties with uniform relocations **************************************)
+(* Constructions with gr_uni ************************************************)
 
 lemma gr_nat_uni (n) (l):
       @↑❪l,𝐮❨n❩❫ ≘ l+n.
 /2 width=1 by gr_nat_pred_bi/
 qed.
 
-(* Inversion lemmas with uniform relocations ********************************)
+(* Inversions with gr_uni ***************************************************)
 
 lemma gr_nat_inv_uni (n) (l) (k):
       @↑❪l,𝐮❨n❩❫ ≘ k → k = l+n.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_nexts.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_nexts.ma
index ff1595ced..88065e56d 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_nexts.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_nexts.ma
@@ -16,7 +16,7 @@ include "ground/notation/functions/uparrowstar_2.ma".
 include "ground/arith/nat_succ_iter.ma".
 include "ground/relocation/gr_map.ma".
 
-(* ITERATED NEXT FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* ITERATED NEXT FOR GENERIC RELOCATION MAPS ********************************)
 
 (*** nexts *)
 definition gr_nexts (f:gr_map) (n:nat) ≝
@@ -26,7 +26,7 @@ interpretation
   "iterated next (generic relocation maps)"
   'UpArrowStar n f = (gr_nexts f n).
 
-(* Basic properties *********************************************************)
+(* Basic constructions ******************************************************)
 
 (*** nexts_O *)
 lemma gr_nexts_zero:
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_nexts_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_nexts_eq.ma
index 928cb4289..addd6c42c 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_nexts_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_nexts_eq.ma
@@ -15,9 +15,9 @@
 include "ground/relocation/gr_eq.ma".
 include "ground/relocation/gr_nexts.ma".
 
-(* ITERATED NEXT FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* ITERATED NEXT FOR GENERIC RELOCATION MAPS ********************************)
 
-(* Properties with gr_eq ******************************************************)
+(* Constructions with gr_eq *************************************************)
 
 (*** nexts_eq_repl *)
 lemma gr_nexts_eq_repl (n):
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat.ma
index 926e94cda..5cd1c947d 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat.ma
@@ -17,7 +17,7 @@ include "ground/xoa/ex_3_2.ma".
 include "ground/arith/pnat.ma".
 include "ground/relocation/gr_tl.ma".
 
-(* POSITIVE APPLICATION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* POSITIVE APPLICATION FOR GENERIC RELOCATION MAPS *************************)
 
 (*** at *)
 coinductive gr_pat: relation3 gr_map pnat pnat ≝
@@ -42,7 +42,7 @@ definition H_gr_pat_div: relation4 gr_map gr_map gr_map gr_map ≝
            ∀jf,jg,j. @❪jf,f2❫ ≘ j → @❪jg,g2❫ ≘ j →
            ∃∃j0. @❪j0,f1❫ ≘ jf & @❪j0,g1❫ ≘ jg.
 
-(* Basic inversion lemmas ***************************************************)
+(* Basic inversions *********************************************************)
 
 (*** at_inv_ppx *)
 lemma gr_pat_inv_unit_push (f) (i1) (i2):
@@ -75,7 +75,7 @@ lemma gr_pat_inv_next (f) (i1) (i2):
 ]
 qed-.
 
-(* Advanced inversion lemmas ************************************************)
+(* Advanced inversions ******************************************************)
 
 (*** at_inv_ppn *)
 lemma gr_pat_inv_unit_push_succ (f) (i1) (i2):
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat_basic.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat_basic.ma
index 8ffe58797..3960be7bd 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat_basic.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat_basic.ma
@@ -14,9 +14,9 @@
 
 include "ground/relocation/gr_nat_basic.ma".
 
-(* POSITIVE APPLICATION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* POSITIVE APPLICATION FOR GENERIC RELOCATION MAPS *************************)
 
-(* Properties with gr_basic **********************************************)
+(* Constructions with gr_basic **********************************************)
 
 (*** at_basic_lt *)
 lemma gr_pat_basic_lt (m) (n) (i):
@@ -32,7 +32,7 @@ lemma gr_pat_basic_ge (m) (n) (i):
 /3 width=1 by gr_nat_basic_ge, nlt_inv_succ_dx/
 qed.
 
-(* Inversion lemmas with gr_basic ****************************************)
+(* Inversions with gr_basic *************************************************)
 
 (*** at_basic_inv_lt *)
 lemma gr_pat_basic_inv_lt (m) (n) (i) (j):
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat_eq.ma
index ad51d7f85..8cd42b575 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat_eq.ma
@@ -15,9 +15,9 @@
 include "ground/relocation/gr_tl_eq.ma".
 include "ground/relocation/gr_pat_lt.ma".
 
-(* POSITIVE APPLICATION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* POSITIVE APPLICATION FOR GENERIC RELOCATION MAPS *************************)
 
-(* Properties with gr_eq *)
+(* Constructions with gr_eq *************************************************)
 
 (*** at_eq_repl_back *)
 corec lemma gr_pat_eq_repl_back (i1) (i2):
@@ -45,7 +45,7 @@ lemma gr_pat_eq (f): ⫯f ≡ f → ∀i. @❪i,f❫ ≘ i.
 ]
 qed.
 
-(* Inversions with gr_eq *)
+(* Inversions with gr_eq ****************************************************)
 
 corec lemma gr_pat_inv_eq (f):
             (∀i. @❪i,f❫ ≘ i) → ⫯f ≡ f.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat_id.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat_id.ma
index 286ecfda9..17464b3d8 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat_id.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat_id.ma
@@ -15,15 +15,15 @@
 include "ground/relocation/gr_id_eq.ma".
 include "ground/relocation/gr_pat_eq.ma".
 
-(* POSITIVE APPLICATION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* POSITIVE APPLICATION FOR GENERIC RELOCATION MAPS *************************)
 
-(* Properties on id ************************************************)
+(* Constructions with gr_id *************************************************)
 
 (*** id_at *)
 lemma gr_pat_id (i): @❪i,𝐢❫ ≘ i.
 /2 width=1 by gr_pat_eq, gr_eq_refl/ qed.
 
-(* Inversions with id *)
+(* Inversions with gr_id ****************************************************)
 
 (*** id_inv_at *)
 lemma gr_pat_inv_id (f):
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):
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat_pat.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat_pat.ma
index c882a8293..b652722f3 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat_pat.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat_pat.ma
@@ -15,9 +15,9 @@
 include "ground/arith/pnat_lt_pred.ma".
 include "ground/relocation/gr_pat.ma".
 
-(* POSITIVE APPLICATION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* POSITIVE APPLICATION FOR GENERIC RELOCATION MAPS *************************)
 
-(* Main properties **********************************************************)
+(* Main constructions *******************************************************)
 
 (*** at_monotonic *)
 theorem gr_pat_monotonic:
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat_pat_id.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat_pat_id.ma
index e4dee24af..e20fb6e5f 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat_pat_id.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat_pat_id.ma
@@ -15,16 +15,16 @@
 include "ground/relocation/gr_pat_id.ma".
 include "ground/relocation/gr_pat_pat.ma".
 
-(* POSITIVE APPLICATION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* POSITIVE APPLICATION FOR GENERIC RELOCATION MAPS *************************)
 
-(* Advanced Forward lemmas on id ********************************************)
+(* Advanced destructions with gr_id *****************************************)
 
 (*** at_id_fwd *)
 lemma gr_pat_id_des (i1) (i2):
       @❪i1,𝐢❫ ≘ i2 → i1 = i2.
 /2 width=4 by gr_pat_mono/ qed-.
 
-(* Main properties on id ****************************************************)
+(* Main constructions with gr_id ********************************************)
 
 (*** at_div_id_dx *)
 theorem gr_pat_div_id_dx (f):
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat_tls.ma
index 524e9aecc..1eca80ecf 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat_tls.ma
@@ -16,9 +16,9 @@ include "ground/arith/pnat_plus.ma".
 include "ground/relocation/gr_tls.ma".
 include "ground/relocation/gr_pat_eq.ma".
 
-(* POSITIVE APPLICATION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* POSITIVE APPLICATION FOR GENERIC RELOCATION MAPS *************************)
 
-(* Properties on tls ********************************************************)
+(* Constructions with gr_tls ************************************************)
 
 (* Note: this requires ↑ on first n *)
 (*** at_pxx_tls *)
@@ -42,7 +42,7 @@ lemma gr_pat_tls (n2) (f): ⫯⫱*[↑n2]f ≡ ⫱*[n2]f → ∃i1. @❪i1,f❫
 ]
 qed-.
 
-(* Inversion lemmas with tls ************************************************)
+(* Inversions with gr_tls ***************************************************)
 
 (* Note: this does not require ↑ on second and third p *)
 (*** at_inv_nxx *)
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat_uni.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat_uni.ma
index f3c53a82e..a75ecb23e 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat_uni.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat_uni.ma
@@ -16,9 +16,9 @@ include "ground/arith/nat_rplus_succ.ma".
 include "ground/relocation/gr_uni.ma".
 include "ground/relocation/gr_pat_pat_id.ma".
 
-(* POSITIVE APPLICATION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* POSITIVE APPLICATION FOR GENERIC RELOCATION MAPS *************************)
 
-(* Properties with uniform relocations **************************************)
+(* Constructions with gr_uni ************************************************)
 
 (*** at_uni *)
 lemma gr_pat_uni (n) (i):
@@ -27,7 +27,7 @@ lemma gr_pat_uni (n) (i):
 /2 width=5 by gr_pat_next/
 qed.
 
-(* Inversion lemmas with uniform relocations ********************************)
+(* Inversions with gr_uni ***************************************************)
 
 (*** at_inv_uni *)
 lemma gr_pat_inv_uni (n) (i) (j):
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_pushs.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_pushs.ma
index 9c2aa0992..f37600948 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_pushs.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_pushs.ma
@@ -16,7 +16,7 @@ include "ground/notation/functions/upspoonstar_2.ma".
 include "ground/arith/nat_succ_iter.ma".
 include "ground/relocation/gr_map.ma".
 
-(* ITERATED PUSH FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* ITERATED PUSH FOR GENERIC RELOCATION MAPS ********************************)
 
 (*** pushs *)
 definition gr_pushs (f:gr_map) (n:nat) ≝
@@ -26,7 +26,7 @@ interpretation
   "iterated push (generic relocation maps)"
   'UpSpoonStar n f = (gr_pushs f n).
 
-(* Basic properties *********************************************************)
+(* Basic constructions ******************************************************)
 
 (*** pushs_O *)
 lemma gr_pushs_zero:
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_pushs_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_pushs_eq.ma
index 7361dcbdc..75cd53974 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_pushs_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_pushs_eq.ma
@@ -15,9 +15,9 @@
 include "ground/relocation/gr_eq.ma".
 include "ground/relocation/gr_pushs.ma".
 
-(* ITERATED PUSH FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* ITERATED PUSH FOR GENERIC RELOCATION MAPS ********************************)
 
-(* Properties with gr_eq *)
+(* Constructions with gr_eq *************************************************)
 
 (*** pushs_eq_repl *)
 lemma gr_pushs_eq_repl (n):
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sand.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sand.ma
index 79fd584d1..e0430e92b 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sand.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sand.ma
@@ -15,7 +15,7 @@
 include "ground/notation/relations/rintersection_3.ma".
 include "ground/relocation/gr_tl.ma".
 
-(* RELATIONAL INTERSECTION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL INTERSECTION FOR GENERIC RELOCATION MAPS **********************)
 
 (*** sand *)
 coinductive gr_sand: relation3 gr_map gr_map gr_map ≝
@@ -37,7 +37,7 @@ interpretation
   "relational intersection (generic relocation maps)"
   'RIntersection f1 f2 f = (gr_sand f1 f2 f).
 
-(* Basic properties *********************************************************)
+(* Basic constructions ******************************************************)
 
 (*** sand_refl *)
 corec lemma gr_sand_idem:
@@ -60,7 +60,7 @@ corec lemma gr_sand_comm:
 ] /2 width=7 by/
 qed-.
 
-(* Basic inversion lemmas ***************************************************)
+(* Basic inversions *********************************************************)
 
 (*** sand_inv_ppx *)
 lemma gr_sand_inv_push_bi:
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sand_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sand_eq.ma
index a199c7706..86c2a71dc 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sand_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sand_eq.ma
@@ -15,9 +15,9 @@
 include "ground/relocation/gr_tl_eq.ma".
 include "ground/relocation/gr_sand.ma".
 
-(* RELATIONAL INTERSECTION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL INTERSECTION FOR GENERIC RELOCATION MAPS **********************)
 
-(* Properties with gr_eq *)
+(* Constructions with gr_eq *************************************************)
 
 (*** sand_eq_repl_back1 *)
 corec lemma gr_sand_eq_repl_back_sn:
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sdj.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sdj.ma
index 66281ee0f..f8b101d22 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sdj.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sdj.ma
@@ -15,7 +15,7 @@
 include "ground/notation/relations/parallel_2.ma".
 include "ground/relocation/gr_tl.ma".
 
-(* DISJOINTNESS FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* DISJOINTNESS FOR GENERIC RELOCATION MAPS *********************************)
 
 (*** sdj *)
 coinductive gr_sdj: relation gr_map ≝
@@ -34,7 +34,7 @@ interpretation
   "disjointness (generic relocation maps)"
   'Parallel f1 f2 = (gr_sdj f1 f2).
 
-(* Basic properties *********************************************************)
+(* Basic constructions ******************************************************)
 
 (*** sdj_sym *)
 corec lemma gr_sdj_sym:
@@ -48,7 +48,7 @@ corec lemma gr_sdj_sym:
 /2 width=1 by/
 qed-.
 
-(* Basic inversion lemmas ***************************************************)
+(* Basic inversions *********************************************************)
 
 (*** sdj_inv_pp *)
 lemma gr_sdj_inv_push_bi:
@@ -97,7 +97,7 @@ lemma gr_sdj_inv_next_bi:
 ]
 qed-.
 
-(* Advanced inversion lemmas ************************************************)
+(* Advanced inversions ******************************************************)
 
 (*** sdj_inv_nx *)
 lemma gr_sdj_inv_next_sn:
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sdj_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sdj_eq.ma
index 3cb13289d..f4b82a59b 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sdj_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sdj_eq.ma
@@ -15,9 +15,9 @@
 include "ground/relocation/gr_tl_eq.ma".
 include "ground/relocation/gr_sdj.ma".
 
-(* DISJOINTNESS FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* DISJOINTNESS FOR GENERIC RELOCATION MAPS *********************************)
 
-(* Properties with gr_eq *********************************************************)
+(* Constructions with gr_eq *************************************************)
 
 (*** sdj_eq_repl_back1 *)
 corec lemma gr_sdj_eq_repl_back_sn:
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sdj_isi.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sdj_isi.ma
index d98726d11..fac14a47a 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sdj_isi.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sdj_isi.ma
@@ -15,9 +15,9 @@
 include "ground/relocation/gr_isi.ma".
 include "ground/relocation/gr_sdj.ma".
 
-(* DISJOINTNESS FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* DISJOINTNESS FOR GENERIC RELOCATION MAPS *********************************)
 
-(* Properties with isid *****************************************************)
+(* Constructions with gr_isi ************************************************)
 
 (*** sdj_isid_dx *)
 corec lemma gr_sdj_isi_dx:
@@ -35,7 +35,7 @@ corec lemma gr_sdj_isi_sn:
 /3 width=5 by gr_sdj_push_next, gr_sdj_push_bi/
 qed.
 
-(* Inversion lemmas with isid ***********************************************)
+(* Inversions with gr_isi ***************************************************)
 
 (*** sdj_inv_refl *)
 corec lemma gr_sdj_inv_refl:
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sle.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sle.ma
index 6ad077f23..8aec4d513 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sle.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sle.ma
@@ -14,7 +14,7 @@
 
 include "ground/relocation/gr_tl.ma".
 
-(* INCLUSION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* INCLUSION FOR GENERIC RELOCATION MAPS ************************************)
 
 (*** sle *)
 coinductive gr_sle: relation gr_map ≝
@@ -33,7 +33,7 @@ interpretation
   "inclusion (generic relocation maps)"
   'subseteq f1 f2 = (gr_sle f1 f2).
 
-(* Basic properties *********************************************************)
+(* Basic constructions ******************************************************)
 
 (*** sle_refl *)
 corec lemma gr_sle_refl:
@@ -42,7 +42,7 @@ corec lemma gr_sle_refl:
 [ @(gr_sle_push … H H) | @(gr_sle_next … H H) ] -H //
 qed.
 
-(* Basic inversion lemmas ***************************************************)
+(* Basic inversions *********************************************************)
 
 (*** sle_inv_xp *)
 lemma gr_sle_inv_push_dx:
@@ -76,7 +76,7 @@ lemma gr_sle_inv_push_next:
 ]
 qed-.
 
-(* Advanced inversion lemmas ************************************************)
+(* Advanced inversions ******************************************************)
 
 (*** sle_inv_pp *)
 lemma gr_sle_inv_push_bi:
@@ -120,7 +120,7 @@ elim (gr_map_split_tl g1) #H1 #H #f2 #H2
 /3 width=3 by ex2_intro, or_introl, or_intror/
 qed-.
 
-(* Properties with tail *****************************************************)
+(* Constructions with gr_tl *************************************************)
 
 (*** sle_px_tl *)
 lemma gr_sle_push_sn_tl:
@@ -145,7 +145,7 @@ lemma gr_sle_tl:
 ]
 qed.
 
-(* Inversion lemmas with tail ***********************************************)
+(* Inversions with gr_tl ****************************************************)
 
 (*** sle_inv_tl_sn *)
 lemma gr_sle_inv_tl_sn:
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sle_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sle_eq.ma
index 244ee713a..caa6ae5d5 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sle_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sle_eq.ma
@@ -13,12 +13,12 @@
 (**************************************************************************)
 
 include "ground/relocation/gr_sle.ma".
-(**) (* this should go first *)
+(* * this should go first *)
 include "ground/relocation/gr_tl_eq.ma".
 
-(* INCLUSION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* INCLUSION FOR GENERIC RELOCATION MAPS ************************************)
 
-(* Properties with gr_eq *********************************************************)
+(* Constructions with gr_eq *************************************************)
 
 (*** sle_eq_repl_back1 *)
 corec lemma gr_sle_eq_repl_back_sn:
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sle_isd.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sle_isd.ma
index 27211194b..5174bab31 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sle_isd.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sle_isd.ma
@@ -15,9 +15,9 @@
 include "ground/relocation/gr_isd.ma".
 include "ground/relocation/gr_sle.ma".
 
-(* INCLUSION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* INCLUSION FOR GENERIC RELOCATION MAPS ************************************)
 
-(* Properties with isdiv ****************************************************)
+(* Constructions with gr_isd ************************************************)
 
 (*** sle_isdiv_dx *)
 corec lemma gr_sle_isd_dx:
@@ -27,7 +27,7 @@ corec lemma gr_sle_isd_dx:
 /3 width=5 by gr_sle_weak, gr_sle_next/
 qed.
 
-(* Inversion lemmas with isdiv **********************************************)
+(* Inversions with gr_isd ***************************************************)
 
 (*** sle_inv_isdiv_sn *)
 corec lemma gr_sle_inv_isd_sn:
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sle_isi.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sle_isi.ma
index b05a5da6c..96b277ba2 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sle_isi.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sle_isi.ma
@@ -15,9 +15,9 @@
 include "ground/relocation/gr_isi.ma".
 include "ground/relocation/gr_sle.ma".
 
-(* INCLUSION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* INCLUSION FOR GENERIC RELOCATION MAPS ************************************)
 
-(* Properties with isid *****************************************************)
+(* Constructions with gr_isi ************************************************)
 
 (*** sle_isid_sn *)
 corec lemma gr_sle_isi_sn:
@@ -27,7 +27,7 @@ corec lemma gr_sle_isi_sn:
 /3 width=5 by gr_sle_weak, gr_sle_push/
 qed.
 
-(* Inversion lemmas with isid ***********************************************)
+(* Inversions with gr_isi ***************************************************)
 
 (*** sle_inv_isid_dx *)
 corec lemma gr_sle_inv_isi_dx:
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sle_pushs.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sle_pushs.ma
index e31471cad..41d2bb7ba 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sle_pushs.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sle_pushs.ma
@@ -15,9 +15,9 @@
 include "ground/relocation/gr_pushs.ma".
 include "ground/relocation/gr_sle.ma".
 
-(* INCLUSION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* INCLUSION FOR GENERIC RELOCATION MAPS ************************************)
 
-(* Properties with iterated push ********************************************)
+(* Constructions with gr_pushs **********************************************)
 
 (*** sle_pushs *)
 lemma gr_sle_pushs:
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sle_sle.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sle_sle.ma
index eeebb6dae..f7c34e1e7 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sle_sle.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sle_sle.ma
@@ -14,9 +14,9 @@
 
 include "ground/relocation/gr_sle.ma".
 
-(* INCLUSION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* INCLUSION FOR GENERIC RELOCATION MAPS ************************************)
 
-(* Main properties **********************************************************)
+(* Main constructions *******************************************************)
 
 (*** sle_trans *)
 corec theorem gr_sle_trans:
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sle_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sle_tls.ma
index 102c37ceb..ac4300633 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sle_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sle_tls.ma
@@ -15,9 +15,9 @@
 include "ground/relocation/gr_tls.ma".
 include "ground/relocation/gr_sle.ma".
 
-(* INCLUSION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* INCLUSION FOR GENERIC RELOCATION MAPS ************************************)
 
-(* Properties with iterated tail ********************************************)
+(* Constructions with gr_tls ************************************************)
 
 (*** sle_tls *)
 lemma gr_sle_tls:
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor.ma
index 7152502c2..54911325e 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor.ma
@@ -17,7 +17,7 @@ include "ground/xoa/or_3.ma".
 include "ground/xoa/ex_3_2.ma".
 include "ground/relocation/gr_tl.ma".
 
-(* RELATIONAL UNION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL UNION FOR GENERIC RELOCATION MAPS *****************************)
 
 (*** sor *)
 coinductive gr_sor: relation3 gr_map gr_map gr_map ≝
@@ -39,7 +39,7 @@ interpretation
   "relational union (generic relocation maps)"
   'RUnion f1 f2 f = (gr_sor f1 f2 f).
 
-(* Basic properties *********************************************************)
+(* Basic constructions ******************************************************)
 
 (*** sor_idem *)
 corec lemma gr_sor_idem:
@@ -58,7 +58,7 @@ corec lemma gr_sor_comm:
 [ @gr_sor_push_bi | @gr_sor_push_next | @gr_sor_next_push | @gr_sor_next_bi ] /2 width=7 by/
 qed-.
 
-(* Basic inversion lemmas ***************************************************)
+(* Basic inversions *********************************************************)
 
 (*** sor_inv_ppx *)
 lemma gr_sor_inv_push_bi:
@@ -112,7 +112,7 @@ try elim (eq_inv_gr_push_next … Hx2) try elim (eq_inv_gr_next_push … Hx2)
 /2 width=3 by ex2_intro/
 qed-.
 
-(* Advanced inversion lemmas ************************************************)
+(* Advanced inversions ******************************************************)
 
 (*** sor_inv_ppn *)
 lemma gr_sor_inv_push_bi_next:
@@ -277,7 +277,7 @@ elim (gr_map_split_tl g1) #H1
 ]
 qed-.
 
-(* Properties with tail *****************************************************)
+(* Constructions with gr_tl *************************************************)
 
 (*** sor_tl *)
 lemma gr_sor_tl:
@@ -323,7 +323,7 @@ lemma gr_sor_next_sn_tl:
 /3 width=5 by ex3_2_intro/
 qed-.
 
-(* Inversion lemmas with tail ***********************************************)
+(* Inversions with gr_tl ****************************************************)
 
 (*** sor_inv_tl_sn *)
 lemma gr_sor_inv_tl_sn:
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor_coafter_ist_isf.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor_coafter_ist_isf.ma
index 4595f8f8f..89b457fe1 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor_coafter_ist_isf.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor_coafter_ist_isf.ma
@@ -17,9 +17,9 @@ include "ground/relocation/gr_coafter_isi.ma".
 include "ground/relocation/gr_coafter_ist_isi.ma".
 include "ground/relocation/gr_sor_isi.ma".
 
-(* RELATIONAL UNION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL UNION FOR GENERIC RELOCATION MAPS *****************************)
 
-(* Properties with coafter and ist and isf ****************************************************)
+(* Constructions with gr_coafter and gr_ist and gr_isf **********************)
 
 (*** coafter_sor *)
 lemma gr_sor_coafter_dx_tans:
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor_eq.ma
index 1e9f130c2..96bf535f8 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor_eq.ma
@@ -15,9 +15,9 @@
 include "ground/relocation/gr_tl_eq.ma".
 include "ground/relocation/gr_sor.ma".
 
-(* RELATIONAL UNION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL UNION FOR GENERIC RELOCATION MAPS *****************************)
 
-(* Properties with gr_eq *********************************************************)
+(* Constructions with gr_eq *************************************************)
 
 (*** sor_eq_repl_back1 *)
 corec lemma gr_sor_eq_repl_back_sn:
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor_fcla.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor_fcla.ma
index a1b8e8feb..3540561b2 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor_fcla.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor_fcla.ma
@@ -19,9 +19,9 @@ include "ground/arith/nat_le_max.ma".
 include "ground/relocation/gr_fcla_eq.ma".
 include "ground/relocation/gr_sor_isi.ma".
 
-(* RELATIONAL UNION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL UNION FOR GENERIC RELOCATION MAPS *****************************)
 
-(* Properties with finite colength assignment *******************************)
+(* Constructions with gr_fcla ***********************************************)
 
 (*** sor_fcla_ex *)
 lemma gr_sor_fcla_bi:
@@ -29,7 +29,7 @@ lemma gr_sor_fcla_bi:
       ∃∃f,n. f1 ⋓ f2 ≘ f & 𝐂❪f❫ ≘ n & (n1 ∨ n2) ≤ n & n ≤ n1 + n2.
 #f1 #n1 #Hf1 elim Hf1 -f1 -n1 /3 width=6 by gr_sor_isi_sn, ex4_2_intro/
 #f1 #n1 #Hf1 #IH #f2 #n2 * -f2 -n2 /3 width=6 by gr_fcla_push, gr_fcla_next, ex4_2_intro, gr_sor_isi_dx/
-#f2 #n2 #Hf2 elim (IH … Hf2) -IH -Hf2 -Hf1 [2,4: #f #n <nplus_succ_dx ] (**) (* full auto fails *)
+#f2 #n2 #Hf2 elim (IH … Hf2) -IH -Hf2 -Hf1 [2,4: #f #n <nplus_succ_dx ] (* * full auto fails *)
 [ /3 width=7 by gr_fcla_next, gr_sor_push_next, nle_max_sn_succ_dx, nle_succ_bi, ex4_2_intro/
 | /4 width=7 by gr_fcla_next, gr_sor_next_bi, nle_succ_dx, nle_succ_bi, ex4_2_intro/
 | /3 width=7 by gr_fcla_push, gr_sor_push_bi, ex4_2_intro/
@@ -37,7 +37,7 @@ lemma gr_sor_fcla_bi:
 ]
 qed-.
 
-(* Forward lemmas with finite colength **************************************)
+(* Destructions with gr_fcla ************************************************)
 
 (*** sor_fcla *)
 lemma gr_sor_inv_fcla_bi:
@@ -47,7 +47,7 @@ lemma gr_sor_inv_fcla_bi:
 /4 width=6 by gr_sor_mono, gr_fcla_eq_repl_back, ex3_intro/
 qed-.
 
-(* Forward lemmas with finite colength **************************************)
+(* Destructions with gr_fcla ************************************************)
 
 (*** sor_fwd_fcla_sn_ex *)
 lemma gr_sor_des_fcla_sn:
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor_isf.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor_isf.ma
index 9dd3e7f9e..f059bfffa 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor_isf.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor_isf.ma
@@ -15,9 +15,9 @@
 include "ground/relocation/gr_isf_eq.ma".
 include "ground/relocation/gr_sor_fcla.ma".
 
-(* RELATIONAL UNION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL UNION FOR GENERIC RELOCATION MAPS *****************************)
 
-(* Properties with test for finite colength *********************************)
+(* Constructions with gr_isf ************************************************)
 
 (*** sor_isfin_ex *)
 lemma gr_sor_isf_bi:
@@ -26,7 +26,7 @@ lemma gr_sor_isf_bi:
 /3 width=4 by ex2_intro, ex_intro/
 qed-.
 
-(* Forward lemmas with test for finite colength *****************************)
+(* Destructions with gr_isf *************************************************)
 
 (*** sor_fwd_isfin_sn *)
 lemma gr_sor_des_isf_sn:
@@ -42,7 +42,7 @@ lemma gr_sor_des_isf_dx:
 elim (gr_sor_des_fcla_dx … Hf … H) -f -f1 /2 width=2 by ex_intro/
 qed-.
 
-(* Inversion lemmas with test for finite colength ***************************)
+(* Inversions with gr_isf ***************************************************)
 
 (*** sor_isfin *)
 lemma gr_sor_inv_isf_bi:
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor_isi.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor_isi.ma
index 49f431d3e..69a568a56 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor_isi.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor_isi.ma
@@ -16,9 +16,9 @@ include "ground/relocation/gr_isi_eq.ma".
 include "ground/relocation/gr_sor_eq.ma".
 include "ground/relocation/gr_sor_sor.ma".
 
-(* RELATIONAL UNION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL UNION FOR GENERIC RELOCATION MAPS *****************************)
 
-(* Properties with test for identity *****************************************)
+(* Constructions with gr_isi ************************************************)
 
 (*** sor_isid_sn *)
 corec lemma gr_sor_isi_sn:
@@ -42,7 +42,7 @@ lemma gr_sor_isi_bi_isi:
 /4 width=3 by gr_sor_eq_repl_back_dx, gr_sor_eq_repl_back_sn, gr_isi_inv_eq_repl/ qed.
 
 
-(* Forward lemmas with test for identity **********************************)
+(* Destructions with gr_isi *************************************************)
 
 (*** sor_fwd_isid1 *)
 corec lemma gr_sor_des_isi_sn:
@@ -62,7 +62,7 @@ corec lemma gr_sor_des_isi_dx:
 cases (gr_isi_inv_next … Hg … H)
 qed-.
 
-(* Inversion lemmas with test for identity **********************************)
+(* Inversions with gr_isi ***************************************************)
 
 (*** sor_isid_inv_sn *)
 lemma gr_sor_inv_isi_sn:
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor_sle.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor_sle.ma
index f3737538d..d036f6aaa 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor_sle.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor_sle.ma
@@ -15,9 +15,9 @@
 include "ground/relocation/gr_sle_sle.ma".
 include "ground/relocation/gr_sor.ma".
 
-(* RELATIONAL UNION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL UNION FOR GENERIC RELOCATION MAPS *****************************)
 
-(* Inversion lemmas with inclusion ******************************************)
+(* Inversions with gr_sle ***************************************************)
 
 (*** sor_inv_sle_sn *)
 corec lemma gr_sor_inv_sle_sn:
@@ -49,7 +49,7 @@ lemma gr_sor_inv_sle_dx_trans:
 axiom gr_sor_inv_sle_bi:
       ∀f1,f2,f. f1 ⋓ f2 ≘ f → ∀g. f1 ⊆ g → f2 ⊆ g → f ⊆ g.
 
-(* Properties with inclusion ************************************************)
+(* Constructions with gr_sle ************************************************)
 
 (*** sor_sle_dx *)
 corec lemma gr_sor_sle_dx:
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor_sor.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor_sor.ma
index 5b8375ed5..c4e037600 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor_sor.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor_sor.ma
@@ -15,9 +15,9 @@
 include "ground/relocation/gr_eq.ma".
 include "ground/relocation/gr_sor.ma".
 
-(* RELATIONAL UNION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL UNION FOR GENERIC RELOCATION MAPS *****************************)
 
-(* Main inversion lemmas ****************************************************)
+(* Main inversions **********************************************************)
 
 (*** sor_mono *)
 corec theorem gr_sor_mono:
@@ -32,7 +32,7 @@ corec theorem gr_sor_mono:
 /3 width=5 by gr_eq_push, gr_eq_next/
 qed-.
 
-(* Main properties **********************************************************)
+(* Main constructions *******************************************************)
 
 (*** sor_assoc_dx *)
 axiom gr_sor_assoc_dx:
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor_sor_sle.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor_sor_sle.ma
index a27e1a2b0..9dc8cb134 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor_sor_sle.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor_sor_sle.ma
@@ -15,9 +15,9 @@
 include "ground/relocation/gr_sle.ma".
 include "ground/relocation/gr_sor.ma".
 
-(* RELATIONAL UNION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL UNION FOR GENERIC RELOCATION MAPS *****************************)
 
-(* Main inversion lemmas with inclusion ****************************************************)
+(* Main inversions with gr_sle **********************************************)
 
 (*** monotonic_sle_sor *)
 axiom gr_sor_monotonic_sle:
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor_tls.ma
index 5c055d02e..82e447995 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor_tls.ma
@@ -15,9 +15,9 @@
 include "ground/relocation/gr_tls.ma".
 include "ground/relocation/gr_sor.ma".
 
-(* RELATIONAL UNION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL UNION FOR GENERIC RELOCATION MAPS *****************************)
 
-(* Properties with iterated tail ********************************************)
+(* Constructions with gr_tls ************************************************)
 
 (*** sor_tls *)
 lemma gr_sor_tls:
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_tl.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_tl.ma
index 9c4fa9e87..c0d15ce19 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_tl.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_tl.ma
@@ -16,7 +16,7 @@ include "ground/notation/functions/droppred_1.ma".
 include "ground/lib/stream_hdtl.ma".
 include "ground/relocation/gr_map.ma".
 
-(* TAIL FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* TAIL FOR GENERIC RELOCATION MAPS *****************************************)
 
 (*** tl *)
 definition gr_tl (f): gr_map ≝ ⫰f.
@@ -25,7 +25,7 @@ interpretation
   "tail (generic relocation maps)"
   'DropPred f = (gr_tl f).
 
-(* Basic properties *********************************************************)
+(* Basic constructions ******************************************************)
 
 (*** tl_push_rew *)
 lemma gr_tl_push (f): f = ⫱⫯f.
@@ -35,7 +35,7 @@ lemma gr_tl_push (f): f = ⫱⫯f.
 lemma gr_tl_next (f): f = ⫱↑f.
 // qed.
 
-(* Basic eliminators ********************************************************)
+(* Basic eliminations *******************************************************)
 
 (*** pn_split gr_map_split *)
 lemma gr_map_split_tl (f): ∨∨ ⫯⫱f = f | ↑⫱f = f.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_tl_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_tl_eq.ma
index d694de270..d93e7215f 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_tl_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_tl_eq.ma
@@ -15,9 +15,9 @@
 include "ground/relocation/gr_eq.ma".
 include "ground/relocation/gr_tl.ma".
 
-(* TAIL FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* TAIL FOR GENERIC RELOCATION MAPS *****************************************)
 
-(* Properties with gr_eq *)
+(* Constructions with gr_eq *************************************************)
 
 (*** eq_refl *)
 corec lemma gr_eq_refl: reflexive … gr_eq.
@@ -31,7 +31,7 @@ lemma gr_tl_eq_repl:
 #f1 #f2 * -f1 -f2 //
 qed.
 
-(* Inversion lemmas with gr_eq ***************************************************)
+(* Inversions with gr_eq ****************************************************)
 
 (*** eq_inv_gen *)
 lemma gr_eq_inv_gen (g1) (g2):
@@ -42,7 +42,7 @@ lemma gr_eq_inv_gen (g1) (g2):
 /3 width=1 by and3_intro, or_introl, or_intror/
 qed-.
 
-(* Advanced Inversion lemmas with gr_eq *)
+(* Advanced inversions with gr_eq *******************************************)
 
 (*** gr_eq_inv_px *)
 lemma gr_eq_inv_push_sn (g1) (g2):
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_tl_eq_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_tl_eq_eq.ma
index 015d05d65..3322574e1 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_tl_eq_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_tl_eq_eq.ma
@@ -14,9 +14,9 @@
 
 include "ground/relocation/gr_tl_eq.ma".
 
-(* TAIL FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* TAIL FOR GENERIC RELOCATION MAPS *****************************************)
 
-(* Main properties with gr_eq **********************************************************)
+(* Main constructions with gr_eq ********************************************)
 
 (*** eq_trans *)
 corec theorem gr_eq_trans: Transitive … gr_eq.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls.ma
index 6d2ddc203..e6134e7f9 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls.ma
@@ -16,7 +16,7 @@ include "ground/notation/functions/droppreds_2.ma".
 include "ground/lib/stream_tls.ma".
 include "ground/relocation/gr_tl.ma".
 
-(* ITERATED TAIL FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* ITERATED TAIL FOR GENERIC RELOCATION MAPS ********************************)
 
 (*** tls *)
 definition gr_tls (n) (f:gr_map) ≝ ⫰*[n]f.
@@ -25,7 +25,7 @@ interpretation
   "iterated tail (generic relocation maps)"
   'DropPreds n f = (gr_tls n f).
 
-(* Basic properties (specific) *********************************************************)
+(* Basic constructions (specific) *******************************************)
 
 (*** tls_O *)
 lemma gr_tls_zero (f): f = ⫱*[𝟎] f.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls_eq.ma
index b2d1d4667..4c6dcda00 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls_eq.ma
@@ -15,9 +15,9 @@
 include "ground/relocation/gr_tl_eq.ma".
 include "ground/relocation/gr_tls.ma".
 
-(* ITERATED TAIL FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* ITERATED TAIL FOR GENERIC RELOCATION MAPS ********************************)
 
-(* Properties with gr_eq ******************************************************)
+(* Constructions with gr_eq *************************************************)
 
 (*** tls_eq_repl *)
 lemma gr_tls_eq_repl (n):
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls_nexts_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls_nexts_eq.ma
index 874eab14f..7934c2e3a 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls_nexts_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls_nexts_eq.ma
@@ -15,9 +15,9 @@
 include "ground/relocation/gr_nexts.ma".
 include "ground/relocation/gr_tls_eq.ma".
 
-(* ITERATED TAIL FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* ITERATED TAIL FOR GENERIC RELOCATION MAPS ********************************)
 
-(* Inversion lemmas with gr_nexts and gr_eq *****************************************************)
+(* Inversions with gr_nexts and gr_eq ***************************************)
 
 (*** eq_inv_nexts_sn *)
 lemma gr_eq_inv_nexts_sn (n):
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls_pushs.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls_pushs.ma
index 7eb749d1b..bcce1e8c8 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls_pushs.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls_pushs.ma
@@ -15,9 +15,9 @@
 include "ground/relocation/gr_pushs.ma".
 include "ground/relocation/gr_tls.ma".
 
-(* ITERATED TAIL FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* ITERATED TAIL FOR GENERIC RELOCATION MAPS ********************************)
 
-(* Properties with pushs ****************************************************)
+(* Constructions with gr_pushs **********************************************)
 
 (*** tls_pushs *)
 lemma gr_tls_pushs (n) (f): f = ⫱*[n] ⫯*[n] f.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls_pushs_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls_pushs_eq.ma
index c4819414e..db5e705a3 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls_pushs_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls_pushs_eq.ma
@@ -15,9 +15,9 @@
 include "ground/relocation/gr_tls_eq.ma".
 include "ground/relocation/gr_pushs.ma".
 
-(* ITERATED TAIL FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* ITERATED TAIL FOR GENERIC RELOCATION MAPS ********************************)
 
-(* Inversion lemmas with gr_pushs and gr_eq *****************************************************)
+(* Inversions with gr_pushs and gr_eq ***************************************)
 
 (*** eq_inv_pushs_sn *)
 lemma gr_eq_inv_pushs_sn (n):
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_uni.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_uni.ma
index 5832c60d9..12a12732b 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_uni.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_uni.ma
@@ -16,7 +16,7 @@ include "ground/notation/functions/element_u_1.ma".
 include "ground/relocation/gr_nexts.ma".
 include "ground/relocation/gr_id.ma".
 
-(* UNIFORM ELEMENTS FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* UNIFORM ELEMENTS FOR GENERIC RELOCATION MAPS *****************************)
 
 (*** uni *)
 definition gr_uni (n) ≝ ↑*[n] 𝐢.
@@ -25,7 +25,7 @@ interpretation
   "uniform elements (generic relocation maps)"
   'ElementU n = (gr_uni n).
 
-(* Basic properties *********************************************************)
+(* Basic constructions ******************************************************)
 
 (*** uni_zero *)
 lemma gr_uni_zero: 𝐢 = 𝐮❨𝟎❩.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_uni_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_uni_eq.ma
index 6a538cb19..f5795585b 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_uni_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_uni_eq.ma
@@ -16,9 +16,9 @@ include "ground/arith/nat_pred_succ.ma".
 include "ground/relocation/gr_tl_eq.ma".
 include "ground/relocation/gr_uni.ma".
 
-(* UNIFORM ELEMENTS FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* UNIFORM ELEMENTS FOR GENERIC RELOCATION MAPS *****************************)
 
-(* Inversion lemmas with gr_eq ***************************************************)
+(* Inversions with gr_eq ****************************************************)
 
 (*** uni_inv_push_dx *)
 lemma gr_eq_inv_uni_push (n) (g):  𝐮❨n❩ ≡ ⫯g → ∧∧ 𝟎 = n & 𝐢 ≡ g.
@@ -44,7 +44,7 @@ qed-.
 lemma gr_eq_inv_next_uni (n) (g): ↑g ≡ 𝐮❨n❩ → ∧∧ 𝐮❨↓n❩ ≡ g & ↑↓n = n.
 /3 width=1 by gr_eq_inv_uni_next, gr_eq_sym/ qed-.
 
-(* Inversion lemmas with id and gr_eq *)
+(* Inversions with gr_id and gr_eq ******************************************)
 
 (*** uni_inv_id_dx *)
 lemma gr_eq_inv_uni_id (n): 𝐮❨n❩ ≡ 𝐢 → 𝟎 = n.
-- 
2.39.2