From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sat, 29 May 2021 08:40:29 +0000 (+0200)
Subject: update in ground
X-Git-Tag: make_still_working~148
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=0bcf2dc1a27e38cb6cd3d44eb838d652926841e0

update in ground

+ some renaming
---

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma
index d5d1c13fe..e4ccf83f4 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma
@@ -32,7 +32,7 @@ lemma nminus_zero_dx (m): m = m - 𝟎.
 // qed.
 
 (*** minus_SO_dx *)
-lemma nminus_one_dx (m): ↓m = m - 𝟏 .
+lemma nminus_unit_dx (m): ↓m = m - 𝟏 .
 // qed.
 
 (*** eq_minus_S_pred *)
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma
index f1dffc51d..a9894fc62 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma
@@ -31,7 +31,7 @@ lemma nplus_zero_dx (m): m = m + 𝟎.
 // qed.
 
 (*** plus_SO_dx *)
-lemma nplus_one_dx (n): ↑n = n + 𝟏.
+lemma nplus_unit_dx (n): ↑n = n + 𝟏.
 // qed.
 
 (*** plus_n_Sm *)
@@ -76,7 +76,7 @@ qed.
 (* Helper constructions *****************************************************)
 
 (*** plus_SO_sn *)
-lemma nplus_one_sn (n): ↑n = 𝟏 + n.
+lemma nplus_unit_sn (n): ↑n = 𝟏 + n.
 #n <nplus_comm // qed.
 
 lemma nplus_succ_shift (m) (n): ↑m + n = m + ↑n.
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_pred.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_pred.ma
index d7f79d76b..3367fe66a 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_pred.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_pred.ma
@@ -44,7 +44,7 @@ lemma npred_zero: 𝟎 = ↓𝟎.
 lemma npred_inj (p): ↓p = ↓(ninj p).
 // qed.
 
-lemma npred_one: 𝟎 = ↓𝟏.
+lemma npred_unit: 𝟎 = ↓𝟏.
 // qed.
 
 lemma npred_psucc (p): ninj p = ↓↑p.
@@ -54,7 +54,7 @@ lemma npred_psucc (p): ninj p = ↓↑p.
 
 lemma npred_pnat_inv_refl (p): ninj p = ↓p → ⊥.
 *
