From bd7183da46c7cb0f389cda40955b270c03b57a4b Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 17 Mar 2013 17:43:13 +0000
Subject: [PATCH] lsubs renamed as lsubr

---
 .../lambdadelta/basic_2/computation/cprs.ma   |  2 +-
 .../basic_2/computation/cprs_cprs.ma          |  4 +-
 .../lambdadelta/basic_2/dynamic/lsubsv.ma     |  8 +--
 .../basic_2/dynamic/lsubsv_cpcs.ma            |  2 +-
 .../lambdadelta/basic_2/dynamic/snv_ltpr.ma   |  2 +-
 .../basic_2/dynamic/snv_ssta_ltpr.ma          |  2 +-
 .../basic_2/equivalence/cpcs_cpcs.ma          |  6 +-
 .../lambdadelta/basic_2/equivalence/lsubss.ma |  6 +-
 .../basic_2/equivalence/lsubss_cpcs.ma        |  2 +-
 .../basic_2/reducibility/cnf_cif.ma           |  2 +-
 .../lambdadelta/basic_2/reducibility/cpr.ma   |  4 +-
 .../basic_2/reducibility/cpr_cpr.ma           |  2 +-
 .../basic_2/reducibility/cpr_lift.ma          | 12 ++--
 .../basic_2/reducibility/ltpr_aaa.ma          |  2 +-
 .../basic_2/reducibility/tpr_tpss.ma          |  8 +--
 .../lambdadelta/basic_2/substitution/ldrop.ma |  4 +-
 .../basic_2/substitution/ldrop_sfr.ma         |  4 +-
 .../substitution/{lsubs.ma => lsubr.ma}       | 64 +++++++++----------
 .../{lsubs_sfr.ma => lsubr_sfr.ma}            | 16 ++---
 .../lambdadelta/basic_2/substitution/tps.ma   |  8 +--
 .../basic_2/substitution/tps_tps.ma           | 20 +++---
 .../lambdadelta/basic_2/unfold/delift.ma      |  6 +-
 .../lambdadelta/basic_2/unfold/delift_alt.ma  |  8 +--
 .../lambdadelta/basic_2/unfold/delift_lift.ma |  2 +-
 .../basic_2/unfold/ltpss_dx_ltpss_dx.ma       |  4 +-
 .../basic_2/unfold/ltpss_sn_ltpss_sn.ma       |  4 +-
 .../basic_2/unfold/ltpss_sn_tpss.ma           |  4 +-
 .../lambdadelta/basic_2/unfold/tpss.ma        |  6 +-
 .../lambdadelta/basic_2/unfold/tpss_alt.ma    |  8 +--
 .../lambdadelta/basic_2/web/basic_2_src.tbl   |  2 +-
 30 files changed, 112 insertions(+), 112 deletions(-)
 rename matita/matita/contribs/lambdadelta/basic_2/substitution/{lsubs.ma => lsubr.ma} (74%)
 rename matita/matita/contribs/lambdadelta/basic_2/substitution/{lsubs_sfr.ma => lsubr_sfr.ma} (84%)

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
index e20ce0559..ccfa79011 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
@@ -59,7 +59,7 @@ lemma cprs_strap2: ∀L,T1,T,T2.
 /2 width=3/ qed.
 
 (* Note: it does not hold replacing |L1| with |L2| *)
-lemma cprs_lsubs_trans: ∀L1,T1,T2. L1 ⊢ T1 ➡* T2 →
+lemma cprs_lsubr_trans: ∀L1,T1,T2. L1 ⊢ T1 ➡* T2 →
                         ∀L2. L2 ≼ [0, |L1|] L1 → L2 ⊢ T1 ➡* T2.
 /3 width=3/
 qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma
index c89fab769..75f74caad 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma
@@ -99,7 +99,7 @@ qed.
 lemma cprs_abst: ∀L,V1,V2. L ⊢ V1 ➡* V2 → ∀V,T1,T2. L.ⓛV ⊢ T1 ➡* T2 →
                  ∀a,I. L ⊢ ⓑ{a,I}V1. T1 ➡* ⓑ{a,I}V2. T2.
 #L #V1 #V2 #HV12 #V #T1 #T2 #HT12 #a #I @(cprs_ind … HV12) -V2
