From 1555848a5546d0154964286d3400114481d78962 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 20 Apr 2014 19:25:00 +0000
Subject: [PATCH] - name changes in the rediction rules - theory of extended
 substitution is active again, we hope to use it to obtain a non-recurisive
 alternative definition of llpx_sn

---
 .../lambdadelta/apps_2/functional/rtm_step.ma |  2 +-
 .../lambdadelta/basic_2/computation/cprs.ma   |  4 +-
 .../basic_2/computation/cprs_cprs.ma          |  2 +-
 .../lambdadelta/basic_2/computation/cpxs.ma   |  8 +-
 .../basic_2/computation/cpxs_cpxs.ma          |  4 +-
 .../basic_2/computation/cpxs_tstc.ma          |  2 +-
 .../lambdadelta/basic_2/computation/lsubc.ma  |  4 +-
 .../basic_2/notation/relations/lrsubeq_4.ma   |  4 +-
 .../relations/{lrsubeq_2.ma => lrsubeqc_2.ma} |  2 +-
 .../relations/lrsubeqc_4.ma}                  |  4 +-
 .../relations/psubst_6.ma}                    |  0
 .../relations/psubststar_6.ma}                |  0
 .../relations/psubststaralt_6.ma}             |  0
 .../lambdadelta/basic_2/reduction/cnr.ma      |  4 +-
 .../lambdadelta/basic_2/reduction/cnr_crr.ma  |  2 +-
 .../lambdadelta/basic_2/reduction/cnx.ma      |  6 +-
 .../lambdadelta/basic_2/reduction/cnx_crx.ma  |  2 +-
 .../lambdadelta/basic_2/reduction/cpr.ma      |  6 +-
 .../lambdadelta/basic_2/reduction/cpr_lift.ma |  4 +-
 .../lambdadelta/basic_2/reduction/cpx.ma      | 14 ++--
 .../lambdadelta/basic_2/reduction/cpx_leq.ma  |  4 +-
 .../lambdadelta/basic_2/reduction/cpx_lift.ma | 16 ++--
 .../lambdadelta/basic_2/reduction/cpx_lleq.ma |  6 +-
 .../lambdadelta/basic_2/reduction/lpr_lpr.ma  | 12 +--
 .../{etc/lsuby/cpy.etc => relocation/cpy.ma}  |  1 +
 .../cpy_cpy.etc => relocation/cpy_cpy.ma}     |  0
 .../cpy_lift.etc => relocation/cpy_lift.ma}   |  0
 .../lsuby/lsuby.etc => relocation/lsuby.ma}   | 82 +++++++++----------
 .../lsuby_lsuby.ma}                           |  0
 .../lambdadelta/basic_2/static/lsubr.ma       |  4 +-
 .../lsuby/cpys.etc => substitution/cpys.ma}   |  0
 .../cpys_alt.etc => substitution/cpys_alt.ma} |  0
 .../cpys_cpys.ma}                             |  0
 .../cpys_lift.ma}                             |  0
 .../lambdadelta/basic_2/web/basic_2_src.tbl   | 16 +++-
 35 files changed, 114 insertions(+), 101 deletions(-)
 rename matita/matita/contribs/lambdadelta/basic_2/notation/relations/{lrsubeq_2.ma => lrsubeqc_2.ma} (97%)
 rename matita/matita/contribs/lambdadelta/basic_2/{etc/lsuby/extlrsubeq_4.etc => notation/relations/lrsubeqc_4.ma} (90%)
 rename matita/matita/contribs/lambdadelta/basic_2/{etc/lsuby/psubst_6.etc => notation/relations/psubst_6.ma} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{etc/lsuby/psubststar_6.etc => notation/relations/psubststar_6.ma} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{etc/lsuby/psubststaralt_6.etc => notation/relations/psubststaralt_6.ma} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{etc/lsuby/cpy.etc => relocation/cpy.ma} (99%)
 rename matita/matita/contribs/lambdadelta/basic_2/{etc/lsuby/cpy_cpy.etc => relocation/cpy_cpy.ma} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{etc/lsuby/cpy_lift.etc => relocation/cpy_lift.ma} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{etc/lsuby/lsuby.etc => relocation/lsuby.ma} (70%)
 rename matita/matita/contribs/lambdadelta/basic_2/{etc/lsuby/lsuby_lsuby.etc => relocation/lsuby_lsuby.ma} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{etc/lsuby/cpys.etc => substitution/cpys.ma} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{etc/lsuby/cpys_alt.etc => substitution/cpys_alt.ma} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{etc/lsuby/cpys_cpys.etc => substitution/cpys_cpys.ma} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{etc/lsuby/cpys_lift.etc => substitution/cpys_lift.ma} (100%)

diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/rtm_step.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/rtm_step.ma
index 5ca6add44..e2d859b74 100644
--- a/matita/matita/contribs/lambdadelta/apps_2/functional/rtm_step.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/functional/rtm_step.ma
@@ -36,7 +36,7 @@ inductive rtm_step: relation rtm ≝
 | rtm_gtype : ∀G,V,u,E,S,p. p = |G| →
               rtm_step (mk_rtm (G. ⓛV) u E S (§p))
                        (mk_rtm G u E S V)
-| rtm_tau   : ∀G,u,E,S,W,T.
+| rtm_eps   : ∀G,u,E,S,W,T.
               rtm_step (mk_rtm G u E S (ⓝW. T))
                        (mk_rtm G u E S T)
 | rtm_appl  : ∀G,u,E,S,V,T.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
index 45c8cfe7d..e4c5460d0 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
@@ -91,9 +91,9 @@ lemma cprs_zeta: ∀G,L,V,T1,T,T2. ⇧[0, 1] T2 ≡ T →
 /3 width=3 by cprs_strap2, cpr_cprs, cpr_bind, cpr_zeta/
 qed.
 
-lemma cprs_tau: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → ∀V. ⦃G, L⦄ ⊢ ⓝV.T1 ➡* T2.
+lemma cprs_eps: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → ∀V. ⦃G, L⦄ ⊢ ⓝV.T1 ➡* T2.
 #G #L #T1 #T2 #H @(cprs_ind … H) -T2
-/3 width=3 by cprs_strap1, cpr_cprs, cpr_tau/
+/3 width=3 by cprs_strap1, cpr_cprs, cpr_eps/
 qed.
 
 lemma cprs_beta_dx: ∀a,G,L,V1,V2,W1,W2,T1,T2.
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 809bf173c..8b073c157 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma
@@ -112,7 +112,7 @@ lemma lpr_cpr_trans: ∀G. s_r_transitive … (cpr G) (λ_. lpr G).
   elim (lpr_inv_pair2 … H) -H #K1 #V1 #HK12 #HV10 #H destruct
   /4 width=6 by cprs_strap2, cprs_delta/
 |3,7: /4 width=1 by lpr_pair, cprs_bind, cprs_beta/
-|4,6: /3 width=1 by cprs_flat, cprs_tau/
+|4,6: /3 width=1 by cprs_flat, cprs_eps/
 |5,8: /4 width=3 by lpr_pair, cprs_zeta, cprs_theta, cprs_strap1/
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma
index 36ef1b2a1..8027a98db 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma
@@ -97,16 +97,16 @@ lemma cpxs_zeta: ∀h,g,G,L,V,T1,T,T2. ⇧[0, 1] T2 ≡ T →
 /3 width=3 by cpxs_strap2, cpx_cpxs, cpx_bind, cpx_zeta/
 qed.
 