-[ <npred_one #H destruct
+[ <npred_unit #H destruct
 | #p /3 width=2 by psucc_inv_refl, eq_inv_ninj_bi/
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma
index 8096e849b..af5bd0943 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma
@@ -25,7 +25,7 @@ interpretation
 
 (* Basic constructions ******************************************************)
 
-lemma pplus_one_dx (p): ↑p = p + 𝟏.
+lemma pplus_unit_dx (p): ↑p = p + 𝟏.
 // qed.
 
 lemma pplus_succ_dx (p) (q): ↑(p+q) = p + ↑q.
@@ -37,7 +37,7 @@ lemma pplus_succ_sn (p) (q): ↑(p+q) = ↑p + q.
 #p #q @(piter_appl … psucc)
 qed.
 
-lemma pplus_one_sn (p): ↑p = 𝟏 + p.
+lemma pplus_unit_sn (p): ↑p = 𝟏 + p.
 #p elim p -p //
 qed.
 
@@ -54,7 +54,7 @@ qed.
 
 lemma eq_inv_unit_pplus (p) (q): 𝟏 = p + q → ⊥.
 #p #q elim q -q
-[ <pplus_one_dx #H destruct
+[ <pplus_unit_dx #H destruct
 | #q #_ <pplus_succ_dx #H destruct
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lminus.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lminus.ma
index 6a2e4dbee..b1dee6cef 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lminus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lminus.ma
@@ -42,7 +42,7 @@ lemma ylminus_succ_dx (x:ynat) (n): ↓(x-n) = x - ↑n.
 qed.
 
 (*** yminus_SO2 *)
-lemma ylminus_one_dx (x): ↓x = x - (𝟏).
+lemma ylminus_unit_dx (x): ↓x = x - (𝟏).
 // qed.
 
 (*** yminus_Y_inj *)
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_plus.ma
index bc75d92d1..f002081e4 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_plus.ma
@@ -47,7 +47,7 @@ lemma yplus_zero_dx (x): x = x + 𝟎.
 (* Constructions with ysucc *************************************************)
 
 (*** yplus_SO2 *)
-lemma yplus_one_dx (x): ↑x = x + 𝟏.
+lemma yplus_unit_dx (x): ↑x = x + 𝟏.
 // qed.
 
 (*** yplus_S2 yplus_succ2 *)
diff --git a/matita/matita/contribs/lambdadelta/ground/counters/rtc_ism_plus.ma b/matita/matita/contribs/lambdadelta/ground/counters/rtc_ism_plus.ma
index 5453b63fb..4451820f9 100644
--- a/matita/matita/contribs/lambdadelta/ground/counters/rtc_ism_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/counters/rtc_ism_plus.ma
@@ -33,7 +33,7 @@ lemma rtc_ism_plus_zero_dx (n) (c1) (c2): 𝐌❪n,c1❫ → 𝐌❪𝟎,c2❫ 
 /2 width=1 by rtc_ism_plus/ qed.
 
 lemma rtc_ism_succ (n) (c): 𝐌❪n,c❫ → 𝐌❪↑n,c+𝟘𝟙❫.
-#n #c #H >nplus_one_dx
+#n #c #H >nplus_unit_dx
 /2 width=1 by rtc_ism_plus/
 qed.
 
diff --git a/matita/matita/contribs/lambdadelta/ground/counters/rtc_ist_plus.ma b/matita/matita/contribs/lambdadelta/ground/counters/rtc_ist_plus.ma
index 08bb3b772..5156acb85 100644
--- a/matita/matita/contribs/lambdadelta/ground/counters/rtc_ist_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/counters/rtc_ist_plus.ma
@@ -33,7 +33,7 @@ lemma rtc_ist_plus_zero_dx (n) (c1) (c2): 𝐓❪n,c1❫ → 𝐓❪𝟎,c2❫ 
 /2 width=1 by rtc_ist_plus/ qed.
 
 lemma rtc_ist_succ (n) (c): 𝐓❪n,c❫ → 𝐓❪↑n,c+𝟘𝟙❫.
-#n #c #H >nplus_one_dx
+#n #c #H >nplus_unit_dx
 /2 width=1 by rtc_ist_plus/
 qed.
 
@@ -54,7 +54,7 @@ lemma rtc_ist_inv_plus_zero_dx (n) (c1) (c2): 𝐓❪n,c1 + c2❫ → 𝐓❪
 elim (rtc_ist_inv_plus … H) -H #n1 #n2 #Hn1 #Hn2 #H destruct //
 qed-.
 
-lemma rtc_ist_inv_plus_one_dx:
+lemma rtc_ist_inv_plus_unit_dx:
       ∀n,c1,c2. 𝐓❪n,c1 + c2❫ → 𝐓❪𝟏,c2❫ →
       ∃∃m. 𝐓❪m,c1❫ & n = ↑m.
 #n #c1 #c2 #H #H2 destruct
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 e3f8acfcd..97780f1c6 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_ist.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_ist.ma
@@ -45,7 +45,7 @@ lemma gr_after_des_ist_sn:
 qed-.
 
 (*** after_at1_fwd *)
-lemma gr_after_pat_sn_des:
+lemma gr_after_des_ist_pat:
       ∀f1,i1,i2. @❪i1, f1❫ ≘ i2 → ∀f2. 𝐓❪f2❫ → ∀f. f2 ⊚ f1 ≘ f →
       ∃∃i. @❪i2, f2❫ ≘ i & @❪i1, f❫ ≘ i.
 #f1 #i1 #i2 #Hf1 #f2 #Hf2 #f #Hf elim (Hf2 i2) -Hf2
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 93077d253..fd325b4d7 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
@@ -20,7 +20,7 @@ include "ground/relocation/gr_after_ist.ma".
 (* Forward lemmas on istot and isid **************************************************)
 
 (*** after_fwd_isid_sn *)
-lemma gr_after_des_isi_sn:
+lemma gr_after_des_ist_eq_sn:
       ∀f2,f1,f. 𝐓❪f❫ → f2 ⊚ f1 ≘ f → f1 ≡ f → 𝐈❪f2❫.
 #f2 #f1 #f #H #Hf elim (gr_after_inv_ist … Hf H) -H
 #Hf2 #Hf1 #H @gr_isi_pat_total // -Hf2
@@ -31,10 +31,10 @@ lemma gr_after_des_isi_sn:
 qed-.
 
 (*** after_fwd_isid_dx *)
-lemma gr_after_des_isi_dx:
+lemma gr_after_des_ist_eq_dx:
       ∀f2,f1,f.  𝐓❪f❫ → f2 ⊚ f1 ≘ f → f2 ≡ f → 𝐈❪f1❫.
 #f2 #f1 #f #H #Hf elim (gr_after_inv_ist … Hf H) -H
 #Hf2 #Hf1 #H2 @gr_isi_pat_total // -Hf1
-#i1 #i2 #Hi12 elim (gr_after_pat_sn_des … Hi12 … Hf) -f1
+#i1 #i2 #Hi12 elim (gr_after_des_ist_pat … Hi12 … Hf) -f1
 /3 width=8 by gr_pat_inj, gr_pat_eq_repl_back/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_nat_uni.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_nat_uni.ma
deleted file mode 100644
index 489e820f6..000000000
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_nat_uni.ma
+++ /dev/null
@@ -1,61 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "ground/relocation/gr_tls.ma".
-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 ***********************************************************)
-
-(* Properties with gr_nat and uni *)
-
-(*** after_uni_dx *)
-lemma gr_after_uni_dx (l2) (l1):
-      ∀f2. @↑❪l1, f2❫ ≘ l2 →
-      ∀f. f2 ⊚ 𝐮❨l1❩ ≘ f → 𝐮❨l2❩ ⊚ ⫱*[l2] f2 ≘ f.
-#l2 @(nat_ind_succ … l2) -l2
-[ #l1 #f2 #Hf2 #f #Hf
-  elim (gr_nat_inv_zero_dx … Hf2) -Hf2 // #g2 #H1 #H2 destruct
-  lapply (gr_after_isi_inv_dx … Hf ?) -Hf
-  /3 width=3 by gr_after_isi_sn, gr_after_eq_repl_back/
-| #l2 #IH #l1 #f2 #Hf2 #f #Hf
-  elim (gr_nat_inv_succ_dx … Hf2) -Hf2 [1,3: * |*: // ]
-  [ #g2 #k1 #Hg2 #H1 #H2 destruct
-    elim (gr_after_inv_push_next … Hf) -Hf [ |*: // ] #g #Hg #H destruct
-    <gr_tls_swap /3 width=5 by gr_after_next/
-  | #g2 #Hg2 #H2 destruct
-    elim (gr_after_inv_next_sn … Hf) -Hf [ |*: // ] #g #Hg #H destruct
-    <gr_tls_swap /3 width=5 by gr_after_next/
-  ]
-]
-qed.
-
-(*** after_uni_sn *)
-lemma gr_after_uni_sn (l2) (l1):
-      ∀f2. @↑❪l1, f2❫ ≘ l2 →
-      ∀f. 𝐮❨l2❩ ⊚ ⫱*[l2] f2 ≘ f → f2 ⊚ 𝐮❨l1❩ ≘ f.
-#l2 @(nat_ind_succ … l2) -l2
-[ #l1 #f2 #Hf2 #f #Hf
-  elim (gr_nat_inv_zero_dx … Hf2) -Hf2 // #g2 #H1 #H2 destruct
-  lapply (gr_after_isi_inv_sn … Hf ?) -Hf
-  /3 width=3 by gr_after_isi_dx, gr_after_eq_repl_back/
-| #l2 #IH #l1 #f2 #Hf2 #f #Hf
-  elim (gr_after_inv_next_sn … Hf) -Hf [2,3: // ] #g #Hg #H destruct
-  elim (gr_nat_inv_succ_dx … Hf2) -Hf2 [1,3: * |*: // ]
-  [ #g2 #k1 #Hg2 #H1 #H2 destruct /3 width=7 by gr_after_push/
-  | #g2 #Hg2 #H2 destruct /3 width=5 by gr_after_next/
-  ]
-]
-qed-.
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
new file mode 100644
index 000000000..04be0911d
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_nat_uni_tls.ma
@@ -0,0 +1,61 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "ground/relocation/gr_tls.ma".
+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 ***********************************************************)
+
+(* Properties with gr_nat and uni *)
+
+(*** after_uni_dx *)
+lemma gr_after_nat_uni (l2) (l1):
+      ∀f2. @↑❪l1, f2❫ ≘ l2 →
+      ∀f. f2 ⊚ 𝐮❨l1❩ ≘ f → 𝐮❨l2❩ ⊚ ⫱*[l2] f2 ≘ f.
+#l2 @(nat_ind_succ … l2) -l2
+[ #l1 #f2 #Hf2 #f #Hf
+  elim (gr_nat_inv_zero_dx … Hf2) -Hf2 // #g2 #H1 #H2 destruct
+  lapply (gr_after_isi_inv_dx … Hf ?) -Hf
+  /3 width=3 by gr_after_isi_sn, gr_after_eq_repl_back/
+| #l2 #IH #l1 #f2 #Hf2 #f #Hf
+  elim (gr_nat_inv_succ_dx … Hf2) -Hf2 [1,3: * |*: // ]
+  [ #g2 #k1 #Hg2 #H1 #H2 destruct
+    elim (gr_after_inv_push_next … Hf) -Hf [ |*: // ] #g #Hg #H destruct
+    <gr_tls_swap /3 width=5 by gr_after_next/
+  | #g2 #Hg2 #H2 destruct
+    elim (gr_after_inv_next_sn … Hf) -Hf [ |*: // ] #g #Hg #H destruct
+    <gr_tls_swap /3 width=5 by gr_after_next/
+  ]
+]
+qed.
+
+(*** after_uni_sn *)
+lemma gr_nat_after_uni_tls (l2) (l1):
+      ∀f2. @↑❪l1, f2❫ ≘ l2 →
+      ∀f. 𝐮❨l2❩ ⊚ ⫱*[l2] f2 ≘ f → f2 ⊚ 𝐮❨l1❩ ≘ f.
+#l2 @(nat_ind_succ … l2) -l2
+[ #l1 #f2 #Hf2 #f #Hf
+  elim (gr_nat_inv_zero_dx … Hf2) -Hf2 // #g2 #H1 #H2 destruct
+  lapply (gr_after_isi_inv_sn … Hf ?) -Hf
+  /3 width=3 by gr_after_isi_dx, gr_after_eq_repl_back/
+| #l2 #IH #l1 #f2 #Hf2 #f #Hf
+  elim (gr_after_inv_next_sn … Hf) -Hf [2,3: // ] #g #Hg #H destruct
+  elim (gr_nat_inv_succ_dx … Hf2) -Hf2 [1,3: * |*: // ]
+  [ #g2 #k1 #Hg2 #H1 #H2 destruct /3 width=7 by gr_after_push/
+  | #g2 #Hg2 #H2 destruct /3 width=5 by gr_after_next/
+  ]
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_pat_uni.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_pat_uni.ma
deleted file mode 100644
index 52765a6bb..000000000
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_pat_uni.ma
+++ /dev/null
@@ -1,79 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "ground/relocation/gr_tls.ma".
-include "ground/relocation/gr_pat.ma".
-(**) (* 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 ***********************************************************)
-
-(* Properties with pat and uni *******************************************************)
-
-(*** after_uni_succ_dx *)
-lemma gr_after_uni_dx (i2) (i1):
-      ∀f2. @❪i1, f2❫ ≘ i2 →
-      ∀f. f2 ⊚ 𝐮❨i1❩ ≘ f → 𝐮❨i2❩ ⊚ ⫱*[i2] f2 ≘ f.
-#i2 elim i2 -i2
-[ #i1 #f2 #Hf2 #f #Hf
-  elim (gr_pat_inv_unit_dx … Hf2) -Hf2 // #g2 #H1 #H2 destruct
-  elim (gr_after_inv_push_next … Hf) -Hf [ |*: // ] #g #Hg #H
-  lapply (gr_after_isi_inv_dx … Hg ?) -Hg
-  /4 width=5 by gr_after_isi_sn, gr_after_eq_repl_back, gr_after_next/
-| #i2 #IH #i1 #f2 #Hf2 #f #Hf >nsucc_inj
-  elim (gr_pat_inv_succ_dx … Hf2) -Hf2 [1,3: * |*: // ]
-  [ #g2 #j1 #Hg2 #H1 #H2 destruct >nsucc_inj in Hf; #Hf
-    elim (gr_after_inv_push_next … Hf) -Hf [ |*: // ] #g #Hg #H destruct
-    <gr_tls_swap /3 width=5 by gr_after_next/
-  | #g2 #Hg2 #H2 destruct
-    elim (gr_after_inv_next_sn … Hf) -Hf [2,3: // ] #g #Hg #H destruct
-    <gr_tls_swap /3 width=5 by gr_after_next/
-  ]
-]
-qed.
-
-(*** after_uni_succ_sn *)
-lemma gr_after_uni_sn (i2) (i1):
-      ∀f2. @❪i1, f2❫ ≘ i2 →
-      ∀f. 𝐮❨i2❩ ⊚ ⫱*[i2] f2 ≘ f → f2 ⊚ 𝐮❨i1❩ ≘ f.
-#i2 elim i2 -i2
-[ #i1 #f2 #Hf2 #f #Hf
-  elim (gr_pat_inv_unit_dx … Hf2) -Hf2 // #g2 #H1 #H2 destruct
-  elim (gr_after_inv_next_sn … Hf) -Hf [ |*: // ] #g #Hg #H destruct
-  lapply (gr_after_isi_inv_sn … Hg ?) -Hg
-  /4 width=7 by gr_after_isi_dx, gr_after_eq_repl_back, gr_after_push/
-| #i2 #IH #i1 #f2 #Hf2 #f >nsucc_inj #Hf
-  elim (gr_after_inv_next_sn … Hf) -Hf [2,3: // ] #g #Hg #H destruct
-  elim (gr_pat_inv_succ_dx … Hf2) -Hf2 [1,3: * |*: // ]
-  [ #g2 #j1 #Hg2 #H1 #H2 destruct <gr_tls_swap in Hg; /3 width=7 by gr_after_push/
-  | #g2 #Hg2 #H2 destruct <gr_tls_swap in Hg; /3 width=5 by gr_after_next/
-  ]
-]
-qed-.
-
-(* Advanced properties with uni *)
-
-(*** after_uni_one_dx *)
-lemma gr_after_uni_one_dx:
-      ∀f2,f. ⫯f2 ⊚ 𝐮❨𝟏❩ ≘ f → 𝐮❨𝟏❩ ⊚ f2 ≘ f.
-#f2 #f #H
-@(gr_after_uni_dx … (⫯f2))
-/2 width=3 by gr_pat_refl/
-qed.
-
-(*** after_uni_one_sn *)
-lemma gr_after_uni_one_sn:
-      ∀f1,f. 𝐮❨𝟏❩ ⊚ f1 ≘ f → ⫯f1 ⊚ 𝐮❨𝟏❩ ≘ f.
-/3 width=3 by gr_after_uni_sn, gr_pat_refl/ qed-.
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
new file mode 100644
index 000000000..e8104fd3e
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_pat_uni_tls.ma
@@ -0,0 +1,79 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "ground/relocation/gr_tls.ma".
+include "ground/relocation/gr_pat.ma".
+(**) (* 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 ***********************************************************)
+
+(* Properties with pat and uni and tls *******************************************************)
+
+(*** after_uni_succ_dx *)
+lemma gr_after_pat_uni (i2) (i1):
+      ∀f2. @❪i1, f2❫ ≘ i2 →
+      ∀f. f2 ⊚ 𝐮❨i1❩ ≘ f → 𝐮❨i2❩ ⊚ ⫱*[i2] f2 ≘ f.
+#i2 elim i2 -i2
+[ #i1 #f2 #Hf2 #f #Hf
+  elim (gr_pat_inv_unit_dx … Hf2) -Hf2 // #g2 #H1 #H2 destruct
+  elim (gr_after_inv_push_next … Hf) -Hf [ |*: // ] #g #Hg #H
+  lapply (gr_after_isi_inv_dx … Hg ?) -Hg
+  /4 width=5 by gr_after_isi_sn, gr_after_eq_repl_back, gr_after_next/
+| #i2 #IH #i1 #f2 #Hf2 #f #Hf >nsucc_inj
+  elim (gr_pat_inv_succ_dx … Hf2) -Hf2 [1,3: * |*: // ]
+  [ #g2 #j1 #Hg2 #H1 #H2 destruct >nsucc_inj in Hf; #Hf
+    elim (gr_after_inv_push_next … Hf) -Hf [ |*: // ] #g #Hg #H destruct
+    <gr_tls_swap /3 width=5 by gr_after_next/
+  | #g2 #Hg2 #H2 destruct
+    elim (gr_after_inv_next_sn … Hf) -Hf [2,3: // ] #g #Hg #H destruct
+    <gr_tls_swap /3 width=5 by gr_after_next/
+  ]
+]
+qed.
+
+(*** after_uni_succ_sn *)
+lemma gr_pat_after_uni_tls (i2) (i1):
+      ∀f2. @❪i1, f2❫ ≘ i2 →
+      ∀f. 𝐮❨i2❩ ⊚ ⫱*[i2] f2 ≘ f → f2 ⊚ 𝐮❨i1❩ ≘ f.
+#i2 elim i2 -i2
+[ #i1 #f2 #Hf2 #f #Hf
+  elim (gr_pat_inv_unit_dx … Hf2) -Hf2 // #g2 #H1 #H2 destruct
+  elim (gr_after_inv_next_sn … Hf) -Hf [ |*: // ] #g #Hg #H destruct
+  lapply (gr_after_isi_inv_sn … Hg ?) -Hg
+  /4 width=7 by gr_after_isi_dx, gr_after_eq_repl_back, gr_after_push/
+| #i2 #IH #i1 #f2 #Hf2 #f >nsucc_inj #Hf
+  elim (gr_after_inv_next_sn … Hf) -Hf [2,3: // ] #g #Hg #H destruct
+  elim (gr_pat_inv_succ_dx … Hf2) -Hf2 [1,3: * |*: // ]
+  [ #g2 #j1 #Hg2 #H1 #H2 destruct <gr_tls_swap in Hg; /3 width=7 by gr_after_push/
+  | #g2 #Hg2 #H2 destruct <gr_tls_swap in Hg; /3 width=5 by gr_after_next/
+  ]
+]
+qed-.
+
+(* Advanced properties with uni *)
+
+(*** after_uni_one_dx *)
+lemma gr_after_push_unit:
+      ∀f2,f. ⫯f2 ⊚ 𝐮❨𝟏❩ ≘ f → 𝐮❨𝟏❩ ⊚ f2 ≘ f.
+#f2 #f #H
+@(gr_after_pat_uni … (⫯f2))
+/2 width=3 by gr_pat_refl/
+qed.
+
+(*** after_uni_one_sn *)
+lemma gr_after_unit_sn:
+      ∀f1,f. 𝐮❨𝟏❩ ⊚ f1 ≘ f → ⫯f1 ⊚ 𝐮❨𝟏❩ ≘ f.
+/3 width=3 by gr_pat_after_uni_tls, gr_pat_refl/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
index 7078e2afc..6c57ebf67 100644
--- a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
+++ b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
@@ -34,7 +34,7 @@ table {
           [ "gr_sdj ( ? ∥ ? )" "gr_sdj_eq" "gr_sdj_isi" * ]
           [ "gr_sle ( ? ⊆ ? )" "gr_sle_eq" "gr_sle_pushs" "gr_sle_tls" "gr_sle_isi" "gr_sle_isd" "gr_sle_sle" * ]
           [ "gr_coafter ( ? ~⊚ ? ≘ ? )" "gr_coafter_eq" "gr_coafter_uni_pushs" "gr_coafter_pat_tls" "gr_coafter_nat_tls" "gr_coafter_nat_tls_pushs" "gr_coafter_isi" "gr_coafter_isu" "gr_coafter_ist_isi" "gr_coafter_ist_isf" "gr_coafter_coafter" "gr_coafter_coafter_ist" * ]
-          [ "gr_after ( ? ⊚ ? ≘ ? )" "gr_after_eq" "gr_after_uni" "gr_after_basic" "gr_after_pat" "gr_after_pat_tls" "gr_after_pat_uni" "gr_after_nat_uni" "gr_after_isi" "gr_after_isu" "gr_after_ist" "gr_after_ist_isi" "gr_after_after" "gr_after_after_ist" * ]
+          [ "gr_after ( ? ⊚ ? ≘ ? )" "gr_after_eq" "gr_after_uni" "gr_after_basic" "gr_after_pat" "gr_after_pat_tls" "gr_after_pat_uni_tls" "gr_after_nat_uni_tls" "gr_after_isi" "gr_after_isu" "gr_after_ist" "gr_after_ist_isi" "gr_after_after" "gr_after_after_ist" * ]
           [ "gr_isd ( 𝛀❪?❫ )" "gr_isd_eq" "gr_isd_tl" "gr_isd_nexts" "gr_isd_tls" * ]
           [ "gr_ist ( 𝐓❪?❫ )" "gr_ist_tls" "gr_ist_isi" "gr_ist_ist" * ]
           [ "gr_isf ( 𝐅❪?❫ )" "gr_isf_eq" "gr_isf_tl" "gr_isf_pushs" "fr_isf_tls" "gr_ifs_uni" "gr_isf_isu" * ]