-[ lapply (cprs_lsubs_trans … HT12 (L.ⓛV1) ?) -HT12 /2 width=2/
+[ lapply (cprs_lsubr_trans … HT12 (L.ⓛV1) ?) -HT12 /2 width=2/
 | #V0 #V2 #_ #HV02 #IHV01
   @(cprs_trans … IHV01) -V1 /2 width=2/
 ]
@@ -146,7 +146,7 @@ lemma cprs_beta_dx: ∀L,V1,V2,W,T1,T2.
 #L #V1 #V2 #W #T1 #T2 #HV12 #HT12 #a @(cprs_ind … HT12) -T2
 [ /3 width=1/
 | -HV12 #T #T2 #_ #HT2 #IHT1
-  lapply (cpr_lsubs_trans … HT2 (L.ⓓV2) ?) -HT2 /2 width=1/ #HT2
+  lapply (cpr_lsubr_trans … HT2 (L.ⓓV2) ?) -HT2 /2 width=1/ #HT2
   @(cprs_trans … IHT1) -V1 -W -T1 /3 width=1/
 ]
 qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma
index 089dbed26..8df6fb710 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma
@@ -101,12 +101,12 @@ lemma lsubsv_fwd_lsubss: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 → h ⊢ L1 •⊑[
 #h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/ /2 width=6/
 qed-.
 
-lemma lsubsv_fwd_lsubs1: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 → L1 ≼[0, |L1|] L2.
-/3 width=3 by lsubsv_fwd_lsubss, lsubss_fwd_lsubs1/
+lemma lsubsv_fwd_lsubr1: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 → L1 ≼[0, |L1|] L2.
+/3 width=3 by lsubsv_fwd_lsubss, lsubss_fwd_lsubr1/
 qed-.
 
-lemma lsubsv_fwd_lsubs2: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 → L1 ≼[0, |L2|] L2.
-/3 width=3 by lsubsv_fwd_lsubss, lsubss_fwd_lsubs2/
+lemma lsubsv_fwd_lsubr2: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 → L1 ≼[0, |L2|] L2.
+/3 width=3 by lsubsv_fwd_lsubss, lsubss_fwd_lsubr2/
 qed-.
 
 (* Basic properties *********************************************************)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpcs.ma
index 15acdc943..750c71fdc 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpcs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpcs.ma
@@ -21,5 +21,5 @@ include "basic_2/dynamic/lsubsv.ma".
 
 lemma lsubsv_cpcs_trans: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 →
                          ∀T1,T2. L2 ⊢ T1 ⬌* T2 → L1 ⊢ T1 ⬌* T2.
-/3 width=5 by lsubsv_fwd_lsubs2, cpcs_lsubs_trans/
+/3 width=5 by lsubsv_fwd_lsubr2, cpcs_lsubr_trans/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma
index 79ca41081..17ae5d326 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma
@@ -41,7 +41,7 @@ fact snv_ltpr_tpr_aux: ∀h,g,L0,T0.
   elim (snv_inv_bind … H1) -H1 #HV1 #HT1
   elim (tpr_inv_bind1 … H2) -H2 *
   [ #V2 #T0 #T2 #HV12 #HT10 #HT02 #H destruct
-    lapply (tps_lsubs_trans … HT02 (L2.ⓑ{I}V2) ?) -HT02 /2 width=1/ #HT02
+    lapply (tps_lsubr_trans … HT02 (L2.ⓑ{I}V2) ?) -HT02 /2 width=1/ #HT02
     lapply (IH1 … HL12 … HV12) // [ /2 width=1/ ] #HV2
     lapply (snv_ltpr_cpr_aux … HT1  (L2.ⓑ{I}V2) … T2 ?) -HT1
     [ /3 width=5 by cpr_intro, tps_tpss/ | /2 width=1/ | /3 width=1/ ] -IH1 -T0 /2 width=1/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta_ltpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta_ltpr.ma
index 1cd5ead77..d7a40613e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta_ltpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta_ltpr.ma
@@ -57,7 +57,7 @@ fact ssta_ltpr_tpr_aux: ∀h,g,L0,T0.
   elim (ssta_inv_bind1 … H2) -H2 #U1 #HTU1 #H destruct
   elim (tpr_inv_bind1 … H3) -H3 *
   [ #V2 #T0 #T2 #HV12 #HT10 #HT02 #H destruct
-    lapply (tps_lsubs_trans … HT02 (L2.ⓑ{I}V2) ?) -HT02 [ /2 width=1/ ] #HT02
+    lapply (tps_lsubr_trans … HT02 (L2.ⓑ{I}V2) ?) -HT02 [ /2 width=1/ ] #HT02
     elim (ssta_ltpr_cpr_aux … HT1 … HTU1 (L2.ⓑ{I}V2) … T2) -HT1 -HTU1
     [2: /3 width=5 by cpr_intro, tps_tpss/ |3: /2 width=1/ |4: /3 width=1/ ] -IH1 -T0 -HL12 #U2 #HTU2 #HU12
     lapply (cpcs_bind2 … V1 … HU12 … a) -HU12 [ /2 width=1/ ] -HV12 /3 width=3/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma
index a31853a7f..cbc1ea3da 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma
@@ -154,7 +154,7 @@ lemma cpcs_beta_dx: ∀a,L,V1,V2,W,T1,T2.
 #a #L #V1 #V2 #W #T1 #T2 #HV12 #HT12
 elim (cpcs_inv_cprs … HT12) -HT12 #T #HT1 #HT2
 lapply (cprs_beta_dx … HV12 HT1 a) -HV12 -HT1 #HT1
-lapply (cprs_lsubs_trans … HT2 (L.ⓓV2) ?) -HT2 /2 width=1/ #HT2
+lapply (cprs_lsubr_trans … HT2 (L.ⓓV2) ?) -HT2 /2 width=1/ #HT2
 @(cprs_div … HT1) /2 width=1/
 qed.
 
@@ -164,11 +164,11 @@ lemma cpcs_beta_dx_tpr_rev: ∀a,L,V1,V2,W,T1,T2.
 /4 width=1/ qed.
 
 (* Note: it does not hold replacing |L1| with |L2| *)
-lemma cpcs_lsubs_trans: ∀L1,T1,T2. L1 ⊢ T1 ⬌* T2 →
+lemma cpcs_lsubr_trans: ∀L1,T1,T2. L1 ⊢ T1 ⬌* T2 →
                         ∀L2. L2 ≼ [0, |L1|] L1 → L2 ⊢ T1 ⬌* T2.
 #L1 #T1 #T2 #HT12
 elim (cpcs_inv_cprs … HT12) -HT12
-/3 width=5 by cprs_div, cprs_lsubs_trans/ (**) (* /3 width=5/ is a bit slow *)
+/3 width=5 by cprs_div, cprs_lsubr_trans/ (**) (* /3 width=5/ is a bit slow *)
 qed.
 
 (* Basic_1: was: pc3_lift *)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/lsubss.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/lsubss.ma
index 5898d4ecf..ac8f5373c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/lsubss.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/lsubss.ma
@@ -94,11 +94,11 @@ lemma lsubss_inv_pair2: ∀h,g,I,L1,K2,W2. h ⊢ L1 •⊑[g] K2. ⓑ{I} W2 →
 
 (* Basic_forward lemmas *****************************************************)
 
-lemma lsubss_fwd_lsubs1: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → L1 ≼[0, |L1|] L2.
+lemma lsubss_fwd_lsubr1: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → L1 ≼[0, |L1|] L2.
 #h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
 qed-.
 
-lemma lsubss_fwd_lsubs2: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → L1 ≼[0, |L2|] L2.
+lemma lsubss_fwd_lsubr2: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → L1 ≼[0, |L2|] L2.
 #h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
 qed-.
 
@@ -110,5 +110,5 @@ qed.
 
 lemma lsubss_cprs_trans: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 →
                          ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2.
-/3 width=5 by lsubss_fwd_lsubs2, cprs_lsubs_trans/
+/3 width=5 by lsubss_fwd_lsubr2, cprs_lsubr_trans/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/lsubss_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/lsubss_cpcs.ma
index cfb7372a4..cbddc65e9 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/lsubss_cpcs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/lsubss_cpcs.ma
@@ -21,5 +21,5 @@ include "basic_2/equivalence/lsubss.ma".
 
 lemma lsubss_cpcs_trans: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 →
                          ∀T1,T2. L2 ⊢ T1 ⬌* T2 → L1 ⊢ T1 ⬌* T2.
-/3 width=5 by lsubss_fwd_lsubs2, cpcs_lsubs_trans/
+/3 width=5 by lsubss_fwd_lsubr2, cpcs_lsubr_trans/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cnf_cif.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cnf_cif.ma
index 8ee507cc1..5a1ae5a5b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cnf_cif.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cnf_cif.ma
@@ -50,7 +50,7 @@ lemma tpr_cif_eq: ∀T1,T2. T1 ➡ T2 → ∀L. L ⊢ 𝐈⦃T1⦄ → T1 = T2.
   elim (cif_inv_appl … H) -H #_ #_ #H
   elim (simple_inv_bind … H)
 | #a * #V1 #V2 #T1 #T #T2 #_ #_ #HT2 #IHV1 #IHT1 #L #H
-  [ lapply (tps_lsubs_trans … HT2 (L.ⓓV2) ?) -HT2 /2 width=1/ #HT2
+  [ lapply (tps_lsubr_trans … HT2 (L.ⓓV2) ?) -HT2 /2 width=1/ #HT2
     elim (cif_inv_bind … H) -H #HV1 #HT1 * #H destruct
     lapply (IHV1 … HV1) -IHV1 -HV1 #H destruct
     lapply (IHT1 … HT1) -IHT1 #H destruct
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr.ma
index 56e10d392..2317250cc 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr.ma
@@ -54,10 +54,10 @@ qed.
 
 (* Note: it does not hold replacing |L1| with |L2| *)
 (* Basic_1: was only: pr2_change *)
-lemma cpr_lsubs_trans: ∀L1,T1,T2. L1 ⊢ T1 ➡ T2 →
+lemma cpr_lsubr_trans: ∀L1,T1,T2. L1 ⊢ T1 ➡ T2 →
                        ∀L2. L2 ≼ [0, |L1|] L1 → L2 ⊢ T1 ➡ T2.
 #L1 #T1 #T2 * #T #HT1 #HT2 #L2 #HL12
-lapply (tpss_lsubs_trans … HT2 … HL12) -HT2 -HL12 /3 width=4/
+lapply (tpss_lsubr_trans … HT2 … HL12) -HT2 -HL12 /3 width=4/
 qed.
 
 (* Basic inversion lemmas ***************************************************)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_cpr.ma
index d0738e4c4..039dc29e0 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_cpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_cpr.ma
@@ -30,7 +30,7 @@ lemma cpr_bind_dx: ∀a,I,L,V1,V2,T1,T2. V1 ➡ V2 → L. ⓑ{I} V2 ⊢ T1 ➡ T
                    L ⊢ ⓑ{a,I} V1. T1 ➡ ⓑ{a,I} V2. T2.
 #a #I #L #V1 #V2 #T1 #T2 #HV12 * #T #HT1 normalize #HT2
 elim (tpss_split_up … HT2 1 ? ?) -HT2 // #T0 <minus_n_O #HT0 normalize <minus_plus_m_m #HT02
-lapply (tpss_lsubs_trans … HT0 (⋆. ⓑ{I} V2) ?) -HT0 /2 width=1/ #HT0
+lapply (tpss_lsubr_trans … HT0 (⋆. ⓑ{I} V2) ?) -HT0 /2 width=1/ #HT0
 lapply (tpss_inv_SO2 … HT0) -HT0 #HT0
 @ex2_intro [2: @(tpr_delta … HV12 HT1 HT0) | skip | /2 width=1/ ] (**) (* /3 width=5/ is too slow *)
 qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_lift.ma
index b59a3e6ed..5206f43ce 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_lift.ma
@@ -32,7 +32,7 @@ lemma cpr_abst: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀V,T1,T2. L.ⓛV ⊢ T1 ➡ T2
                           ∀a,I. L ⊢ ⓑ{a,I}V1. T1 ➡ ⓑ{a,I}V2. T2.
 #L #V1 #V2 * #V0 #HV10 #HV02 #V #T1 #T2 * #T0 #HT10 #HT02 #a #I
 lapply (tpss_inv_S2 … HT02 L V ?) -HT02 // #HT02
-lapply (tpss_lsubs_trans … HT02 (L.ⓑ{I}V2) ?) -HT02 /2 width=1/ #HT02
+lapply (tpss_lsubr_trans … HT02 (L.ⓑ{I}V2) ?) -HT02 /2 width=1/ #HT02
 @(ex2_intro … (ⓑ{a,I}V0.T0)) /2 width=1/ (* explicit constructors *)
 qed.
 
@@ -40,7 +40,7 @@ lemma cpr_beta: ∀a,L,V1,V2,W,T1,T2.
                 L ⊢ V1 ➡ V2 → L.ⓛW ⊢ T1 ➡ T2 → L ⊢ ⓐV1.ⓛ{a}W.T1 ➡ ⓓ{a}V2.T2.
 #a #L #V1 #V2 #W #T1 #T2 * #V #HV1 #HV2 * #T #HT1 #HT2
 lapply (tpss_inv_S2 … HT2 L W ?) -HT2 // #HT2
-lapply (tpss_lsubs_trans … HT2 (L.ⓓV2) ?) -HT2 /2 width=1/ #HT2
+lapply (tpss_lsubr_trans … HT2 (L.ⓓV2) ?) -HT2 /2 width=1/ #HT2
 @(ex2_intro … (ⓓ{a}V.T)) /2 width=1/ (**) (* explicit constructor, /3/ is too slow *)
 qed.
 
@@ -74,9 +74,9 @@ lemma cpr_inv_abbr1: ∀a,L,V1,T1,U2. L ⊢ ⓓ{a}V1. T1 ➡ U2 →
 elim (tpr_inv_abbr1 … H1) -H1 *
 [ #V #T #T0 #HV1 #HT1 #HT0 #H destruct
   elim (tpss_inv_bind1 … H2) -H2 #V2 #T2 #HV2 #HT02 #H destruct
-  lapply (tps_lsubs_trans … HT0 (L. ⓓV) ?) -HT0 /2 width=1/ #HT0
+  lapply (tps_lsubr_trans … HT0 (L. ⓓV) ?) -HT0 /2 width=1/ #HT0
   lapply (tps_weak_all … HT0) -HT0 #HT0
-  lapply (tpss_lsubs_trans … HT02 (L. ⓓV) ?) -HT02 /2 width=1/ #HT02
+  lapply (tpss_lsubr_trans … HT02 (L. ⓓV) ?) -HT02 /2 width=1/ #HT02
   lapply (tpss_weak_all … HT02) -HT02 #HT02
   lapply (tpss_strap2 … HT0 HT02) -T0 /4 width=7/
 | #T2 #HT12 #HXT2 #H destruct
@@ -92,7 +92,7 @@ lemma cpr_inv_abst1: ∀a,L,V1,T1,U2. L ⊢ ⓛ{a}V1. T1 ➡ U2 → ∀I,W.
 #a #L #V1 #T1 #Y * #X #H1 #H2 #I #W
 elim (tpr_inv_abst1 … H1) -H1 #V #T #HV1 #HT1 #H destruct
 elim (tpss_inv_bind1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H destruct
-lapply (tpss_lsubs_trans … HT2 (L. ⓑ{I} W) ?) -HT2 /2 width=1/ /4 width=5/
+lapply (tpss_lsubr_trans … HT2 (L. ⓑ{I} W) ?) -HT2 /2 width=1/ /4 width=5/
 qed-.
 
 (* Basic_1: was pr2_gen_appl *)
@@ -143,7 +143,7 @@ lemma cpr_fwd_abst1: ∀a,L,V1,T1,U2. L ⊢ ⓛ{a}V1.T1 ➡ U2 → ∀b,I,W.
 #a #L #V1 #T1 #U2 * #U #H #HU2 #b #I #W
 elim (tpr_fwd_abst1 … H b I W) -H #V #T #HT1 #H destruct
 elim (tpss_inv_bind1 … HU2) -HU2 #V2 #T2 #_ #HT2
-lapply (tpss_lsubs_trans … HT2 (L.ⓑ{I}W) ?) -HT2 /2 width=1/ /4 width=5/
+lapply (tpss_lsubr_trans … HT2 (L.ⓑ{I}W) ?) -HT2 /2 width=1/ /4 width=5/
 qed-.
 
 (* Relocation properties ****************************************************)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_aaa.ma
index a8b117fec..5208a6405 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_aaa.ma
@@ -38,7 +38,7 @@ lemma aaa_ltpr_tpr_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → ∀L2. L1 ➡ L2 →
 | elim (aaa_inv_abbr … H1) -H1 #B #HB #HA
   elim (tpr_inv_abbr1 … H2) -H2 *
   [ #V2 #T #T2 #HV12 #HT1 #HT2 #H destruct
-    lapply (tps_lsubs_trans … HT2 (L2.ⓓV2) ?) -HT2 /2 width=1/ #HT2
+    lapply (tps_lsubr_trans … HT2 (L2.ⓓV2) ?) -HT2 /2 width=1/ #HT2
     lapply (IH … HB … HL12 … HV12) -HB /width=5/ #HB
     lapply (IH … HA … (L2.ⓓV2) … HT1) -IH -HA -HT1 /width=5/ -T1 /2 width=1/ -L1 -V1 /3 width=5/
   | -B #T #HT1 #HXT #H destruct
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpss.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpss.ma
index ff5cfb6a1..597fe64eb 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpss.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpss.ma
@@ -36,16 +36,16 @@ lemma tpr_tps_ltpr: ∀T1,T2. T1 ➡ T2 →
   elim (tps_inv_bind1 … HY) -HY #WW #TT1 #_ #HTT1 #H destruct
   elim (IHV12 … HVV1 … HL12) -V1 #VV2 #HVV12 #HVV2
   elim (IHT12 … HTT1 (L2. ⓛWW) ?) -T1 /2 width=1/ -HL12 #TT2 #HTT12 #HTT2
-  lapply (tpss_lsubs_trans … HTT2 (L2. ⓓVV2) ?) -HTT2 /3 width=5/
+  lapply (tpss_lsubr_trans … HTT2 (L2. ⓓVV2) ?) -HTT2 /3 width=5/
 | #a #I #V1 #V2 #T1 #T #T2 #HV12 #_ #HT2 #IHV12 #IHT1 #L1 #d #e #X #H #L2 #HL12
   elim (tps_inv_bind1 … H) -H #W1 #U1 #HVW1 #HTU1 #H destruct
   elim (IHV12 … HVW1 … HL12) -V1 #W2 #HW12 #HVW2
   elim (IHT1 … HTU1 (L2. ⓑ{I} W2) ?) -T1 /2 width=1/ -HL12 #U #HU1 #HTU
   elim (tpss_strip_neq … HTU … HT2 ?) -T /2 width=1/ #U2 #HU2 #HTU2
-  lapply (tps_lsubs_trans … HU2 (L2. ⓑ{I} V2) ?) -HU2 /2 width=1/ #HU2
+  lapply (tps_lsubr_trans … HU2 (L2. ⓑ{I} V2) ?) -HU2 /2 width=1/ #HU2
   elim (ltpss_dx_tps_conf … HU2 (L2. ⓑ{I} W2) (d + 1) e ?) -HU2 /2 width=1/ #U3 #HU3 #HU23
-  lapply (tps_lsubs_trans … HU3 (⋆. ⓑ{I} W2) ?) -HU3 /2 width=1/ #HU3
-  lapply (tpss_lsubs_trans … HU23 (L2. ⓑ{I} W2) ?) -HU23 /2 width=1/ #HU23
+  lapply (tps_lsubr_trans … HU3 (⋆. ⓑ{I} W2) ?) -HU3 /2 width=1/ #HU3
+  lapply (tpss_lsubr_trans … HU23 (L2. ⓑ{I} W2) ?) -HU23 /2 width=1/ #HU23
   lapply (tpss_trans_eq … HTU2 … HU23) -U2 /3 width=5/
 | #a #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #L1 #d #e #X #H #L2 #HL12
   elim (tps_inv_flat1 … H) -H #VV1 #Y #HVV1 #HY #HX destruct
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop.ma
index 87d83b347..7e7ac3c54 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop.ma
@@ -14,7 +14,7 @@
 
 include "basic_2/grammar/cl_weight.ma".
 include "basic_2/substitution/lift.ma".
-include "basic_2/substitution/lsubs.ma".
+include "basic_2/substitution/lsubr.ma".
 
 (* LOCAL ENVIRONMENT SLICING ************************************************)
 
@@ -186,7 +186,7 @@ lemma ldrop_O1_lt: ∀L,i. i < |L| → ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V.
 ]
 qed.
 
-lemma ldrop_lsubs_ldrop2_abbr: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
+lemma ldrop_lsubr_ldrop2_abbr: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
                                ∀K2,V,i. ⇩[0, i] L2 ≡ K2. ⓓV →
                                d ≤ i → i < d + e →
                                ∃∃K1. K1 ≼ [0, d + e - i - 1] K2 &
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_sfr.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_sfr.ma
index 83c157a5a..9d4cc3108 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_sfr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_sfr.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/substitution/lsubs_sfr.ma".
+include "basic_2/substitution/lsubr_sfr.ma".
 include "basic_2/substitution/ldrop_ldrop.ma".
 
 (* DROPPING *****************************************************************)
@@ -30,7 +30,7 @@ lemma sfr_inv_ldrop: ∀I,L,K,V,i. ⇩[0, i] L ≡ K. ⓑ{I}V → ∀d,e. ≽ [d
   [ -IHL #H1 #H2 #d #e #HL #Hdi #Hide destruct
     lapply (le_n_O_to_eq … Hdi) -Hdi #H destruct
     lapply (HL … (L.ⓓW) ?) -HL /2 width=1/ #H
-    elim (lsubs_inv_abbr2 … H ?) -H // -Hide #K #_ #H destruct //
+    elim (lsubr_inv_abbr2 … H ?) -H // -Hide #K #_ #H destruct //
   | #Hi #HLK #d @(nat_ind_plus … d) -d
     [ #e #H #_ #Hide
       elim (sfr_inv_bind … H ?) -H [2: /2 width=2/ ] #HL #H destruct
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubs.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr.ma
similarity index 74%
rename from matita/matita/contribs/lambdadelta/basic_2/substitution/lsubs.ma
rename to matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr.ma
index 1c0756c37..2a4e43271 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr.ma
@@ -16,59 +16,59 @@ include "basic_2/grammar/lenv_length.ma".
 
 (* LOCAL ENVIRONMENT REFINEMENT FOR SUBSTITUTION ****************************)
 
-inductive lsubs: nat → nat → relation lenv ≝
-| lsubs_sort: ∀d,e. lsubs d e (⋆) (⋆)
-| lsubs_OO:   ∀L1,L2. lsubs 0 0 L1 L2
-| lsubs_abbr: ∀L1,L2,V,e. lsubs 0 e L1 L2 →
-              lsubs 0 (e + 1) (L1. ⓓV) (L2.ⓓV)
-| lsubs_abst: ∀L1,L2,I,V1,V2,e. lsubs 0 e L1 L2 →
-              lsubs 0 (e + 1) (L1. ⓑ{I}V1) (L2. ⓛV2)
-| lsubs_skip: ∀L1,L2,I1,I2,V1,V2,d,e.
-              lsubs d e L1 L2 → lsubs (d + 1) e (L1. ⓑ{I1} V1) (L2. ⓑ{I2} V2)
+inductive lsubr: nat → nat → relation lenv ≝
+| lsubr_sort: ∀d,e. lsubr d e (⋆) (⋆)
+| lsubr_OO:   ∀L1,L2. lsubr 0 0 L1 L2
+| lsubr_abbr: ∀L1,L2,V,e. lsubr 0 e L1 L2 →
+              lsubr 0 (e + 1) (L1. ⓓV) (L2.ⓓV)
+| lsubr_abst: ∀L1,L2,I,V1,V2,e. lsubr 0 e L1 L2 →
+              lsubr 0 (e + 1) (L1. ⓑ{I}V1) (L2. ⓛV2)
+| lsubr_skip: ∀L1,L2,I1,I2,V1,V2,d,e.
+              lsubr d e L1 L2 → lsubr (d + 1) e (L1. ⓑ{I1} V1) (L2. ⓑ{I2} V2)
 .
 
 interpretation
   "local environment refinement (substitution)"
-  'SubEq L1 d e L2 = (lsubs d e L1 L2).
+  'SubEq L1 d e L2 = (lsubr d e L1 L2).
 
-definition lsubs_trans: ∀S. (lenv → relation S) → Prop ≝ λS,R.
+definition lsubr_trans: ∀S. (lenv → relation S) → Prop ≝ λS,R.
                         ∀L2,s1,s2. R L2 s1 s2 →
                         ∀L1,d,e. L1 ≼ [d, e] L2 → R L1 s1 s2.
 
 (* Basic properties *********************************************************)
 
-lemma lsubs_bind_eq: ∀L1,L2,e. L1 ≼ [0, e] L2 → ∀I,V.
+lemma lsubr_bind_eq: ∀L1,L2,e. L1 ≼ [0, e] L2 → ∀I,V.
                      L1. ⓑ{I} V ≼ [0, e + 1] L2.ⓑ{I} V.
 #L1 #L2 #e #HL12 #I #V elim I -I /2 width=1/
 qed.
 
-lemma lsubs_abbr_lt: ∀L1,L2,V,e. L1 ≼ [0, e - 1] L2 → 0 < e →
+lemma lsubr_abbr_lt: ∀L1,L2,V,e. L1 ≼ [0, e - 1] L2 → 0 < e →
                      L1. ⓓV ≼ [0, e] L2.ⓓV.
 #L1 #L2 #V #e #HL12 #He >(plus_minus_m_m e 1) // /2 width=1/
 qed.
 
-lemma lsubs_abst_lt: ∀L1,L2,I,V1,V2,e. L1 ≼ [0, e - 1] L2 → 0 < e →
+lemma lsubr_abst_lt: ∀L1,L2,I,V1,V2,e. L1 ≼ [0, e - 1] L2 → 0 < e →
                      L1. ⓑ{I}V1 ≼ [0, e] L2. ⓛV2.
 #L1 #L2 #I #V1 #V2 #e #HL12 #He >(plus_minus_m_m e 1) // /2 width=1/
 qed.
 
-lemma lsubs_skip_lt: ∀L1,L2,d,e. L1 ≼ [d - 1, e] L2 → 0 < d →
+lemma lsubr_skip_lt: ∀L1,L2,d,e. L1 ≼ [d - 1, e] L2 → 0 < d →
                      ∀I1,I2,V1,V2. L1. ⓑ{I1} V1 ≼ [d, e] L2. ⓑ{I2} V2.
 #L1 #L2 #d #e #HL12 #Hd >(plus_minus_m_m d 1) // /2 width=1/
 qed.
 
-lemma lsubs_bind_lt: ∀I,L1,L2,V,e. L1 ≼ [0, e - 1] L2 → 0 < e →
+lemma lsubr_bind_lt: ∀I,L1,L2,V,e. L1 ≼ [0, e - 1] L2 → 0 < e →
                      L1. ⓓV ≼ [0, e] L2. ⓑ{I}V.
 * /2 width=1/ qed.
 
-lemma lsubs_refl: ∀d,e,L. L ≼ [d, e] L.
+lemma lsubr_refl: ∀d,e,L. L ≼ [d, e] L.
 #d elim d -d
 [ #e elim e -e // #e #IHe #L elim L -L // /2 width=1/
 | #d #IHd #e #L elim L -L // /2 width=1/
 ]
 qed.
 
-lemma TC_lsubs_trans: ∀S,R. lsubs_trans S R → lsubs_trans S (λL. (TC … (R L))).
+lemma TC_lsubr_trans: ∀S,R. lsubr_trans S R → lsubr_trans S (λL. (TC … (R L))).
 #S #R #HR #L1 #s1 #s2 #H elim H -s2
 [ /3 width=5/
 | #s #s2 #_ #Hs2 #IHs1 #L2 #d #e #HL12
@@ -78,7 +78,7 @@ qed.
 
 (* Basic inversion lemmas ***************************************************)
 
-fact lsubs_inv_atom1_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 → L1 = ⋆ →
+fact lsubr_inv_atom1_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 → L1 = ⋆ →
                           L2 = ⋆ ∨ (d = 0 ∧ e = 0).
 #L1 #L2 #d #e * -L1 -L2 -d -e
 [ /2 width=1/
@@ -89,11 +89,11 @@ fact lsubs_inv_atom1_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 → L1 = ⋆ →
 ]
 qed.
 
-lemma lsubs_inv_atom1: ∀L2,d,e. ⋆ ≼ [d, e] L2 →
+lemma lsubr_inv_atom1: ∀L2,d,e. ⋆ ≼ [d, e] L2 →
                        L2 = ⋆ ∨ (d = 0 ∧ e = 0).
 /2 width=3/ qed-.
 
-fact lsubs_inv_skip1_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
+fact lsubr_inv_skip1_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
                           ∀I1,K1,V1. L1 = K1.ⓑ{I1}V1 → 0 < d →
                           ∃∃I2,K2,V2. K1 ≼ [d - 1, e] K2 & L2 = K2.ⓑ{I2}V2.
 #L1 #L2 #d #e * -L1 -L2 -d -e
@@ -108,11 +108,11 @@ fact lsubs_inv_skip1_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
 ]
 qed.
 
-lemma lsubs_inv_skip1: ∀I1,K1,L2,V1,d,e. K1.ⓑ{I1}V1 ≼ [d, e] L2 → 0 < d →
+lemma lsubr_inv_skip1: ∀I1,K1,L2,V1,d,e. K1.ⓑ{I1}V1 ≼ [d, e] L2 → 0 < d →
                        ∃∃I2,K2,V2. K1 ≼ [d - 1, e] K2 & L2 = K2.ⓑ{I2}V2.
 /2 width=5/ qed-.
 
-fact lsubs_inv_atom2_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 → L2 = ⋆ →
+fact lsubr_inv_atom2_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 → L2 = ⋆ →
                           L1 = ⋆ ∨ (d = 0 ∧ e = 0).
 #L1 #L2 #d #e * -L1 -L2 -d -e
 [ /2 width=1/
@@ -123,11 +123,11 @@ fact lsubs_inv_atom2_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 → L2 = ⋆ →
 ]
 qed.
 
-lemma lsubs_inv_atom2: ∀L1,d,e. L1 ≼ [d, e] ⋆ →
+lemma lsubr_inv_atom2: ∀L1,d,e. L1 ≼ [d, e] ⋆ →
                        L1 = ⋆ ∨ (d = 0 ∧ e = 0).
 /2 width=3/ qed-.
 
-fact lsubs_inv_abbr2_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
+fact lsubr_inv_abbr2_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
                           ∀K2,V. L2 = K2.ⓓV → d = 0 → 0 < e →
                           ∃∃K1. K1 ≼ [0, e - 1] K2 & L1 = K1.ⓓV.
 #L1 #L2 #d #e * -L1 -L2 -d -e
@@ -140,11 +140,11 @@ fact lsubs_inv_abbr2_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
 ]
 qed.
 
-lemma lsubs_inv_abbr2: ∀L1,K2,V,e. L1 ≼ [0, e] K2.ⓓV → 0 < e →
+lemma lsubr_inv_abbr2: ∀L1,K2,V,e. L1 ≼ [0, e] K2.ⓓV → 0 < e →
                        ∃∃K1. K1 ≼ [0, e - 1] K2 & L1 = K1.ⓓV.
 /2 width=5/ qed-.
 
-fact lsubs_inv_skip2_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
+fact lsubr_inv_skip2_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
                           ∀I2,K2,V2. L2 = K2.ⓑ{I2}V2 → 0 < d →
                           ∃∃I1,K1,V1. K1 ≼ [d - 1, e] K2 & L1 = K1.ⓑ{I1}V1.
 #L1 #L2 #d #e * -L1 -L2 -d -e
@@ -159,13 +159,13 @@ fact lsubs_inv_skip2_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
 ]
 qed.
 
-lemma lsubs_inv_skip2: ∀I2,L1,K2,V2,d,e. L1 ≼ [d, e] K2.ⓑ{I2}V2 → 0 < d →
+lemma lsubr_inv_skip2: ∀I2,L1,K2,V2,d,e. L1 ≼ [d, e] K2.ⓑ{I2}V2 → 0 < d →
                        ∃∃I1,K1,V1. K1 ≼ [d - 1, e] K2 & L1 = K1.ⓑ{I1}V1.
 /2 width=5/ qed-.
 
 (* Basic forward lemmas *****************************************************)
 
-fact lsubs_fwd_length_full1_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
+fact lsubr_fwd_length_full1_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
                                  d = 0 → e = |L1| → |L1| ≤ |L2|.
 #L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize
 [ //
@@ -176,10 +176,10 @@ fact lsubs_fwd_length_full1_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
 ]
 qed.
 
-lemma lsubs_fwd_length_full1: ∀L1,L2. L1 ≼ [0, |L1|] L2 → |L1| ≤ |L2|.
+lemma lsubr_fwd_length_full1: ∀L1,L2. L1 ≼ [0, |L1|] L2 → |L1| ≤ |L2|.
 /2 width=5/ qed-.
 
-fact lsubs_fwd_length_full2_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
+fact lsubr_fwd_length_full2_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
                                  d = 0 → e = |L2| → |L2| ≤ |L1|.
 #L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize
 [ //
@@ -190,5 +190,5 @@ fact lsubs_fwd_length_full2_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
 ]
 qed.
 
-lemma lsubs_fwd_length_full2: ∀L1,L2. L1 ≼ [0, |L2|] L2 → |L2| ≤ |L1|.
+lemma lsubr_fwd_length_full2: ∀L1,L2. L1 ≼ [0, |L2|] L2 → |L2| ≤ |L1|.
 /2 width=5/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubs_sfr.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr_sfr.ma
similarity index 84%
rename from matita/matita/contribs/lambdadelta/basic_2/substitution/lsubs_sfr.ma
rename to matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr_sfr.ma
index b71f25e51..e35a371bc 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubs_sfr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr_sfr.ma
@@ -12,13 +12,13 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/substitution/lsubs.ma".
+include "basic_2/substitution/lsubr.ma".
 
 (* LOCAL ENVIRONMENT REFINEMENT FOR SUBSTITUTION ****************************)
 
 (* bottom element of the refinement *)
 definition sfr: nat → nat → predicate lenv ≝
-   λd,e. NF_sn … (lsubs d e) (lsubs d e …).
+   λd,e. NF_sn … (lsubr d e) (lsubr d e …).
 
 interpretation
    "local environment full refinement (substitution)"
@@ -28,7 +28,7 @@ interpretation
 
 lemma sfr_atom: ∀d,e. ≽ [d, e] ⋆.
 #d #e #L #H
-elim (lsubs_inv_atom2 … H) -H
+elim (lsubr_inv_atom2 … H) -H
 [ #H destruct //
 | * #H1 #H2 destruct //
 ]
@@ -39,7 +39,7 @@ lemma sfr_OO: ∀L. ≽ [0, 0] L.
 
 lemma sfr_abbr: ∀L,V,e. ≽ [0, e] L → ≽ [0, e + 1] L.ⓓV.
 #L #V #e #HL #K #H
-elim (lsubs_inv_abbr2 … H ?) -H // <minus_plus_m_m #X #HLX #H destruct
+elim (lsubr_inv_abbr2 … H ?) -H // <minus_plus_m_m #X #HLX #H destruct
 lapply (HL … HLX) -HL -HLX /2 width=1/
 qed.
 
@@ -50,7 +50,7 @@ qed.
 
 lemma sfr_skip: ∀I,L,V,d,e. ≽ [d, e] L → ≽ [d + 1, e] L.ⓑ{I}V.
 #I #L #V #d #e #HL #K #H
-elim (lsubs_inv_skip2 … H ?) -H // <minus_plus_m_m #J #X #W #HLX #H destruct
+elim (lsubr_inv_skip2 … H ?) -H // <minus_plus_m_m #J #X #W #HLX #H destruct
 lapply (HL … HLX) -HL -HLX /2 width=1/
 qed.
 
@@ -60,14 +60,14 @@ lemma sfr_inv_bind: ∀I,L,V,e. ≽ [0, e] L.ⓑ{I}V → 0 < e →
                     ≽ [0, e - 1] L ∧ I = Abbr.
 #I #L #V #e #HL #He
 lapply (HL (L.ⓓV) ?) /2 width=1/ #H
-elim (lsubs_inv_abbr2 … H ?) -H // #K #_ #H destruct
+elim (lsubr_inv_abbr2 … H ?) -H // #K #_ #H destruct
 @conj // #L #HKL
 lapply (HL (L.ⓓV) ?) -HL /2 width=1/ -HKL #H
-elim (lsubs_inv_abbr2 … H ?) -H // -He #X #HLX #H destruct //
+elim (lsubr_inv_abbr2 … H ?) -H // -He #X #HLX #H destruct //
 qed-.
 
 lemma sfr_inv_skip: ∀I,L,V,d,e. ≽ [d, e] L.ⓑ{I}V → 0 < d → ≽ [d - 1, e] L.
 #I #L #V #d #e #HL #Hd #K #HLK
 lapply (HL (K.ⓑ{I}V) ?) -HL /2 width=1/ -HLK #H
-elim (lsubs_inv_skip2 … H ?) -H // -Hd #J #X #W #HKX #H destruct //
+elim (lsubr_inv_skip2 … H ?) -H // -Hd #J #X #W #HKX #H destruct //
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma
index 2efd00298..ebce56c24 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma
@@ -33,12 +33,12 @@ interpretation "parallel substritution (term)"
 
 (* Basic properties *********************************************************)
 
-lemma tps_lsubs_trans: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶ [d, e] T2 →
+lemma tps_lsubr_trans: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶ [d, e] T2 →
                        ∀L2. L2 ≼ [d, e] L1 → L2 ⊢ T1 ▶ [d, e] T2.
 #L1 #T1 #T2 #d #e #H elim H -L1 -T1 -T2 -d -e
 [ //
 | #L1 #K1 #V #W #i #d #e #Hdi #Hide #HLK1 #HVW #L2 #HL12
-  elim (ldrop_lsubs_ldrop2_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /2 width=4/
+  elim (ldrop_lsubr_ldrop2_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /2 width=4/
 | /4 width=1/
 | /3 width=1/
 ]
@@ -113,7 +113,7 @@ lemma tps_split_up: ∀L,T1,T2,d,e. L ⊢ T1 ▶ [d, e] T2 → ∀i. d ≤ i →
   elim (IHV12 i ? ?) -IHV12 // #V #HV1 #HV2
   elim (IHT12 (i + 1) ? ?) -IHT12 /2 width=1/
   -Hdi -Hide >arith_c1x #T #HT1 #HT2
-  lapply (tps_lsubs_trans … HT1 (L. ⓑ{I} V) ?) -HT1 /3 width=5/
+  lapply (tps_lsubr_trans … HT1 (L. ⓑ{I} V) ?) -HT1 /3 width=5/
 | #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #i #Hdi #Hide
   elim (IHV12 i ? ?) -IHV12 // elim (IHT12 i ? ?) -IHT12 //
   -Hdi -Hide /3 width=5/
@@ -136,7 +136,7 @@ lemma tps_split_down: ∀L,T1,T2,d,e. L ⊢ T1 ▶ [d, e] T2 →
   elim (IHV12 i ? ?) -IHV12 // #V #HV1 #HV2
   elim (IHT12 (i + 1) ? ?) -IHT12 /2 width=1/
   -Hdi -Hide >arith_c1x #T #HT1 #HT2
-  lapply (tps_lsubs_trans … HT1 (L. ⓑ{I} V) ?) -HT1 /3 width=5/
+  lapply (tps_lsubr_trans … HT1 (L. ⓑ{I} V) ?) -HT1 /3 width=5/
 | #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #i #Hdi #Hide
   elim (IHV12 i ? ?) -IHV12 // elim (IHT12 i ? ?) -IHT12 //
   -Hdi -Hide /3 width=5/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/tps_tps.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/tps_tps.ma
index a99b352ab..7e146c21e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/tps_tps.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/tps_tps.ma
@@ -33,11 +33,11 @@ theorem tps_conf_eq: ∀L,T0,T1,d1,e1. L ⊢ T0 ▶ [d1, e1] T1 →
   ]
 | #L #a #I #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #X #d2 #e2 #HX
   elim (tps_inv_bind1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct
-  lapply (tps_lsubs_trans … HT02 (L. ⓑ{I} V1) ?) -HT02 /2 width=1/ #HT02
+  lapply (tps_lsubr_trans … HT02 (L. ⓑ{I} V1) ?) -HT02 /2 width=1/ #HT02
   elim (IHV01 … HV02) -V0 #V #HV1 #HV2
   elim (IHT01 … HT02) -T0 #T #HT1 #HT2
-  lapply (tps_lsubs_trans … HT1 (L. ⓑ{I} V) ?) -HT1 /2 width=1/
-  lapply (tps_lsubs_trans … HT2 (L. ⓑ{I} V) ?) -HT2 /3 width=5/
+  lapply (tps_lsubr_trans … HT1 (L. ⓑ{I} V) ?) -HT1 /2 width=1/
+  lapply (tps_lsubr_trans … HT2 (L. ⓑ{I} V) ?) -HT2 /3 width=5/
 | #L #I #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #X #d2 #e2 #HX
   elim (tps_inv_flat1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct
   elim (IHV01 … HV02) -V0
@@ -71,8 +71,8 @@ theorem tps_conf_neq: ∀L1,T0,T1,d1,e1. L1 ⊢ T0 ▶ [d1, e1] T1 →
   elim (IHV01 … HV02 H) -V0 #V #HV1 #HV2
   elim (IHT01 … HT02 ?) -T0
   [ -H #T #HT1 #HT2
-    lapply (tps_lsubs_trans … HT1 (L2. ⓑ{I} V) ?) -HT1 /2 width=1/
-    lapply (tps_lsubs_trans … HT2 (L1. ⓑ{I} V) ?) -HT2 /2 width=1/ /3 width=5/
+    lapply (tps_lsubr_trans … HT1 (L2. ⓑ{I} V) ?) -HT1 /2 width=1/
+    lapply (tps_lsubr_trans … HT2 (L1. ⓑ{I} V) ?) -HT2 /2 width=1/ /3 width=5/
   | -HV1 -HV2 >plus_plus_comm_23 >plus_plus_comm_23 in ⊢ (? ? %); elim H -H #H
     [ @or_introl | @or_intror ] /2 by monotonic_le_plus_l/ (**) (* /3 / is too slow *)
   ]
@@ -100,9 +100,9 @@ theorem tps_trans_ge: ∀L,T1,T0,d,e. L ⊢ T1 ▶ [d, e] T0 →
   <(tps_inv_lift1_eq … HVT2 … HVW) -HVT2 /2 width=4/
 | #L #a #I #V1 #V0 #T1 #T0 #d #e #_ #_ #IHV10 #IHT10 #X #H #He
   elim (tps_inv_bind1 … H) -H #V2 #T2 #HV02 #HT02 #H destruct
-  lapply (tps_lsubs_trans … HT02 (L. ⓑ{I} V0) ?) -HT02 /2 width=1/ #HT02
+  lapply (tps_lsubr_trans … HT02 (L. ⓑ{I} V0) ?) -HT02 /2 width=1/ #HT02
   lapply (IHT10 … HT02 He) -T0 #HT12
-  lapply (tps_lsubs_trans … HT12 (L. ⓑ{I} V2) ?) -HT12 /2 width=1/ /3 width=1/
+  lapply (tps_lsubr_trans … HT12 (L. ⓑ{I} V2) ?) -HT12 /2 width=1/ /3 width=1/
 | #L #I #V1 #V0 #T1 #T0 #d #e #_ #_ #IHV10 #IHT10 #X #H #He
   elim (tps_inv_flat1 … H) -H #V2 #T2 #HV02 #HT02 #H destruct /3 width=1/
 ]
@@ -119,11 +119,11 @@ theorem tps_trans_down: ∀L,T1,T0,d1,e1. L ⊢ T1 ▶ [d1, e1] T0 →
   <(tps_inv_lift1_eq … HWT2 … HVW) -HWT2 /3 width=8/
 | #L #a #I #V1 #V0 #T1 #T0 #d1 #e1 #_ #_ #IHV10 #IHT10 #X #d2 #e2 #HX #de2d1
   elim (tps_inv_bind1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct
-  lapply (tps_lsubs_trans … HT02 (L. ⓑ{I} V0) ?) -HT02 /2 width=1/ #HT02
+  lapply (tps_lsubr_trans … HT02 (L. ⓑ{I} V0) ?) -HT02 /2 width=1/ #HT02
   elim (IHV10 … HV02 ?) -IHV10 -HV02 // #V
   elim (IHT10 … HT02 ?) -T0 /2 width=1/ #T #HT1 #HT2
-  lapply (tps_lsubs_trans … HT1 (L. ⓑ{I} V) ?) -HT1 /2 width=1/
-  lapply (tps_lsubs_trans … HT2 (L. ⓑ{I} V2) ?) -HT2 /2 width=1/ /3 width=6/
+  lapply (tps_lsubr_trans … HT1 (L. ⓑ{I} V) ?) -HT1 /2 width=1/
+  lapply (tps_lsubr_trans … HT2 (L. ⓑ{I} V2) ?) -HT2 /2 width=1/ /3 width=6/
 | #L #I #V1 #V0 #T1 #T0 #d1 #e1 #_ #_ #IHV10 #IHT10 #X #d2 #e2 #HX #de2d1
   elim (tps_inv_flat1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct
   elim (IHV10 … HV02 ?) -V0 //
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/delift.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/delift.ma
index cde529122..e0c736440 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/delift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/delift.ma
@@ -31,7 +31,7 @@ lemma lift_delift: ∀T1,T2,d,e. ⇧[d, e] T1 ≡ T2 →
 lemma delift_refl_O2: ∀L,T,d. L ⊢ ▼*[d, 0] T ≡ T.
 /2 width=3/ qed.
 
-lemma delift_lsubs_trans: ∀L1,T1,T2,d,e. L1 ⊢ ▼*[d, e] T1 ≡ T2 →
+lemma delift_lsubr_trans: ∀L1,T1,T2,d,e. L1 ⊢ ▼*[d, e] T1 ≡ T2 →
                           ∀L2. L2 ≼ [d, e] L1 → L2 ⊢ ▼*[d, e] T1 ≡ T2.
 #L1 #T1 #T2 #d #e * /3 width=3/
 qed.
@@ -52,7 +52,7 @@ lemma delift_bind: ∀a,I,L,V1,V2,T1,T2,d,e.
                    L ⊢ ▼*[d, e] V1 ≡ V2 → L. ⓑ{I} V2 ⊢ ▼*[d+1, e] T1 ≡ T2 →
                    L ⊢ ▼*[d, e] ⓑ{a,I} V1. T1 ≡ ⓑ{a,I} V2. T2.
 #a #I #L #V1 #V2 #T1 #T2 #d #e * #V #HV1 #HV2 * #T #HT1 #HT2
-lapply (tpss_lsubs_trans … HT1 (L. ⓑ{I} V) ?) -HT1 /2 width=1/ /3 width=5/
+lapply (tpss_lsubr_trans … HT1 (L. ⓑ{I} V) ?) -HT1 /2 width=1/ /3 width=5/
 qed.
 
 lemma delift_flat: ∀I,L,V1,V2,T1,T2,d,e.
@@ -82,7 +82,7 @@ lemma delift_inv_bind1: ∀a,I,L,V1,T1,U2,d,e. L ⊢ ▼*[d, e] ⓑ{a,I} V1. T1
 #a #I #L #V1 #T1 #U2 #d #e * #U #HU #HU2
 elim (tpss_inv_bind1 … HU) -HU #V #T #HV1 #HT1 #X destruct
 elim (lift_inv_bind2 … HU2) -HU2 #V2 #T2 #HV2 #HT2
-lapply (tpss_lsubs_trans … HT1 (L. ⓑ{I} V2) ?) -HT1 /2 width=1/ /3 width=5/
+lapply (tpss_lsubr_trans … HT1 (L. ⓑ{I} V2) ?) -HT1 /2 width=1/ /3 width=5/
 qed-.
 
 lemma delift_inv_flat1: ∀I,L,V1,T1,U2,d,e. L ⊢ ▼*[d, e] ⓕ{I} V1. T1 ≡ U2 →
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_alt.ma
index 1b82f79e3..10657d3c3 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_alt.ma
@@ -38,11 +38,11 @@ interpretation "inverse basic relocation (term) alternative"
 
 (* Basic properties *********************************************************)
 
-lemma delifta_lsubs_trans: ∀L1,T1,T2,d,e. L1 ⊢ ▼▼*[d, e] T1 ≡ T2 →
+lemma delifta_lsubr_trans: ∀L1,T1,T2,d,e. L1 ⊢ ▼▼*[d, e] T1 ≡ T2 →
                            ∀L2. L2 ≼ [d, e] L1 → L2 ⊢ ▼▼*[d, e] T1 ≡ T2.
 #L1 #T1 #T2 #d #e #H elim H -L1 -T1 -T2 -d -e // /2 width=1/
 [ #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
-  elim (ldrop_lsubs_ldrop2_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /3 width=6/
+  elim (ldrop_lsubr_ldrop2_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /3 width=6/
 | /4 width=1/
 | /3 width=1/
 ]
@@ -60,10 +60,10 @@ lemma delift_delifta: ∀L,T1,T2,d,e. L ⊢ ▼*[d, e] T1 ≡ T2 → L ⊢ ▼
   ]
 | * [ #a ] #I #V1 #T1 #Hn #X #d #e #H
   [ elim (delift_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
-    lapply (delift_lsubs_trans … HT12 (L.ⓑ{I}V1) ?) -HT12 /2 width=1/ #HT12
+    lapply (delift_lsubr_trans … HT12 (L.ⓑ{I}V1) ?) -HT12 /2 width=1/ #HT12
     lapply (IH … HV12) -HV12 // #HV12
     lapply (IH … HT12) -IH -HT12 /2 width=1/ #HT12
-    lapply (delifta_lsubs_trans … HT12 (L.ⓑ{I}V2) ?) -HT12 /2 width=1/
+    lapply (delifta_lsubr_trans … HT12 (L.ⓑ{I}V2) ?) -HT12 /2 width=1/
   | elim (delift_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
     lapply (IH … HV12) -HV12 //
     lapply (IH … HT12) -IH -HT12 // /2 width=1/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_lift.ma
index 7a654023a..eb3dc1f28 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_lift.ma
@@ -51,7 +51,7 @@ lemma sfr_delift: ∀L,T1,d,e. d + e ≤ |L| → ≽ [d, e] L →
 | #a #I #V1 #T1 #H #d #e #Hde #HL destruct
   elim (IH … V1 … Hde HL) // #V2 #HV12
   elim (IH (L.ⓑ{I}V1) T1 … (d+1) e ??) -IH // [2,3: /2 width=1/ ] -Hde -HL #T2 #HT12
-  lapply (delift_lsubs_trans … HT12 (L.ⓑ{I}V2) ?) -HT12 /2 width=1/ /3 width=4/
+  lapply (delift_lsubr_trans … HT12 (L.ⓑ{I}V2) ?) -HT12 /2 width=1/ /3 width=4/
 | #I #V1 #T1 #H #d #e #Hde #HL destruct
   elim (IH … V1 … Hde HL) // #V2 #HV12
   elim (IH … T1 … Hde HL) -IH -Hde -HL // /3 width=2/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_ltpss_dx.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_ltpss_dx.ma
index ab281b92b..74b898d69 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_ltpss_dx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_ltpss_dx.ma
@@ -58,10 +58,10 @@ lemma ltpss_dx_tpss_trans_eq: ∀L1,T2,U2,d,e. L1 ⊢ T2 ▶* [d, e] U2 →
   [ normalize /2 width=1/ | /2 width=6/ ]
 | * [ #a ] #I #V2 #T2 #Hn #X #d #e #H #L0 #HL0 destruct
   [ elim (tpss_inv_bind1 … H) -H #W2 #U2 #HVW2 #HTU2 #H destruct
-    lapply (tpss_lsubs_trans … HTU2 (L1. ⓑ{I} V2) ?) -HTU2 /2 width=1/ #HTU2
+    lapply (tpss_lsubr_trans … HTU2 (L1. ⓑ{I} V2) ?) -HTU2 /2 width=1/ #HTU2
     lapply (IH … HVW2 … HL0) -HVW2 [ /2 width=2/ ] #HVW2
     lapply (IH … HTU2 (L0. ⓑ{I} V2) ?) -IH -HTU2 // /2 width=2/ -HL0 #HTU2
-    lapply (tpss_lsubs_trans … HTU2 (L0. ⓑ{I} W2) ?) -HTU2 /2 width=1/
+    lapply (tpss_lsubr_trans … HTU2 (L0. ⓑ{I} W2) ?) -HTU2 /2 width=1/
   | elim (tpss_inv_flat1 … H) -H #W2 #U2 #HVW2 #HTU2 #H destruct
     lapply (IH … HVW2 … HL0) -HVW2 //
     lapply (IH … HTU2 … HL0) -IH -HTU2 // -HL0 /2 width=1/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_ltpss_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_ltpss_sn.ma
index dfcd35c73..67c287e2b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_ltpss_sn.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_ltpss_sn.ma
@@ -32,10 +32,10 @@ lemma ltpss_sn_tpss_trans_eq: ∀L1,T2,U2,d,e. L1 ⊢ T2 ▶* [d, e] U2 →
   lapply (tpss_trans_eq … HV01 HV12) -V1 /2 width=6/
 | * [ #a ] #I #V2 #T2 #Hn #X #d #e #H #L0 #HL0 destruct
   [ elim (tpss_inv_bind1 … H) -H #W2 #U2 #HVW2 #HTU2 #H destruct
-    lapply (tpss_lsubs_trans … HTU2 (L1. ⓑ{I} V2) ?) -HTU2 /2 width=1/ #HTU2
+    lapply (tpss_lsubr_trans … HTU2 (L1. ⓑ{I} V2) ?) -HTU2 /2 width=1/ #HTU2
     lapply (IH … HVW2 … HL0) -HVW2 [ /2 width=2/ ] #HVW2
     lapply (IH … HTU2 (L0. ⓑ{I} V2) ?) -IH -HTU2 // /2 width=2/ -HL0 #HTU2
-    lapply (tpss_lsubs_trans … HTU2 (L0. ⓑ{I} W2) ?) -HTU2 /2 width=1/
+    lapply (tpss_lsubr_trans … HTU2 (L0. ⓑ{I} W2) ?) -HTU2 /2 width=1/
   | elim (tpss_inv_flat1 … H) -H #W2 #U2 #HVW2 #HTU2 #H destruct
     lapply (IH … HVW2 … HL0) -HVW2 //
     lapply (IH … HTU2 … HL0) -IH -HTU2 // -HL0 /2 width=1/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_tpss.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_tpss.ma
index d23c1a255..007613cf9 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_tpss.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_tpss.ma
@@ -52,7 +52,7 @@ lemma ltpss_sn_tps_conf: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶ [d2, e2] U2 →
 | #L0 #a #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01
   elim (IHVW2 … HL01) -IHVW2 #V #HV2 #HVW2
   elim (IHTU2 (L1. ⓑ{I} V) (d1 + 1) e1 ?) -IHTU2 /2 width=1/ -HL01 #T #HT2 #H
-  lapply (tpss_lsubs_trans … H (L0.ⓑ{I}V) ?) -H /2 width=1/ /3 width=5/
+  lapply (tpss_lsubr_trans … H (L0.ⓑ{I}V) ?) -H /2 width=1/ /3 width=5/
 | #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01
   elim (IHVW2 … HL01) -IHVW2
   elim (IHTU2 … HL01) -IHTU2 -HL01 /3 width=5/
@@ -93,7 +93,7 @@ lemma ltpss_sn_tps_trans: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶ [d2, e2] U2 →
 | #L0 #a #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10
   elim (IHVW2 … HL10) -IHVW2 #V #HV2 #HVW2
   elim (IHTU2 (L1. ⓑ{I} V) (d1 + 1) e1 ?) -IHTU2 /2 width=1/ -HL10 #T #HT2 #H
-  lapply (tpss_lsubs_trans … H (L1.ⓑ{I}W2) ?) -H /2 width=1/ /3 width=5/
+  lapply (tpss_lsubr_trans … H (L1.ⓑ{I}W2) ?) -H /2 width=1/ /3 width=5/
 | #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10
   elim (IHVW2 … HL10) -IHVW2
   elim (IHTU2 … HL10) -IHTU2 -HL10 /3 width=5/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma
index ba88f64e9..d2ce11a36 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma
@@ -51,7 +51,7 @@ lemma tpss_strap2: ∀L,T1,T,T2,d,e.
                    L ⊢ T1 ▶ [d, e] T → L ⊢ T ▶* [d, e] T2 → L ⊢ T1 ▶* [d, e] T2.
 /2 width=3/ qed.
 
-lemma tpss_lsubs_trans: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶* [d, e] T2 →
+lemma tpss_lsubr_trans: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶* [d, e] T2 →
                         ∀L2. L2 ≼ [d, e] L1 → L2 ⊢ T1 ▶* [d, e] T2.
 /3 width=3/ qed.
 
@@ -67,7 +67,7 @@ lemma tpss_bind: ∀L,V1,V2,d,e. L ⊢ V1 ▶* [d, e] V2 →
   | #T #T2 #_ #HT2 #IHT @step /2 width=5/ (**) (* /3 width=5/ is too slow *)
   ]
 | #V #V2 #_ #HV12 #IHV #a #I #T1 #T2 #HT12
-  lapply (tpss_lsubs_trans … HT12 (L. ⓑ{I} V) ?) -HT12 /2 width=1/ #HT12
+  lapply (tpss_lsubr_trans … HT12 (L. ⓑ{I} V) ?) -HT12 /2 width=1/ #HT12
   lapply (IHV a … HT12) -IHV -HT12 #HT12 @step /2 width=5/ (**) (* /3 width=5/ is too slow *)
 ]
 qed.
@@ -144,7 +144,7 @@ lemma tpss_inv_bind1: ∀d,e,L,a,I,V1,T1,U2. L ⊢ ⓑ{a,I} V1. T1 ▶* [d, e] U
 [ /2 width=5/
 | #U #U2 #_ #HU2 * #V #T #HV1 #HT1 #H destruct
   elim (tps_inv_bind1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H
-  lapply (tpss_lsubs_trans … HT1 (L. ⓑ{I} V2) ?) -HT1 /2 width=1/ /3 width=5/
+  lapply (tpss_lsubr_trans … HT1 (L. ⓑ{I} V2) ?) -HT1 /2 width=1/ /3 width=5/
 ]
 qed-.
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_alt.ma
index 8f77dd0d0..8adea69bc 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_alt.ma
@@ -35,12 +35,12 @@ interpretation "parallel unfold (term) alternative"
 
 (* Basic properties *********************************************************)
 
-lemma tpssa_lsubs_trans: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶▶* [d, e] T2 →
+lemma tpssa_lsubr_trans: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶▶* [d, e] T2 →
                          ∀L2. L2 ≼ [d, e] L1 → L2 ⊢ T1 ▶▶* [d, e] T2.
 #L1 #T1 #T2 #d #e #H elim H -L1 -T1 -T2 -d -e
 [ //
 | #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
-  elim (ldrop_lsubs_ldrop2_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /3 width=6/
+  elim (ldrop_lsubr_ldrop2_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /3 width=6/
 | /4 width=1/
 | /3 width=1/
 ]
@@ -62,10 +62,10 @@ lemma tpssa_tps_trans: ∀L,T1,T,d,e. L ⊢ T1 ▶▶* [d, e] T →
   elim (tps_inv_lift1_be … H … H0LK … HVW2 ? ?) -H -H0LK -HVW2 // /3 width=6/
 | #L #a #I #V1 #V #T1 #T #d #e #_ #_ #IHV1 #IHT1 #X #H
   elim (tps_inv_bind1 … H) -H #V2 #T2 #HV2 #HT2 #H destruct
-  lapply (tps_lsubs_trans … HT2 (L.ⓑ{I}V) ?) -HT2 /2 width=1/ #HT2
+  lapply (tps_lsubr_trans … HT2 (L.ⓑ{I}V) ?) -HT2 /2 width=1/ #HT2
   lapply (IHV1 … HV2) -IHV1 -HV2 #HV12
   lapply (IHT1 … HT2) -IHT1 -HT2 #HT12
-  lapply (tpssa_lsubs_trans … HT12 (L.ⓑ{I}V2) ?) -HT12 /2 width=1/
+  lapply (tpssa_lsubr_trans … HT12 (L.ⓑ{I}V2) ?) -HT12 /2 width=1/
 | #L #I #V1 #V #T1 #T #d #e #_ #_ #IHV1 #IHT1 #X #H
   elim (tps_inv_flat1 … H) -H #V2 #T2 #HV2 #HT2 #H destruct /3 width=1/
 ]
diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
index 00db0e50b..4139f7344 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
@@ -239,7 +239,7 @@ table {
           }
         ]
         [ { "local env. ref. for substitution" * } {
-             [ "lsubs ( ? ≼[?,?] ? )" "(lsubs_lsubs)" "lsubs_sfr ( ≽[?,?] ? )" * ]
+             [ "lsubr ( ? ≼[?,?] ? )" "(lsubr_lsubr)" "lsubr_sfr ( ≽[?,?] ? )" * ]
           }
         ]
         [ { "restricted structural predecessor for closures" * } {
-- 
2.39.2