-lemma cpxs_tau: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 →
+lemma cpxs_eps: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 →
                 ∀V. ⦃G, L⦄ ⊢ ⓝV.T1 ➡*[h, g] T2.
 #h #g #G #L #T1 #T2 #H @(cpxs_ind … H) -T2
-/3 width=3 by cpxs_strap1, cpx_cpxs, cpx_tau/
+/3 width=3 by cpxs_strap1, cpx_cpxs, cpx_eps/
 qed.
 
-lemma cpxs_ti: ∀h,g,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 →
+lemma cpxs_ct: ∀h,g,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 →
                ∀T. ⦃G, L⦄ ⊢ ⓝV1.T ➡*[h, g] V2.
 #h #g #G #L #V1 #V2 #H @(cpxs_ind … H) -V2
-/3 width=3 by cpxs_strap1, cpx_cpxs, cpx_ti/
+/3 width=3 by cpxs_strap1, cpx_cpxs, cpx_ct/
 qed.
 
 lemma cpxs_beta_dx: ∀h,g,a,G,L,V1,V2,W1,W2,T1,T2.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma
index fad7c97a5..b6431c294 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma
@@ -96,13 +96,13 @@ qed-.
 lemma lpx_cpx_trans: ∀h,g,G. s_r_transitive … (cpx h g G) (λ_.lpx h g G).
 #h #g #G #L2 #T1 #T2 #HT12 elim HT12 -G -L2 -T1 -T2
 [ /2 width=3 by/
-| /3 width=2 by cpx_cpxs, cpx_sort/
+| /3 width=2 by cpx_cpxs, cpx_st/
 | #I #G #L2 #K2 #V0 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV02 #L1 #HL12
   elim (lpx_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H
   elim (lpx_inv_pair2 … H) -H #K1 #V1 #HK12 #HV10 #H destruct
   /4 width=7 by cpxs_delta, cpxs_strap2/
 |4,9: /4 width=1 by cpxs_beta, cpxs_bind, lpx_pair/
-|5,7,8: /3 width=1 by cpxs_flat, cpxs_ti, cpxs_tau/
+|5,7,8: /3 width=1 by cpxs_flat, cpxs_ct, cpxs_eps/
 | /4 width=3 by cpxs_zeta, lpx_pair/
 | /4 width=3 by cpxs_theta, cpxs_strap1, lpx_pair/
 ]
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma
index eed76daea..c0a202ae5 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma
@@ -34,7 +34,7 @@ elim (cpxs_inv_sort1 … H) -H #n #l generalize in match k; -k @(nat_ind_plus 
   elim (IHn … Hnl) -IHn
   [ #H lapply (tstc_inv_atom1 … H) -H #H >H -H /2 width=1 by or_intror/
   | generalize in match Hnl; -Hnl @(nat_ind_plus … n) -n
-    /4 width=3 by cpxs_strap2, cpx_sort, or_intror/
+    /4 width=3 by cpxs_strap2, cpx_st, or_intror/
   | >iter_SO >iter_n_Sm //
   ]
 ]
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc.ma
index e43f81978..ccc102933 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/notation/relations/lrsubeq_4.ma".
+include "basic_2/notation/relations/lrsubeqc_4.ma".
 include "basic_2/static/aaa.ma".
 include "basic_2/computation/acp_cr.ma".
 
@@ -27,7 +27,7 @@ inductive lsubc (RP) (G): relation lenv ≝
 
 interpretation
   "local environment refinement (abstract candidates of reducibility)"
-  'LRSubEq RP G L1 L2 = (lsubc RP G L1 L2).
+  'LRSubEqC RP G L1 L2 = (lsubc RP G L1 L2).
 
 (* Basic inversion lemmas ***************************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeq_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeq_4.ma
index e638d21c1..f38c1f86a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeq_4.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeq_4.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( G ⊢ break term 46 L1 ⫃ break [ term 46 R ] break term 46 L2 )"
+notation "hvbox( L1 break ⊆ [ term 46 d , break term 46 e ] break term 46 L2 )"
    non associative with precedence 45
-   for @{ 'LRSubEq $R $G $L1 $L2 }.
+   for @{ 'LRSubEq $L1 $d $e $L2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeq_2.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqc_2.ma
similarity index 97%
rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeq_2.ma
rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqc_2.ma
index 1f0f64888..3a6e5eded 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeq_2.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqc_2.ma
@@ -16,4 +16,4 @@
 
 notation "hvbox( L1 ⫃ break term 46 L2 )"
    non associative with precedence 45
-   for @{ 'LRSubEq $L1 $L2 }.
+   for @{ 'LRSubEqC $L1 $L2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/extlrsubeq_4.etc b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqc_4.ma
similarity index 90%
rename from matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/extlrsubeq_4.etc
rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqc_4.ma
index 8a9714dd8..823d6bebf 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/extlrsubeq_4.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqc_4.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( L1 break ⊑ × [ term 46 d , break term 46 e ] break term 46 L2 )"
+notation "hvbox( G ⊢ break term 46 L1 ⫃ break [ term 46 R ] break term 46 L2 )"
    non associative with precedence 45
-   for @{ 'ExtLRSubEq $L1 $d $e $L2 }.
+   for @{ 'LRSubEqC $R $G $L1 $L2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/psubst_6.etc b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubst_6.ma
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/psubst_6.etc
rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubst_6.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/psubststar_6.etc b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubststar_6.ma
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/psubststar_6.etc
rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubststar_6.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/psubststaralt_6.etc b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubststaralt_6.ma
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/psubststaralt_6.etc
rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubststaralt_6.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr.ma
index e0e84742f..d68be1680 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr.ma
@@ -69,9 +69,9 @@ lemma cnr_inv_appl: ∀G,L,V,T. ⦃G, L⦄ ⊢ ➡ 𝐍⦃ⓐV.T⦄ → ∧∧ 
 ]
 qed-.
 
-lemma cnr_inv_tau: ∀G,L,V,T. ⦃G, L⦄ ⊢ ➡ 𝐍⦃ⓝV.T⦄ → ⊥.
+lemma cnr_inv_eps: ∀G,L,V,T. ⦃G, L⦄ ⊢ ➡ 𝐍⦃ⓝV.T⦄ → ⊥.
 #G #L #V #T #H lapply (H T ?) -H
-/2 width=4 by cpr_tau, discr_tpair_xy_y/
+/2 width=4 by cpr_eps, discr_tpair_xy_y/
 qed-.
 
 (* Basic properties *********************************************************)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_crr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_crr.ma
index 35937fb41..e1d75cd04 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_crr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_crr.ma
@@ -30,7 +30,7 @@ lemma cnr_inv_crr: ∀G,L,T. ⦃G, L⦄ ⊢ ➡ 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ 
   elim (cnr_inv_appl … H) -H /2 width=1/
 | #I #L #V #T * #H1 #H2 destruct
   [ elim (cnr_inv_zeta … H2)
-  | elim (cnr_inv_tau … H2)
+  | elim (cnr_inv_eps … H2)
   ]
 |5,6: #a * [ elim a ] #L #V #T * #H1 #_ #IH #H2 destruct
   [1,3: elim (cnr_inv_abbr … H2) -H2 /2 width=1/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma
index 983e2ac36..a464e95be 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma
@@ -30,7 +30,7 @@ interpretation
 lemma cnx_inv_sort: ∀h,g,G,L,k. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃⋆k⦄ → deg h g k 0.
 #h #g #G #L #k #H elim (deg_total h g k)
 #l @(nat_ind_plus … l) -l // #l #_ #Hkl
-lapply (H (⋆(next h k)) ?) -H /2 width=2 by cpx_sort/ -L -l #H destruct -H -e0 (**) (* destruct does not remove some premises *)
+lapply (H (⋆(next h k)) ?) -H /2 width=2 by cpx_st/ -L -l #H destruct -H -e0 (**) (* destruct does not remove some premises *)
 lapply (next_lt h k) >e1 -e1 #H elim (lt_refl_false … H)
 qed-.
 
@@ -82,9 +82,9 @@ lemma cnx_inv_appl: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃ⓐV.T⦄ 
 ]
 qed-.
 
-lemma cnx_inv_tau: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃ⓝV.T⦄ → ⊥.
+lemma cnx_inv_eps: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃ⓝV.T⦄ → ⊥.
 #h #g #G #L #V #T #H lapply (H T ?) -H
-/2 width=4 by cpx_tau, discr_tpair_xy_y/
+/2 width=4 by cpx_eps, discr_tpair_xy_y/
 qed-.
 
 (* Basic forward lemmas *****************************************************)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_crx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_crx.ma
index db2da4fb8..c4948b776 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_crx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_crx.ma
@@ -33,7 +33,7 @@ lemma cnx_inv_crx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃T⦄ → ⦃G,
   elim (cnx_inv_appl … H) -H /2 width=1 by/
 | #I #L #V #T * #H1 #H2 destruct
   [ elim (cnx_inv_zeta … H2)
-  | elim (cnx_inv_tau … H2)
+  | elim (cnx_inv_eps … H2)
   ]
 |6,7: #a * [ elim a ] #L #V #T * #H1 #_ #IH #H2 destruct
   [1,3: elim (cnx_inv_abbr … H2) -H2 /2 width=1 by/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma
index c68911d4f..bbb13d14e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma
@@ -34,7 +34,7 @@ inductive cpr: relation4 genv lenv term term ≝
              cpr G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
 | cpr_zeta : ∀G,L,V,T1,T,T2. cpr G (L.ⓓV) T1 T →
              ⇧[0, 1] T2 ≡ T → cpr G L (+ⓓV.T1) T2
-| cpr_tau  : ∀G,L,V,T1,T2. cpr G L T1 T2 → cpr G L (ⓝV.T1) T2
+| cpr_eps  : ∀G,L,V,T1,T2. cpr G L T1 T2 → cpr G L (ⓝV.T1) T2
 | cpr_beta : ∀a,G,L,V1,V2,W1,W2,T1,T2.
              cpr G L V1 V2 → cpr G L W1 W2 → cpr G (L.ⓛW1) T1 T2 →
              cpr G L (ⓐV1.ⓛ{a}W1.T1) (ⓓ{a}ⓝW2.V2.T2)
@@ -55,7 +55,7 @@ lemma lsubr_cpr_trans: ∀G. lsub_trans … (cpr G) lsubr.
   elim (lsubr_fwd_ldrop2_abbr … HL12 … HLK1) -L1 *
   /3 width=6 by cpr_delta/
 |3,7: /4 width=1 by lsubr_bind, cpr_bind, cpr_beta/
-|4,6: /3 width=1 by cpr_flat, cpr_tau/
+|4,6: /3 width=1 by cpr_flat, cpr_eps/
 |5,8: /4 width=3 by lsubr_bind, cpr_zeta, cpr_theta/
 ]
 qed-.
@@ -290,6 +290,6 @@ qed-.
             pr2_gen_ctail pr2_ctail
 *)
 (* Basic_1: removed local theorems 4:
-            pr0_delta_tau pr0_cong_delta
+            pr0_delta_eps pr0_cong_delta
             pr2_free_free pr2_free_delta
 *)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_lift.ma
index 101e2b029..36c349e4e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_lift.ma
@@ -43,7 +43,7 @@ lemma cpr_lift: ∀G. l_liftable (cpr G).
   elim (lift_inv_bind1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct
   elim (lift_conf_O1 … HTU2 … HT2) -T2 /4 width=6 by cpr_zeta, ldrop_skip/
 | #G #K #V #T1 #T2 #_ #IHT12 #L #s #d #e #HLK #U1 #H #U2 #HTU2
-  elim (lift_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct /3 width=6 by cpr_tau/
+  elim (lift_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct /3 width=6 by cpr_eps/
 | #a #G #K #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L #s #d #e #HLK #X1 #HX1 #X2 #HX2
   elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct
   elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct
@@ -91,7 +91,7 @@ lemma cpr_inv_lift1: ∀G. l_deliftable_sn (cpr G).
   elim (lift_div_le … HU2 … HTU) -U /3 width=6 by cpr_zeta, ex2_intro/
 | #G #L #V #U1 #U2 #_ #IHU12 #K #s #d #e #HLK #X #H
   elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
-  elim (IHU12 … HLK … HTU1) -L -U1 /3 width=3 by cpr_tau, ex2_intro/
+  elim (IHU12 … HLK … HTU1) -L -U1 /3 width=3 by cpr_eps, ex2_intro/
 | #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #K #s #d #e #HLK #X #HX
   elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct
   elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma
index 9fd1ccf48..edfc74f5b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma
@@ -21,7 +21,7 @@ include "basic_2/reduction/cpr.ma".
 (* avtivate genv *)
 inductive cpx (h) (g): relation4 genv lenv term term ≝
 | cpx_atom : ∀I,G,L. cpx h g G L (⓪{I}) (⓪{I})
-| cpx_sort : ∀G,L,k,l. deg h g k (l+1) → cpx h g G L (⋆k) (⋆(next h k))
+| cpx_st   : ∀G,L,k,l. deg h g k (l+1) → cpx h g G L (⋆k) (⋆(next h k))
 | cpx_delta: ∀I,G,L,K,V,V2,W2,i.
              ⇩[i] L ≡ K.ⓑ{I}V → cpx h g G K V V2 →
              ⇧[0, i+1] V2 ≡ W2 → cpx h g G L (#i) W2
@@ -33,8 +33,8 @@ inductive cpx (h) (g): relation4 genv lenv term term ≝
              cpx h g G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
 | cpx_zeta : ∀G,L,V,T1,T,T2. cpx h g G (L.ⓓV) T1 T →
              ⇧[0, 1] T2 ≡ T → cpx h g G L (+ⓓV.T1) T2
-| cpx_tau  : ∀G,L,V,T1,T2. cpx h g G L T1 T2 → cpx h g G L (ⓝV.T1) T2
-| cpx_ti   : ∀G,L,V1,V2,T. cpx h g G L V1 V2 → cpx h g G L (ⓝV1.T) V2
+| cpx_eps  : ∀G,L,V,T1,T2. cpx h g G L T1 T2 → cpx h g G L (ⓝV.T1) T2
+| cpx_ct   : ∀G,L,V1,V2,T. cpx h g G L V1 V2 → cpx h g G L (ⓝV1.T) V2
 | cpx_beta : ∀a,G,L,V1,V2,W1,W2,T1,T2.
              cpx h g G L V1 V2 → cpx h g G L W1 W2 → cpx h g G (L.ⓛW1) T1 T2 →
              cpx h g G L (ⓐV1.ⓛ{a}W1.T1) (ⓓ{a}ⓝW2.V2.T2)
@@ -53,12 +53,12 @@ interpretation
 lemma lsubr_cpx_trans: ∀h,g,G. lsub_trans … (cpx h g G) lsubr.
 #h #g #G #L1 #T1 #T2 #H elim H -G -L1 -T1 -T2
 [ //
-| /2 width=2 by cpx_sort/
+| /2 width=2 by cpx_st/
 | #I #G #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
   elim (lsubr_fwd_ldrop2_bind … HL12 … HLK1) -HL12 -HLK1 *
-  /4 width=7 by cpx_delta, cpx_ti/
+  /4 width=7 by cpx_delta, cpx_ct/
 |4,9: /4 width=1 by cpx_bind, cpx_beta, lsubr_bind/
-|5,7,8: /3 width=1 by cpx_flat, cpx_tau, cpx_ti/
+|5,7,8: /3 width=1 by cpx_flat, cpx_eps, cpx_ct/
 |6,10: /4 width=3 by cpx_zeta, cpx_theta, lsubr_bind/
 ]
 qed-.
@@ -70,7 +70,7 @@ qed.
 
 lemma cpr_cpx: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ⦃G, L⦄ ⊢ T1 ➡[h, g] T2.
 #h #g #G #L #T1 #T2 #H elim H -L -T1 -T2
-/2 width=7 by cpx_delta, cpx_bind, cpx_flat, cpx_zeta, cpx_tau, cpx_beta, cpx_theta/
+/2 width=7 by cpx_delta, cpx_bind, cpx_flat, cpx_zeta, cpx_eps, cpx_beta, cpx_theta/
 qed.
 
 lemma cpx_pair_sn: ∀h,g,I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡[h, g] V2 →
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_leq.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_leq.ma
index 7d86e027d..cbc336500 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_leq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_leq.ma
@@ -22,11 +22,11 @@ include "basic_2/reduction/cpx.ma".
 lemma leq_cpx_trans: ∀h,g,G. lsub_trans … (cpx h g G) (leq 0 (∞)).
 #h #g #G #L1 #T1 #T2 #H elim H -G -L1 -T1 -T2
 [ //
-| /2 width=2 by cpx_sort/
+| /2 width=2 by cpx_st/
 | #I #G #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
   elim (leq_ldrop_trans_be … HL12 … HLK1) // -HL12 -HLK1 /3 width=7 by cpx_delta/
 |4,9: /4 width=1 by cpx_bind, cpx_beta, leq_pair_O_Y/
-|5,7,8: /3 width=1 by cpx_flat, cpx_tau, cpx_ti/
+|5,7,8: /3 width=1 by cpx_flat, cpx_eps, cpx_ct/
 |6,10: /4 width=3 by cpx_zeta, cpx_theta, leq_pair_O_Y/
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma
index 87cfd3ca3..1cd6da260 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma
@@ -24,7 +24,7 @@ include "basic_2/reduction/cpx.ma".
 lemma ssta_cpx: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 •[h, g] T2 →
                 ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T1 ➡[h, g] T2.
 #h #g #G #L #T1 #T2 #l #H elim H -G -L -T1 -T2
-[ /3 width=4 by cpx_sort, da_inv_sort/
+[ /3 width=4 by cpx_st, da_inv_sort/
 | #G #L #K #V #U #W #i #HLK #_ #HWU #IHVW #H
   elim (da_inv_lref … H) -H * #K0 #V0 [| #l0 ] #HLK0
   lapply (ldrop_mono … HLK0 … HLK) -HLK0 #H destruct /3 width=7 by cpx_delta/
@@ -33,7 +33,7 @@ lemma ssta_cpx: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 •[h, g] T2 →
   lapply (ldrop_mono … HLK0 … HLK) -HLK0 #H destruct /2 width=7 by cpx_delta/
 | /4 width=2 by cpx_bind, da_inv_bind/
 | /4 width=3 by cpx_flat, da_inv_flat/
-| /4 width=3 by cpx_tau, da_inv_flat/
+| /4 width=3 by cpx_eps, da_inv_flat/
 ]
 qed.
 
@@ -45,7 +45,7 @@ lemma cpx_lift: ∀h,g,G. l_liftable (cpx h g G).
   >(lift_mono … H1 … H2) -H1 -H2 //
 | #G #K #k #l #Hkl #L #s #d #e #_ #U1 #H1 #U2 #H2
   >(lift_inv_sort1 … H1) -U1
-  >(lift_inv_sort1 … H2) -U2 /2 width=2 by cpx_sort/
+  >(lift_inv_sort1 … H2) -U2 /2 width=2 by cpx_st/
 | #I #G #K #KV #V #V2 #W2 #i #HKV #HV2 #HVW2 #IHV2 #L #s #d #e #HLK #U1 #H #U2 #HWU2
   elim (lift_inv_lref1 … H) * #Hid #H destruct
   [ elim (lift_trans_ge … HVW2 … HWU2) -W2 // <minus_plus #W2 #HVW2 #HWU2
@@ -65,9 +65,9 @@ lemma cpx_lift: ∀h,g,G. l_liftable (cpx h g G).
   elim (lift_inv_bind1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct
   elim (lift_conf_O1 … HTU2 … HT2) -T2 /4 width=6 by cpx_zeta, ldrop_skip/
 | #G #K #V #T1 #T2 #_ #IHT12 #L #s #d #e #HLK #U1 #H #U2 #HTU2
-  elim (lift_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct /3 width=6 by cpx_tau/
+  elim (lift_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct /3 width=6 by cpx_eps/
 | #G #K #V1 #V2 #T #_ #IHV12 #L #s #d #e #HLK #U1 #H #U2 #HVU2
-  elim (lift_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct /3 width=6 by cpx_ti/
+  elim (lift_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct /3 width=6 by cpx_ct/
 | #a #G #K #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L #s #d #e #HLK #X1 #HX1 #X2 #HX2
   elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct
   elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct
@@ -90,7 +90,7 @@ lemma cpx_inv_lift1: ∀h,g,G. l_deliftable_sn (cpx h g G).
   | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3 by cpx_atom, lift_gref, ex2_intro/
   ]
 | #G #L #k #l #Hkl #K #s #d #e #_ #T1 #H
-  lapply (lift_inv_sort2 … H) -H #H destruct /3 width=3 by cpx_sort, lift_sort, ex2_intro/
+  lapply (lift_inv_sort2 … H) -H #H destruct /3 width=3 by cpx_st, lift_sort, ex2_intro/
 | #I #G #L #LV #V #V2 #W2 #i #HLV #HV2 #HVW2 #IHV2 #K #s #d #e #HLK #T1 #H
   elim (lift_inv_lref2 … H) -H * #Hid #H destruct
   [ elim (ldrop_conf_lt … HLK … HLV) -L // #L #U #HKL #HLV #HUV
@@ -115,10 +115,10 @@ lemma cpx_inv_lift1: ∀h,g,G. l_deliftable_sn (cpx h g G).
   elim (lift_div_le … HU2 … HTU) -U /3 width=5 by cpx_zeta, ex2_intro/
 | #G #L #V #U1 #U2 #_ #IHU12 #K #s #d #e #HLK #X #H
   elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
-  elim (IHU12 … HLK … HTU1) -L -U1 /3 width=3 by cpx_tau, ex2_intro/
+  elim (IHU12 … HLK … HTU1) -L -U1 /3 width=3 by cpx_eps, ex2_intro/
 | #G #L #V1 #V2 #U1 #_ #IHV12 #K #s #d #e #HLK #X #H
   elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
-  elim (IHV12 … HLK … HWV1) -L -V1 /3 width=3 by cpx_ti, ex2_intro/
+  elim (IHV12 … HLK … HWV1) -L -V1 /3 width=3 by cpx_ct, ex2_intro/
 | #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #K #s #d #e #HLK #X #HX
   elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct
   elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma
index 7779c7f92..c36dd0fb4 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma
@@ -21,7 +21,7 @@ include "basic_2/reduction/cpx_llpx_sn.ma".
 
 lemma lleq_cpx_trans: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 →
                       ∀L1. L1 ⋕[T1, 0] L2 → ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2.
-#h #g #G #L2 #T1 #T2 #H elim H -G -L2 -T1 -T2 /2 width=2 by cpx_sort/
+#h #g #G #L2 #T1 #T2 #H elim H -G -L2 -T1 -T2 /2 width=2 by cpx_st/
 [ #I #G #L2 #K2 #V1 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV12 #L1 #H elim (lleq_fwd_lref_dx … H … HLK2) -L2
   [ #H elim (ylt_yle_false … H) //
   | * /3 width=7 by cpx_delta/
@@ -33,9 +33,9 @@ lemma lleq_cpx_trans: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 →
 | #G #L2 #V2 #T1 #T #T2 #_ #HT2 #IHT1 #L1 #H elim (lleq_inv_bind_O … H) -H
   /3 width=3 by cpx_zeta/
 | #G #L2 #W1 #T1 #T2 #_ #IHT12 #L1 #H elim (lleq_inv_flat … H) -H
-  /3 width=1 by cpx_tau/
+  /3 width=1 by cpx_eps/
 | #G #L2 #W1 #W2 #T1 #_ #IHW12 #L1 #H elim (lleq_inv_flat … H) -H
-  /3 width=1 by cpx_ti/
+  /3 width=1 by cpx_ct/
 | #a #G #L1 #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L1 #H elim (lleq_inv_flat … H) -H
   #HV1 #H elim (lleq_inv_bind_O … H) -H /3 width=1 by cpx_beta/
 | #a #G #L1 #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L1 #H elim (lleq_inv_flat … H) -H
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma
index d0b363455..ebf3d6406 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma
@@ -146,7 +146,7 @@ elim (IH … HV01 … HV02 … HL01 … HL02) //
 elim (IH … HT01 … HT02 … HL01 … HL02) /3 width=5 by cpr_flat, ex2_intro/
 qed-.
 
-fact cpr_conf_lpr_flat_tau:
+fact cpr_conf_lpr_flat_eps:
    ∀G,L0,V0,T0. (
       ∀L,T. ⦃G, L0, ⓝV0.T0⦄ ⊐+ ⦃G, L, T⦄ →
       ∀T1. ⦃G, L⦄ ⊢ T ➡ T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡ T2 →
@@ -158,10 +158,10 @@ fact cpr_conf_lpr_flat_tau:
    ∃∃T. ⦃G, L1⦄ ⊢ ⓝV1.T1 ➡ T & ⦃G, L2⦄ ⊢ T2 ➡ T.
 #G #L0 #V0 #T0 #IH #V1 #T1 #HT01
 #T2 #HT02 #L1 #HL01 #L2 #HL02
-elim (IH … HT01 … HT02 … HL01 … HL02) // -L0 -V0 -T0 /3 width=3 by cpr_tau, ex2_intro/
+elim (IH … HT01 … HT02 … HL01 … HL02) // -L0 -V0 -T0 /3 width=3 by cpr_eps, ex2_intro/
 qed-.
 
-fact cpr_conf_lpr_tau_tau:
+fact cpr_conf_lpr_eps_eps:
    ∀G,L0,V0,T0. (
       ∀L,T. ⦃G, L0, ⓝV0.T0⦄ ⊐+ ⦃G, L, T⦄ →
       ∀T1. ⦃G, L⦄ ⊢ T ➡ T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡ T2 →
@@ -319,11 +319,11 @@ theorem cpr_conf_lpr: ∀G. lpx_sn_confluent (cpr G) (cpr G).
   |4,8,12,16: #a2 #V2 #U2 #Y2 #W2 #Z2 #T2 #HV02 #HVU2 #HYW2 #HZT2 #H21 #H22 #H23
   ] destruct
   [ /3 width=10 by cpr_conf_lpr_flat_flat/
-  | /4 width=8 by ex2_commute, cpr_conf_lpr_flat_tau/
+  | /4 width=8 by ex2_commute, cpr_conf_lpr_flat_eps/
   | /4 width=12 by ex2_commute, cpr_conf_lpr_flat_beta/
   | /4 width=14 by ex2_commute, cpr_conf_lpr_flat_theta/
-  | /3 width=8 by cpr_conf_lpr_flat_tau/
-  | /3 width=7 by cpr_conf_lpr_tau_tau/
+  | /3 width=8 by cpr_conf_lpr_flat_eps/
+  | /3 width=7 by cpr_conf_lpr_eps_eps/
   | /3 width=12 by cpr_conf_lpr_flat_beta/
   | /3 width=13 by cpr_conf_lpr_beta_beta/
   | /3 width=14 by cpr_conf_lpr_flat_theta/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/cpy.etc b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma
similarity index 99%
rename from matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/cpy.etc
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma
index a1e538ae0..cf29f1cc2 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/cpy.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma
@@ -83,6 +83,7 @@ lemma cpy_weak: ∀G,L,T1,T2,d1,e1. ⦃G, L⦄ ⊢ T1 ▶[d1, e1] T2 →
 ]
 qed-.
 
+(* Note: lemma 1250 *)
 lemma cpy_weak_top: ∀G,L,T1,T2,d,e.
                     ⦃G, L⦄ ⊢ T1 ▶[d, e] T2 → ⦃G, L⦄ ⊢ T1 ▶[d, |L| - d] T2.
 #G #L #T1 #T2 #d #e #H elim H -G -L -T1 -T2 -d -e //
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/cpy_cpy.etc b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_cpy.ma
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/cpy_cpy.etc
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_cpy.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/cpy_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_lift.ma
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/cpy_lift.etc
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_lift.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lsuby.etc b/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma
similarity index 70%
rename from matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lsuby.etc
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma
index 6c90b202b..eb2c7bfec 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lsuby.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "ground_2/ynat/ynat_plus.ma".
-include "basic_2/notation/relations/extlrsubeq_4.ma".
+include "basic_2/notation/relations/lrsubeq_4.ma".
 include "basic_2/relocation/ldrop.ma".
 
 (* LOCAL ENVIRONMENT REFINEMENT FOR EXTENDED SUBSTITUTION *******************)
@@ -25,31 +25,31 @@ inductive lsuby: relation4 ynat ynat lenv lenv ≝
 | lsuby_pair: ∀I1,I2,L1,L2,V,e. lsuby 0 e L1 L2 →
               lsuby 0 (⫯e) (L1.ⓑ{I1}V) (L2.ⓑ{I2}V)
 | lsuby_succ: ∀I1,I2,L1,L2,V1,V2,d,e.
-              lsuby d e L1 L2 → lsuby (⫯d) e (L1. ⓑ{I1}V1) (L2. ⓑ{I2} V2)
+              lsuby d e L1 L2 → lsuby (⫯d) e (L1.ⓑ{I1}V1) (L2.ⓑ{I2}V2)
 .
 
 interpretation
   "local environment refinement (extended substitution)"
-  'ExtLRSubEq L1 d e L2 = (lsuby d e L1 L2).
+  'LRSubEq L1 d e L2 = (lsuby d e L1 L2).
 
 (* Basic properties *********************************************************)
 
-lemma lsuby_pair_lt: ∀I1,I2,L1,L2,V,e. L1 ⊑×[0, ⫰e] L2 → 0 < e →
-                     L1.ⓑ{I1}V ⊑×[0, e] L2.ⓑ{I2}V.
+lemma lsuby_pair_lt: ∀I1,I2,L1,L2,V,e. L1 ⊆[0, ⫰e] L2 → 0 < e →
+                     L1.ⓑ{I1}V ⊆[0, e] L2.ⓑ{I2}V.
 #I1 #I2 #L1 #L2 #V #e #HL12 #He <(ylt_inv_O1 … He) /2 width=1 by lsuby_pair/
 qed.
 
-lemma lsuby_succ_lt: ∀I1,I2,L1,L2,V1,V2,d,e. L1 ⊑×[⫰d, e] L2 → 0 < d →
-                     L1.ⓑ{I1}V1 ⊑×[d, e] L2. ⓑ{I2}V2.
+lemma lsuby_succ_lt: ∀I1,I2,L1,L2,V1,V2,d,e. L1 ⊆[⫰d, e] L2 → 0 < d →
+                     L1.ⓑ{I1}V1 ⊆[d, e] L2. ⓑ{I2}V2.
 #I1 #I2 #L1 #L2 #V1 #V2 #d #e #HL12 #Hd <(ylt_inv_O1 … Hd) /2 width=1 by lsuby_succ/
 qed.
 
-lemma lsuby_pair_O_Y: ∀L1,L2. L1 ⊑×[0, ∞] L2 →
-                      ∀I1,I2,V. L1.ⓑ{I1}V ⊑×[0,∞] L2.ⓑ{I2}V.
+lemma lsuby_pair_O_Y: ∀L1,L2. L1 ⊆[0, ∞] L2 →
+                      ∀I1,I2,V. L1.ⓑ{I1}V ⊆[0,∞] L2.ⓑ{I2}V.
 #L1 #L2 #HL12 #I1 #I2 #V lapply (lsuby_pair I1 I2 … V … HL12) -HL12 //
 qed.
 
-lemma lsuby_refl: ∀L,d,e. L ⊑×[d, e] L.
+lemma lsuby_refl: ∀L,d,e. L ⊆[d, e] L.
 #L elim L -L //
 #L #I #V #IHL #d elim (ynat_cases … d) [| * #x ]
 #Hd destruct /2 width=1 by lsuby_succ/
@@ -57,7 +57,7 @@ lemma lsuby_refl: ∀L,d,e. L ⊑×[d, e] L.
 #He destruct /2 width=1 by lsuby_zero, lsuby_pair/
 qed.
 
-lemma lsuby_O2: ∀L2,L1,d. |L2| ≤ |L1| → L1 ⊑×[d, yinj 0] L2.
+lemma lsuby_O2: ∀L2,L1,d. |L2| ≤ |L1| → L1 ⊆[d, yinj 0] L2.
 #L2 elim L2 -L2 // #L2 #I2 #V2 #IHL2 * normalize
 [ #d #H lapply (le_n_O_to_eq … H) -H <plus_n_Sm #H destruct
 | #L1 #I1 #V1 #d #H lapply (le_plus_to_le_r … H) -H #HL12
@@ -66,7 +66,7 @@ lemma lsuby_O2: ∀L2,L1,d. |L2| ≤ |L1| → L1 ⊑×[d, yinj 0] L2.
 ]
 qed.
 
-lemma lsuby_sym: ∀d,e,L1,L2. L1 ⊑×[d, e] L2 → |L1| = |L2| → L2 ⊑×[d, e] L1.
+lemma lsuby_sym: ∀d,e,L1,L2. L1 ⊆[d, e] L2 → |L1| = |L2| → L2 ⊆[d, e] L1.
 #d #e #L1 #L2 #H elim H -d -e -L1 -L2
 [ #L1 #d #e #H >(length_inv_zero_dx … H) -L1 //
 | /2 width=1 by lsuby_O2/
@@ -79,7 +79,7 @@ qed-.
 
 (* Basic inversion lemmas ***************************************************)
 
-fact lsuby_inv_atom1_aux: ∀L1,L2,d,e. L1 ⊑×[d, e] L2 → L1 = ⋆ → L2 = ⋆.
+fact lsuby_inv_atom1_aux: ∀L1,L2,d,e. L1 ⊆[d, e] L2 → L1 = ⋆ → L2 = ⋆.
 #L1 #L2 #d #e * -L1 -L2 -d -e //
 [ #I1 #I2 #L1 #L2 #V1 #V2 #_ #H destruct
 | #I1 #I2 #L1 #L2 #V #e #_ #H destruct
@@ -87,13 +87,13 @@ fact lsuby_inv_atom1_aux: ∀L1,L2,d,e. L1 ⊑×[d, e] L2 → L1 = ⋆ → L2 =
 ]
 qed-.
 
-lemma lsuby_inv_atom1: ∀L2,d,e. ⋆ ⊑×[d, e] L2 → L2 = ⋆.
+lemma lsuby_inv_atom1: ∀L2,d,e. ⋆ ⊆[d, e] L2 → L2 = ⋆.
 /2 width=5 by lsuby_inv_atom1_aux/ qed-.
 
-fact lsuby_inv_zero1_aux: ∀L1,L2,d,e. L1 ⊑×[d, e] L2 →
+fact lsuby_inv_zero1_aux: ∀L1,L2,d,e. L1 ⊆[d, e] L2 →
                           ∀J1,K1,W1. L1 = K1.ⓑ{J1}W1 → d = 0 → e = 0 →
                           L2 = ⋆ ∨
-                          ∃∃J2,K2,W2. K1 ⊑×[0, 0] K2 & L2 = K2.ⓑ{J2}W2.
+                          ∃∃J2,K2,W2. K1 ⊆[0, 0] K2 & L2 = K2.ⓑ{J2}W2.
 #L1 #L2 #d #e * -L1 -L2 -d -e /2 width=1 by or_introl/
 [ #I1 #I2 #L1 #L2 #V1 #V2 #HL12 #J1 #K1 #W1 #H #_ #_ destruct
   /3 width=5 by ex2_3_intro, or_intror/
@@ -104,15 +104,15 @@ fact lsuby_inv_zero1_aux: ∀L1,L2,d,e. L1 ⊑×[d, e] L2 →
 ]
 qed-.
 
-lemma lsuby_inv_zero1: ∀I1,K1,L2,V1. K1.ⓑ{I1}V1 ⊑×[0, 0] L2 →
+lemma lsuby_inv_zero1: ∀I1,K1,L2,V1. K1.ⓑ{I1}V1 ⊆[0, 0] L2 →
                        L2 = ⋆ ∨
-                       ∃∃I2,K2,V2. K1 ⊑×[0, 0] K2 & L2 = K2.ⓑ{I2}V2.
+                       ∃∃I2,K2,V2. K1 ⊆[0, 0] K2 & L2 = K2.ⓑ{I2}V2.
 /2 width=9 by lsuby_inv_zero1_aux/ qed-.
 
-fact lsuby_inv_pair1_aux: ∀L1,L2,d,e. L1 ⊑×[d, e] L2 →
+fact lsuby_inv_pair1_aux: ∀L1,L2,d,e. L1 ⊆[d, e] L2 →
                           ∀J1,K1,W. L1 = K1.ⓑ{J1}W → d = 0 → 0 < e →
                           L2 = ⋆ ∨
-                          ∃∃J2,K2. K1 ⊑×[0, ⫰e] K2 & L2 = K2.ⓑ{J2}W.
+                          ∃∃J2,K2. K1 ⊆[0, ⫰e] K2 & L2 = K2.ⓑ{J2}W.
 #L1 #L2 #d #e * -L1 -L2 -d -e /2 width=1 by or_introl/
 [ #I1 #I2 #L1 #L2 #V1 #V2 #_ #J1 #K1 #W #_ #_ #H
   elim (ylt_yle_false … H) //
@@ -123,15 +123,15 @@ fact lsuby_inv_pair1_aux: ∀L1,L2,d,e. L1 ⊑×[d, e] L2 →
 ]
 qed-.
 
-lemma lsuby_inv_pair1: ∀I1,K1,L2,V,e. K1.ⓑ{I1}V ⊑×[0, e] L2 → 0 < e →
+lemma lsuby_inv_pair1: ∀I1,K1,L2,V,e. K1.ⓑ{I1}V ⊆[0, e] L2 → 0 < e →
                        L2 = ⋆ ∨
-                       ∃∃I2,K2. K1 ⊑×[0, ⫰e] K2 & L2 = K2.ⓑ{I2}V.
+                       ∃∃I2,K2. K1 ⊆[0, ⫰e] K2 & L2 = K2.ⓑ{I2}V.
 /2 width=6 by lsuby_inv_pair1_aux/ qed-.
 
-fact lsuby_inv_succ1_aux: ∀L1,L2,d,e. L1 ⊑×[d, e] L2 →
+fact lsuby_inv_succ1_aux: ∀L1,L2,d,e. L1 ⊆[d, e] L2 →
                           ∀J1,K1,W1. L1 = K1.ⓑ{J1}W1 → 0 < d →
                           L2 = ⋆ ∨
-                          ∃∃J2,K2,W2. K1 ⊑×[⫰d, e] K2 & L2 = K2.ⓑ{J2}W2.
+                          ∃∃J2,K2,W2. K1 ⊆[⫰d, e] K2 & L2 = K2.ⓑ{J2}W2.
 #L1 #L2 #d #e * -L1 -L2 -d -e /2 width=1 by or_introl/
 [ #I1 #I2 #L1 #L2 #V1 #V2 #_ #J1 #K1 #W1 #_ #H
   elim (ylt_yle_false … H) //
@@ -142,14 +142,14 @@ fact lsuby_inv_succ1_aux: ∀L1,L2,d,e. L1 ⊑×[d, e] L2 →
 ]
 qed-.
 
-lemma lsuby_inv_succ1: ∀I1,K1,L2,V1,d,e. K1.ⓑ{I1}V1 ⊑×[d, e] L2 → 0 < d →
+lemma lsuby_inv_succ1: ∀I1,K1,L2,V1,d,e. K1.ⓑ{I1}V1 ⊆[d, e] L2 → 0 < d →
                        L2 = ⋆ ∨
-                       ∃∃I2,K2,V2. K1 ⊑×[⫰d, e] K2 & L2 = K2.ⓑ{I2}V2.
+                       ∃∃I2,K2,V2. K1 ⊆[⫰d, e] K2 & L2 = K2.ⓑ{I2}V2.
 /2 width=5 by lsuby_inv_succ1_aux/ qed-.
 
-fact lsuby_inv_zero2_aux: ∀L1,L2,d,e. L1 ⊑×[d, e] L2 →
+fact lsuby_inv_zero2_aux: ∀L1,L2,d,e. L1 ⊆[d, e] L2 →
                           ∀J2,K2,W2. L2 = K2.ⓑ{J2}W2 → d = 0 → e = 0 →
-                          ∃∃J1,K1,W1. K1 ⊑×[0, 0] K2 & L1 = K1.ⓑ{J1}W1.
+                          ∃∃J1,K1,W1. K1 ⊆[0, 0] K2 & L1 = K1.ⓑ{J1}W1.
 #L1 #L2 #d #e * -L1 -L2 -d -e
 [ #L1 #d #e #J2 #K2 #W1 #H destruct
 | #I1 #I2 #L1 #L2 #V1 #V2 #HL12 #J2 #K2 #W2 #H #_ #_ destruct
@@ -161,13 +161,13 @@ fact lsuby_inv_zero2_aux: ∀L1,L2,d,e. L1 ⊑×[d, e] L2 →
 ]
 qed-.
 
-lemma lsuby_inv_zero2: ∀I2,K2,L1,V2. L1 ⊑×[0, 0] K2.ⓑ{I2}V2 →
-                       ∃∃I1,K1,V1. K1 ⊑×[0, 0] K2 & L1 = K1.ⓑ{I1}V1.
+lemma lsuby_inv_zero2: ∀I2,K2,L1,V2. L1 ⊆[0, 0] K2.ⓑ{I2}V2 →
+                       ∃∃I1,K1,V1. K1 ⊆[0, 0] K2 & L1 = K1.ⓑ{I1}V1.
 /2 width=9 by lsuby_inv_zero2_aux/ qed-.
 
-fact lsuby_inv_pair2_aux: ∀L1,L2,d,e. L1 ⊑×[d, e] L2 →
+fact lsuby_inv_pair2_aux: ∀L1,L2,d,e. L1 ⊆[d, e] L2 →
                           ∀J2,K2,W. L2 = K2.ⓑ{J2}W → d = 0 → 0 < e →
-                          ∃∃J1,K1. K1 ⊑×[0, ⫰e] K2 & L1 = K1.ⓑ{J1}W.
+                          ∃∃J1,K1. K1 ⊆[0, ⫰e] K2 & L1 = K1.ⓑ{J1}W.
 #L1 #L2 #d #e * -L1 -L2 -d -e
 [ #L1 #d #e #J2 #K2 #W #H destruct
 | #I1 #I2 #L1 #L2 #V1 #V2 #_ #J2 #K2 #W #_ #_ #H
@@ -179,13 +179,13 @@ fact lsuby_inv_pair2_aux: ∀L1,L2,d,e. L1 ⊑×[d, e] L2 →
 ]
 qed-.
 
-lemma lsuby_inv_pair2: ∀I2,K2,L1,V,e. L1 ⊑×[0, e] K2.ⓑ{I2}V → 0 < e →
-                       ∃∃I1,K1. K1 ⊑×[0, ⫰e] K2 & L1 = K1.ⓑ{I1}V.
+lemma lsuby_inv_pair2: ∀I2,K2,L1,V,e. L1 ⊆[0, e] K2.ⓑ{I2}V → 0 < e →
+                       ∃∃I1,K1. K1 ⊆[0, ⫰e] K2 & L1 = K1.ⓑ{I1}V.
 /2 width=6 by lsuby_inv_pair2_aux/ qed-.
 
-fact lsuby_inv_succ2_aux: ∀L1,L2,d,e. L1 ⊑×[d, e] L2 →
+fact lsuby_inv_succ2_aux: ∀L1,L2,d,e. L1 ⊆[d, e] L2 →
                           ∀J2,K2,W2. L2 = K2.ⓑ{J2}W2 → 0 < d →
-                          ∃∃J1,K1,W1. K1 ⊑×[⫰d, e] K2 & L1 = K1.ⓑ{J1}W1.
+                          ∃∃J1,K1,W1. K1 ⊆[⫰d, e] K2 & L1 = K1.ⓑ{J1}W1.
 #L1 #L2 #d #e * -L1 -L2 -d -e
 [ #L1 #d #e #J2 #K2 #W2 #H destruct
 | #I1 #I2 #L1 #L2 #V1 #V2 #_ #J2 #K2 #W2 #_ #H
@@ -197,22 +197,22 @@ fact lsuby_inv_succ2_aux: ∀L1,L2,d,e. L1 ⊑×[d, e] L2 →
 ]
 qed-.
 
-lemma lsuby_inv_succ2: ∀I2,K2,L1,V2,d,e. L1 ⊑×[d, e] K2.ⓑ{I2}V2 → 0 < d →
-                       ∃∃I1,K1,V1. K1 ⊑×[⫰d, e] K2 & L1 = K1.ⓑ{I1}V1.
+lemma lsuby_inv_succ2: ∀I2,K2,L1,V2,d,e. L1 ⊆[d, e] K2.ⓑ{I2}V2 → 0 < d →
+                       ∃∃I1,K1,V1. K1 ⊆[⫰d, e] K2 & L1 = K1.ⓑ{I1}V1.
 /2 width=5 by lsuby_inv_succ2_aux/ qed-.
 
 (* Basic forward lemmas *****************************************************)
 
-lemma lsuby_fwd_length: ∀L1,L2,d,e. L1 ⊑×[d, e] L2 → |L2| ≤ |L1|.
+lemma lsuby_fwd_length: ∀L1,L2,d,e. L1 ⊆[d, e] L2 → |L2| ≤ |L1|.
 #L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize /2 width=1 by le_S_S/
 qed-.
 
 (* Properties on basic slicing **********************************************)
 
-lemma lsuby_ldrop_trans_be: ∀L1,L2,d,e. L1 ⊑×[d, e] L2 →
+lemma lsuby_ldrop_trans_be: ∀L1,L2,d,e. L1 ⊆[d, e] L2 →
                             ∀I2,K2,W,s,i. ⇩[s, 0, i] L2 ≡ K2.ⓑ{I2}W →
                             d ≤ i → i < d + e →
-                            ∃∃I1,K1. K1 ⊑×[0, ⫰(d+e-i)] K2 & ⇩[s, 0, i] L1 ≡ K1.ⓑ{I1}W.
+                            ∃∃I1,K1. K1 ⊆[0, ⫰(d+e-i)] K2 & ⇩[s, 0, i] L1 ≡ K1.ⓑ{I1}W.
 #L1 #L2 #d #e #H elim H -L1 -L2 -d -e
 [ #L1 #d #e #J2 #K2 #W #s #i #H
   elim (ldrop_inv_atom1 … H) -H #H destruct
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lsuby_lsuby.etc b/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby_lsuby.ma
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lsuby_lsuby.etc
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby_lsuby.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubr.ma
index 1d1a01beb..0595e7c20 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lsubr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsubr.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/notation/relations/lrsubeq_2.ma".
+include "basic_2/notation/relations/lrsubeqc_2.ma".
 include "basic_2/relocation/ldrop.ma".
 
 (* RESTRICTED LOCAL ENVIRONMENT REFINEMENT **********************************)
@@ -25,7 +25,7 @@ inductive lsubr: relation lenv ≝
 
 interpretation
   "local environment refinement (restricted)"
-  'LRSubEq L1 L2 = (lsubr L1 L2).
+  'LRSubEqC L1 L2 = (lsubr L1 L2).
 
 (* Basic properties *********************************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/cpys.etc b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys.ma
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/cpys.etc
rename to matita/matita/contribs/lambdadelta/basic_2/substitution/cpys.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/cpys_alt.etc b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_alt.ma
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/cpys_alt.etc
rename to matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_alt.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/cpys_cpys.etc b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_cpys.ma
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/cpys_cpys.etc
rename to matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_cpys.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/cpys_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_lift.ma
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/cpys_lift.etc
rename to matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_lift.ma
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 1c427b89f..50b02acb9 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
@@ -214,7 +214,11 @@ table {
              [ "lleq ( ? ⋕[?,?] ? )" "lleq_alt" + "lleq_leq" + "lleq_ldrop" + "lleq_fqus" + "lleq_lleq" * ]
           }
         ]
-        [ { "iterated structural successor for closures" * } {
+        [ { "contxt-sensitive extended multiple substitution" * } {
+             [ "cpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? )" "cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? )" "cpys_lift" + "cpys_cpys" * ]
+          }
+        ]
+	[ { "iterated structural successor for closures" * } {
              [ "fqus ( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ )" "fqus_alt" + "fqus_fqus" * ]
              [ "fqup ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ )" "fqup_fqup" * ]
           }
@@ -254,7 +258,15 @@ table {
              [ "lpx_sn" "lpx_sn_alt" + "lpx_sn_tc" + "lpx_sn_ldrop" + "lpx_sn_lpx_sn" * ]
           }
         ]
-        [ { "basic local env. slicing" * } {
+        [ { "contxt-sensitive extended ordinary substitution" * } {
+             [ "cpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? )" "cpy_lift" + "cpy_cpy" * ]
+          }
+        ]
+        [ { "local env. ref. for extended substitution" * } {
+             [ "lsuby ( ? ⊑×[?,?] ? )" "lsuby_lsuby" * ]
+          }
+        ]
+	[ { "basic local env. slicing" * } {
              [ "ldrop ( ⇩[?,?,?] ? ≡ ? )"  "ldrop_leq" + "ldrop_ldrop" * ]
           }
         ]
-- 
2.39.2