From ea83c19f4cac864dd87eb059d8aeb2343eba480f Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sat, 2 Jun 2012 18:37:03 +0000
Subject: [PATCH] - predefined_virtuals: an addition - lambda_delta: lenv ref
 for native type assignment completed                 levn ref for
 substitution correctly oriented

---
 .../contribs/lambda_delta/basic_2/basic_1.txt |  2 -
 .../lambda_delta/basic_2/computation/cprs.ma  |  4 +-
 .../basic_2/computation/cprs_cprs.ma          |  2 +-
 .../lambda_delta/basic_2/dynamic/lsubn.ma     | 10 +++
 .../basic_2/dynamic/lsubn_cpcs.ma             | 34 ++++++++++
 .../lambda_delta/basic_2/dynamic/lsubn_nta.ma |  6 +-
 .../lambda_delta/basic_2/dynamic/nta_thin.ma  |  8 +--
 .../basic_2/equivalence/cpcs_cpcs.ma          |  9 +++
 .../contribs/lambda_delta/basic_2/notation.ma |  4 +-
 .../lambda_delta/basic_2/reducibility/cpr.ma  | 10 +--
 .../basic_2/reducibility/cpr_cpr.ma           |  2 +-
 .../basic_2/reducibility/cpr_lift.ma          |  4 +-
 .../basic_2/reducibility/ltpr_aaa.ma          |  2 +-
 .../basic_2/reducibility/tpr_tpss.ma          |  8 +--
 .../lambda_delta/basic_2/static/lsuba.ma      |  2 +-
 .../basic_2/static/lsuba_ldrop.ma             |  2 +-
 .../basic_2/substitution/ldrop.ma             | 10 +--
 .../basic_2/substitution/ldrop_sfr.ma         | 18 ++---
 .../basic_2/substitution/lsubs.ma             | 68 ++++++++++++++-----
 .../basic_2/substitution/lsubs_sfr.ma         | 32 ++++-----
 .../lambda_delta/basic_2/substitution/tps.ma  | 10 +--
 .../basic_2/substitution/tps_tps.ma           | 20 +++---
 .../lambda_delta/basic_2/unfold/delift.ma     |  8 +--
 .../lambda_delta/basic_2/unfold/delift_alt.ma | 10 +--
 .../basic_2/unfold/ltpss_ltpss.ma             |  4 +-
 .../lambda_delta/basic_2/unfold/tpss.ma       |  8 +--
 .../lambda_delta/basic_2/unfold/tpss_alt.ma   | 10 +--
 .../contribs/lambda_delta/ground_2/star.ma    | 13 ++++
 matita/matita/predefined_virtuals.ml          |  3 +-
 29 files changed, 211 insertions(+), 112 deletions(-)
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/dynamic/lsubn_cpcs.ma

diff --git a/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt b/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt
index 9e3ecb792..544232544 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt
+++ b/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt
@@ -81,8 +81,6 @@ csubc/drop drop_csubc_trans
 csubt/csuba csubt_csuba
 csubt/fwd csubt_gen_abbr
 csubt/fwd csubt_gen_abst
-csubt/pc3 csubt_pr2
-csubt/pc3 csubt_pc3
 
 csubv/clear csubv_clear_conf
 csubv/clear csubv_clear_conf_void
diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma
index dbd23a0a4..0891cb00c 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma
@@ -55,8 +55,8 @@ lemma cprs_strap2: ∀L,T1,T,T2.
 /2 width=3/ qed.
 
 (* Note: it does not hold replacing |L1| with |L2| *)
-lemma cprs_lsubs_conf: ∀L1,T1,T2. L1 ⊢ T1 ➡* T2 →
-                       ∀L2. L1 ≼ [0, |L1|] L2 → L2 ⊢ T1 ➡* T2.
+lemma cprs_lsubs_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/lambda_delta/basic_2/computation/cprs_cprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_cprs.ma
index 85b391d2d..a71c773bc 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_cprs.ma
+++ b/matita/matita/contribs/lambda_delta/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 → L ⊢ ⓛV1. T1 ➡* ⓛV2. T2.
 #L #V1 #V2 #HV12 #V #T1 #T2 #HT12 @(cprs_ind … HV12) -V2
-[ lapply (cprs_lsubs_conf … HT12 (L.ⓛV1) ?) -HT12 /2 width=2/
+[ lapply (cprs_lsubs_trans … HT12 (L.ⓛV1) ?) -HT12 /2 width=2/
 | #V0 #V2 #_ #HV02 #IHV01
   @(cprs_trans … IHV01) -V1 /2 width=2/
 ]
diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/lsubn.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/lsubn.ma
index 9a4eaac88..cedff815a 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/lsubn.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/lsubn.ma
@@ -87,6 +87,16 @@ lemma lsubn_inv_pair2: ∀h,I,L1,K2,W. h ⊢ L1 :⊑ K2. ⓑ{I} W →
                                h ⊢ K1 :⊑ K2 & L1 = K1. ⓓV & I = Abst.
 /2 width=3/ qed-.
 
+(* Basic_forward lemmas *****************************************************)
+
+lemma lsubn_fwd_lsubs1: ∀h,L1,L2. h ⊢ L1 :⊑ L2 → L1 ≼[0, |L1|] L2.
+#h #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
+qed-.
+
+lemma lsubn_fwd_lsubs2: ∀h,L1,L2. h ⊢ L1 :⊑ L2 → L1 ≼[0, |L2|] L2.
+#h #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
+qed-.
+
 (* Basic properties *********************************************************)
 
 (* Basic_1: was: csubt_refl *)
diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/lsubn_cpcs.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/lsubn_cpcs.ma
new file mode 100644
index 000000000..5f610bc96
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/lsubn_cpcs.ma
@@ -0,0 +1,34 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/equivalence/cpcs_cpcs.ma".
+include "basic_2/dynamic/lsubn.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE TYPE ASSIGNMENT ******************)
+
+(* Properties on context-sensitive parallel equivalence for terms ***********)
+
+(* Basic_1: was: csubt_pr2 *)
+lemma cpr_lsubn_trans: ∀h,L1,L2. h ⊢ L1 :⊑ L2 →
+                       ∀T1,T2. L2 ⊢ T1 ➡ T2 → L1 ⊢ T1 ➡ T2.
+/3 width=4 by lsubn_fwd_lsubs2, cpr_lsubs_trans/ qed.
+
+lemma cprs_lsubn_trans: ∀h,L1,L2. h ⊢ L1 :⊑ L2 →
+                        ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2.
+/3 width=4 by lsubn_fwd_lsubs2, cprs_lsubs_trans/ qed.
+
+(* Basic_1: was: csubt_pc3 *)
+lemma cpcs_lsubn_trans: ∀h,L1,L2. h ⊢ L1 :⊑ L2 →
+                        ∀T1,T2. L2 ⊢ T1 ⬌* T2 → L1 ⊢ T1 ⬌* T2.
+/3 width=4 by lsubn_fwd_lsubs2, cpcs_lsubs_trans/ qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/lsubn_nta.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/lsubn_nta.ma
index 6f91a1c52..5832b00b6 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/lsubn_nta.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/lsubn_nta.ma
@@ -14,6 +14,7 @@
 
 include "basic_2/dynamic/nta_nta.ma".
 include "basic_2/dynamic/lsubn_ldrop.ma".
+include "basic_2/dynamic/lsubn_cpcs.ma".
 
 (* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE TYPE ASSIGNMENT ******************)
 
@@ -21,9 +22,8 @@ include "basic_2/dynamic/lsubn_ldrop.ma".
 
 (* Note: the corresponding confluence property does not hold *)
 (* Basic_1: was: csubt_ty3 *)
-axiom lsubn_nta_trans: ∀h,L2,T,U. ⦃h, L2⦄ ⊢ T : U → ∀L1. h ⊢ L1 :⊑ L2 →
+lemma lsubn_nta_trans: ∀h,L2,T,U. ⦃h, L2⦄ ⊢ T : U → ∀L1. h ⊢ L1 :⊑ L2 →
                        ⦃h, L1⦄ ⊢ T : U.
-(*
 #h #L2 #T #U #H elim H -L2 -T -U
 [ //
 | #L2 #K2 #V2 #W2 #U2 #i #HLK2 #_ #WU2 #IHVW2 #L1 #HL12
@@ -42,6 +42,6 @@ axiom lsubn_nta_trans: ∀h,L2,T,U. ⦃h, L2⦄ ⊢ T : U → ∀L1. h ⊢ L1 :
 | /3 width=1/
 | /3 width=2/
 | /3 width=1/
+| /4 width=6/
 ]
 qed.
-*)
diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_thin.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_thin.ma
index c3f94f9eb..96e84dd51 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_thin.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_thin.ma
@@ -25,7 +25,7 @@ include "basic_2/dynamic/nta_lift.ma".
 (* Note: this is known as the substitution lemma *)
 (* Basic_1: was only: ty3_gen_cabbr *)
 lemma nta_thin_conf: ∀h,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 : U1 →
-                     ∀L2,d,e. ≼ [d, e] L1 → L1 ▼*[d, e] ≡ L2 →
+                     ∀L2,d,e. ≽ [d, e] L1 → L1 ▼*[d, e] ≡ L2 →
                      ∃∃T2,U2. ⦃h, L2⦄ ⊢ T2 : U2 &
                               L1 ⊢ T1 ▼*[d, e] ≡ T2 & L1 ⊢ U1 ▼*[d, e] ≡ U2.
 #h #L1 #T1 #U1 #H elim H -L1 -T1 -U1
@@ -87,8 +87,8 @@ lemma nta_thin_conf: ∀h,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 : U1 →
 | #I #L1 #V1 #W1 #T1 #U1 #_ #_ #IHVW1 #IHTU1 #L2 #d #e #HL1 #HL12
   elim (IHVW1 … HL1 HL12) -IHVW1 #V2 #W2 #HVW2 #HV12 #_
   elim (IHTU1 (L2.ⓑ{I}V2) (d+1) e ? ?) -IHTU1 /2 width=1/ -HL1 -HL12 #T2 #U2 #HTU2 #HT12 #HU12
-  lapply (delift_lsubs_conf … HT12 (L1.ⓑ{I}V2) ?) -HT12 /2 width=1/
-  lapply (delift_lsubs_conf … HU12 (L1.ⓑ{I}V2) ?) -HU12 /2 width=1/ /3 width=7/
+  lapply (delift_lsubs_trans … HT12 (L1.ⓑ{I}V2) ?) -HT12 /2 width=1/
+  lapply (delift_lsubs_trans … HU12 (L1.ⓑ{I}V2) ?) -HU12 /2 width=1/ /3 width=7/
 | #L1 #V1 #W1 #T1 #U1 #_ #_ #IHVW1 #IHTU1 #L2 #d #e #HL1 #HL12
   elim (IHVW1 … HL1 HL12) -IHVW1 #V2 #W2 #HVW2 #HV12 #HW12
   elim (IHTU1 … HL1 HL12) -IHTU1 -HL1 -HL12 #X2 #Y2 #HXY2 #HX2 #HY2
@@ -112,7 +112,7 @@ lemma nta_thin_conf: ∀h,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 : U1 →
 qed.
 
 lemma nta_ldrop_conf: ∀h,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 : U1 →
-                      ∀L2,d,e. ≼ [d, e] L1 → ⇩[d, e] L1 ≡ L2 →
+                      ∀L2,d,e. ≽ [d, e] L1 → ⇩[d, e] L1 ≡ L2 →
                       ∃∃T2,U2. ⦃h, L2⦄ ⊢ T2 : U2 &
                                L1 ⊢ T1 ▼*[d, e] ≡ T2 & L1 ⊢ U1 ▼*[d, e] ≡ U2.
 /3 width=1/ qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma
index 71fe21e80..bbf70c782 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma
@@ -111,6 +111,15 @@ qed.
 lemma cpcs_bind_sn: ∀I,L,V1,V2,T. L ⊢ V1 ⬌* V2 → L ⊢ ⓑ{I}V1. T ⬌* ⓑ{I}V2. T.
 * /2 width=1/ /2 width=2/ qed.
 
+(* Note: it does not hold replacing |L1| with |L2| *)
+lemma cpcs_lsubs_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 *)
+qed.
+
+
 (* Basic_1: was: pc3_lift *)
 lemma cpcs_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K →
                  ∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀T2,U2. ⇧[d, e] T2 ≡ U2 →
diff --git a/matita/matita/contribs/lambda_delta/basic_2/notation.ma b/matita/matita/contribs/lambda_delta/basic_2/notation.ma
index eb3d61cac..8a947e683 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/notation.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/notation.ma
@@ -138,9 +138,9 @@ notation "hvbox( T1 break ≼ [ d , break e ] break term 46 T2 )"
    non associative with precedence 45
    for @{ 'SubEq $T1 $d $e $T2 }.
 
-notation "hvbox( ≼ [ d , break e ] break term 46 T2 )"
+notation "hvbox( ≽ [ d , break e ] break term 46 T2 )"
    non associative with precedence 45
-   for @{ 'SubEqTop $d $e $T2 }.
+   for @{ 'SubEqBottom $d $e $T2 }.
 
 notation "hvbox( ⇩ [ e ] break term 46 L1 ≡ break term 46 L2 )"
    non associative with precedence 45
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma
index 18ad47c3e..072d951ba 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma
@@ -55,10 +55,10 @@ qed.
 
 (* Note: it does not hold replacing |L1| with |L2| *)
 (* Basic_1: was only: pr2_change *)
-lemma cpr_lsubs_conf: ∀L1,T1,T2. L1 ⊢ T1 ➡ T2 →
-                      ∀L2. L1 ≼ [0, |L1|] L2 → L2 ⊢ T1 ➡ T2.
+lemma cpr_lsubs_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_conf … HT2 … HL12) -HT2 -HL12 /3 width=4/
+lapply (tpss_lsubs_trans … HT2 … HL12) -HT2 -HL12 /3 width=4/
 qed.
 
 (* Basic inversion lemmas ***************************************************)
@@ -87,9 +87,9 @@ lemma cpr_inv_abbr1: ∀L,V1,T1,U2. L ⊢ ⓓV1. T1 ➡ U2 →
 elim (tpr_inv_abbr1 … H1) -H1 *
 [ #V #T0 #T #HV1 #HT10 #HT0 #H destruct
   elim (tpss_inv_bind1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H destruct
-  lapply (tps_lsubs_conf … HT0 (L. ⓓV) ?) -HT0 /2 width=1/ #HT0
+  lapply (tps_lsubs_trans … HT0 (L. ⓓV) ?) -HT0 /2 width=1/ #HT0
   lapply (tps_weak_all … HT0) -HT0 #HT0
-  lapply (tpss_lsubs_conf … HT2 (L. ⓓV) ?) -HT2 /2 width=1/ #HT2
+  lapply (tpss_lsubs_trans … HT2 (L. ⓓV) ?) -HT2 /2 width=1/ #HT2
   lapply (tpss_weak_all … HT2) -HT2 #HT2
   lapply (tpss_strap … HT0 HT2) -T /4 width=7/
 | /4 width=5/
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_cpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_cpr.ma
index aadf05b82..583726cd4 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_cpr.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_cpr.ma
@@ -30,7 +30,7 @@ lemma cpr_bind_dx: ∀I,L,V1,V2,T1,T2. V1 ➡ V2 → L. ⓑ{I} V2 ⊢ T1 ➡ T2
                    L ⊢ ⓑ{I} V1. T1 ➡ ⓑ{I} V2. T2.
 #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_conf … HT0 (⋆. ⓑ{I} V2) ?) -HT0 /2 width=1/ #HT0
+lapply (tpss_lsubs_trans … HT0 (⋆. ⓑ{I} V2) ?) -HT0 /2 width=1/ #HT0
 lapply (tpss_tps … HT0) -HT0 #HT0
 @ex2_1_intro [2: @(tpr_delta … HV12 HT1 HT0) | skip | /2 width=1/ ] (**) (* /3 width=5/ is too slow *)
 qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma
index dedb174e6..9994fdd6b 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma
@@ -34,7 +34,7 @@ lemma cpr_abst: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀V,T1,T2.
 lapply (tpss_inv_S2 … HT02 L V ?) -HT02 // #HT02
 @(ex2_1_intro … (ⓛV0.T0)) /2 width=1/ -V1 -T1 (**) (* explicit constructors *)
 @tpss_bind // -V0
-@(tpss_lsubs_conf (L.ⓛV)) // -T0 -T2 /2 width=1/
+@(tpss_lsubs_trans (L.ⓛV)) // -T0 -T2 /2 width=1/
 qed.
 
 (* Advanced inversion lemmas ************************************************)
@@ -58,7 +58,7 @@ lemma cpr_inv_abst1: ∀L,V1,T1,U2. L ⊢ ⓛV1. T1 ➡ U2 → ∀I,W.
 #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_conf … HT2 (L. ⓑ{I} W) ?) -HT2 /2 width=1/ /4 width=5/
+lapply (tpss_lsubs_trans … HT2 (L. ⓑ{I} W) ?) -HT2 /2 width=1/ /4 width=5/
 qed-.
 
 (* Basic_1: was pr2_gen_appl *)
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma
index 91777310c..a7d12a5e2 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma
@@ -35,7 +35,7 @@ fact aaa_ltpr_tpr_conf_aux: ∀L,T,L1,T1,A. L1 ⊢ T1 ⁝ A → L = L1 → T = T
 | #L1 #V1 #T1 #B #A #HB #HA #H1 #H2 #L2 #HL12 #X #H destruct
   elim (tpr_inv_abbr1 … H) -H *
   [ #V2 #T0 #T2 #HV12 #HT10 #HT02 #H destruct
-    lapply (tps_lsubs_conf … HT02 (L2.ⓓV2) ?) -HT02 /2 width=1/ #HT02
+    lapply (tps_lsubs_trans … HT02 (L2.ⓓV2) ?) -HT02 /2 width=1/ #HT02
     lapply (IH … HB … HL12 … HV12) -HB /width=5/ #HB
     lapply (IH … HA … (L2.ⓓV2) … HT10) -IH -HA -HT10 /width=5/ -T1 /2 width=1/ -L1 -V1 /3 width=5/
   | -B #T #HT1 #HTX
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpss.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpss.ma
index ebbc21330..5bb210876 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpss.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpss.ma
@@ -44,16 +44,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_conf … HTT2 (L2. ⓓVV2) ?) -HTT2 /3 width=5/
+  lapply (tpss_lsubs_trans … HTT2 (L2. ⓓVV2) ?) -HTT2 /3 width=5/
 | #I #V1 #V2 #T1 #T2 #U2 #HV12 #_ #HTU2 #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12
   elim (tps_inv_bind1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct
   elim (IHV12 … HVV1 … HL12) -V1 #VV2 #HVV12 #HVV2
   elim (IHT12 … HTT1 (L2. ⓑ{I} VV2) ?) -T1 /2 width=1/ -HL12 #TT2 #HTT12 #HTT2
   elim (tpss_strip_neq … HTT2 … HTU2 ?) -T2 /2 width=1/ #T2 #HTT2 #HUT2
-  lapply (tps_lsubs_conf … HTT2 (L2. ⓑ{I} V2) ?) -HTT2 /2 width=1/ #HTT2
+  lapply (tps_lsubs_trans … HTT2 (L2. ⓑ{I} V2) ?) -HTT2 /2 width=1/ #HTT2
   elim (ltpss_tps_conf … HTT2 (L2. ⓑ{I} VV2) (d + 1) e ?) -HTT2 /2 width=1/ #W2 #HTTW2 #HTW2
-  lapply (tps_lsubs_conf … HTTW2 (⋆. ⓑ{I} VV2) ?) -HTTW2 /2 width=1/ #HTTW2
-  lapply (tpss_lsubs_conf … HTW2 (L2. ⓑ{I} VV2) ?) -HTW2 /2 width=1/ #HTW2
+  lapply (tps_lsubs_trans … HTTW2 (⋆. ⓑ{I} VV2) ?) -HTTW2 /2 width=1/ #HTTW2
+  lapply (tpss_lsubs_trans … HTW2 (L2. ⓑ{I} VV2) ?) -HTW2 /2 width=1/ #HTW2
   lapply (tpss_trans_eq … HUT2 … HTW2) -T2 /3 width=5/
 | #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/lambda_delta/basic_2/static/lsuba.ma b/matita/matita/contribs/lambda_delta/basic_2/static/lsuba.ma
index 1f253774a..aa4800fd5 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/static/lsuba.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/static/lsuba.ma
@@ -19,7 +19,7 @@ include "basic_2/static/aaa.ma".
 inductive lsuba: relation lenv ≝
 | lsuba_atom: lsuba (⋆) (⋆)
 | lsuba_pair: ∀I,L1,L2,V. lsuba L1 L2 → lsuba (L1. ⓑ{I} V) (L2. ⓑ{I} V)
-| lsuba_abbr: ∀L1,L2,V,W,A. L1 ⊢ V ⁝ A → L2 ⊢ W ⁝ A → 
+| lsuba_abbr: ∀L1,L2,V,W,A. L1 ⊢ V ⁝ A → L2 ⊢ W ⁝ A →
               lsuba L1 L2 → lsuba (L1. ⓓV) (L2. ⓛW)
 .
 
diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/lsuba_ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/static/lsuba_ldrop.ma
index 1094133f0..247a8b221 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/static/lsuba_ldrop.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/static/lsuba_ldrop.ma
@@ -19,7 +19,6 @@ include "basic_2/static/lsuba.ma".
 (* Properties concerning basic local environment slicing ********************)
 
 (* Note: the constant 0 cannot be generalized *)
-
 lemma lsuba_ldrop_O1_conf: ∀L1,L2. L1 ⁝⊑ L2 → ∀K1,e. ⇩[0, e] L1 ≡ K1 →
                            ∃∃K2. K1 ⁝⊑ K2 & ⇩[0, e] L2 ≡ K2.
 #L1 #L2 #H elim H -L1 -L2
@@ -41,6 +40,7 @@ lemma lsuba_ldrop_O1_conf: ∀L1,L2. L1 ⁝⊑ L2 → ∀K1,e. ⇩[0, e] L1 ≡
 ]
 qed-.
 
+(* Note: the constant 0 cannot be generalized *)
 lemma lsuba_ldrop_O1_trans: ∀L1,L2. L1 ⁝⊑ L2 → ∀K2,e. ⇩[0, e] L2 ≡ K2 →
                             ∃∃K1. K1 ⁝⊑ K2 & ⇩[0, e] L1 ≡ K1.
 #L1 #L2 #H elim H -L1 -L2
diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma
index 9ab903f1e..29759fe08 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma
@@ -148,13 +148,13 @@ lemma ldrop_O1: ∀L,i. i < |L| → ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V.
   lapply (lt_plus_to_lt_l … H) -H #Hi
   elim (IHL i ?) // /3 width=4/
 ]
-qed.   
+qed.
 
-lemma ldrop_lsubs_ldrop1_abbr: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
-                               ∀K1,V,i. ⇩[0, i] L1 ≡ K1. ⓓV →
+lemma ldrop_lsubs_ldrop2_abbr: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
+                               ∀K2,V,i. ⇩[0, i] L2 ≡ K2. ⓓV →
                                d ≤ i → i < d + e →
-                               ∃∃K2. K1 ≼ [0, d + e - i - 1] K2 &
-                                     ⇩[0, i] L2 ≡ K2. ⓓV.
+                               ∃∃K1. K1 ≼ [0, d + e - i - 1] K2 &
+                                     ⇩[0, i] L1 ≡ K1. ⓓV.
 #L1 #L2 #d #e #H elim H -L1 -L2 -d -e
 [ #d #e #K1 #V #i #H
   lapply (ldrop_inv_atom1 … H) -H #H destruct
diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_sfr.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_sfr.ma
index d8b00df1d..78a15d70d 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_sfr.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_sfr.ma
@@ -20,7 +20,7 @@ include "basic_2/substitution/ldrop_ldrop.ma".
 (* Inversion lemmas about local env. full refinement for substitution *******)
 
 (* Note: ldrop_ldrop not needed *)
-lemma sfr_inv_ldrop: ∀I,L,K,V,i. ⇩[0, i] L ≡ K. ⓑ{I}V → ∀d,e. ≼ [d, e] L →
+lemma sfr_inv_ldrop: ∀I,L,K,V,i. ⇩[0, i] L ≡ K. ⓑ{I}V → ∀d,e. ≽ [d, e] L →
                      d ≤ i → i < d + e → I = Abbr.
 #I #L elim L -L
 [ #K #V #i #H
@@ -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_abbr1 … H ?) -H // -Hide #K #_ #H destruct //
+    elim (lsubs_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
@@ -48,7 +48,7 @@ qed-.
 (* Note: ldrop_ldrop not needed *)
 lemma sfr_ldrop: ∀L,d,e.
                  (∀I,K,V,i. d ≤ i → i < d + e → ⇩[0, i] L ≡ K. ⓑ{I}V → I = Abbr) →
-                 ≼ [d, e] L.
+                 ≽ [d, e] L.
 #L elim L -L //
 #L #I #V #IHL #d @(nat_ind_plus … d) -d
 [ #e @(nat_ind_plus … e) -e //
@@ -58,8 +58,8 @@ lemma sfr_ldrop: ∀L,d,e.
 ]
 qed.
 
-lemma sfr_ldrop_trans_le: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → ∀dd,ee. ≼ [dd, ee] L1 → 
-                          dd + ee ≤ d → ≼ [dd, ee] L2.
+lemma sfr_ldrop_trans_le: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → ∀dd,ee. ≽ [dd, ee] L1 → 
+                          dd + ee ≤ d → ≽ [dd, ee] L2.
 #L1 #L2 #d #e #HL12 #dd #ee #HL1 #Hddee
 @sfr_ldrop #I #K2 #V2 #i #Hddi #Hiddee #HLK2
 lapply (lt_to_le_to_lt … Hiddee Hddee) -Hddee #Hid
@@ -69,9 +69,9 @@ elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K1 #V1 #HK12 #HV21 #H destru
 qed.
 
 lemma sfr_ldrop_trans_be_up: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 →
-                             ∀dd,ee. ≼ [dd, ee] L1 →
+                             ∀dd,ee. ≽ [dd, ee] L1 →
                              dd ≤ d + e → d + e ≤ dd + ee →
-                             ≼ [d, dd + ee - d - e] L2.
+                             ≽ [d, dd + ee - d - e] L2.
 #L1 #L2 #d #e #HL12 #dd #ee #HL1 #Hdde #Hddee
 @sfr_ldrop #I #K2 #V2 #i #Hdi #Hiddee #HLK2
 lapply (transitive_le ? ? (i+e)… Hdde ?) -Hdde /2 width=1/ #Hddie
@@ -80,8 +80,8 @@ lapply (ldrop_trans_ge … HL12 … HLK2 ?) -L2 // -Hdi  #HL1K2
 @(sfr_inv_ldrop … HL1K2 … HL1) -L1 >commutative_plus // -Hddie /2 width=1/
 qed.
 
-lemma sfr_ldrop_trans_ge: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → ∀dd,ee. ≼ [dd, ee] L1 → 
-                          d + e ≤ dd → ≼ [dd - e, ee] L2.
+lemma sfr_ldrop_trans_ge: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → ∀dd,ee. ≽ [dd, ee] L1 → 
+                          d + e ≤ dd → ≽ [dd - e, ee] L2.
 #L1 #L2 #d #e #HL12 #dd #ee #HL1 #Hddee
 @sfr_ldrop #I #K2 #V2 #i #Hddi #Hiddee #HLK2
 elim (le_inv_plus_l … Hddee) -Hddee #Hdde #Hedd
diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/lsubs.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/lsubs.ma
index fb6468c90..f27883b02 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/substitution/lsubs.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/lsubs.ma
@@ -22,7 +22,7 @@ inductive lsubs: nat → nat → relation lenv ≝
 | 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. ⓛV1) (L2.ⓑ{I} V2)
+              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)
 .
@@ -31,9 +31,9 @@ interpretation
   "local environment refinement (substitution)"
   'SubEq L1 d e L2 = (lsubs d e L1 L2).
 
-definition lsubs_conf: ∀S. (lenv → relation S) → Prop ≝ λS,R.
-                       ∀L1,s1,s2. R L1 s1 s2 →
-                       ∀L2,d,e. L1 ≼ [d, e] L2 → R L2 s1 s2.
+definition lsubs_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 *********************************************************)
 
@@ -48,7 +48,7 @@ lemma lsubs_abbr_lt: ∀L1,L2,V,e. L1 ≼ [0, e - 1] L2 → 0 < e →
 qed.
 
 lemma lsubs_abst_lt: ∀L1,L2,I,V1,V2,e. L1 ≼ [0, e - 1] L2 → 0 < e →
-                     L1. ⓛV1 ≼ [0, e] L2.ⓑ{I} V2.
+                     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.
 
@@ -58,7 +58,7 @@ lemma lsubs_skip_lt: ∀L1,L2,d,e. L1 ≼ [d - 1, e] L2 → 0 < d →
 qed.
 
 lemma lsubs_bind_lt: ∀I,L1,L2,V,e. L1 ≼ [0, e - 1] L2 → 0 < e → 
-                     L1. ⓑ{I}V ≼ [0, e] L2.ⓓV.
+                     L1. ⓓV ≼ [0, e] L2. ⓑ{I}V.
 * /2 width=1/ qed.
 
 lemma lsubs_refl: ∀d,e,L. L ≼ [d, e] L.
@@ -68,7 +68,7 @@ lemma lsubs_refl: ∀d,e,L. L ≼ [d, e] L.
 ]
 qed.
 
-lemma TC_lsubs_conf: ∀S,R. lsubs_conf S R → lsubs_conf S (λL. (TC … (R L))).
+lemma TC_lsubs_trans: ∀S,R. lsubs_trans S R → lsubs_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
@@ -93,9 +93,43 @@ lemma lsubs_inv_atom1: ∀L2,d,e. ⋆ ≼ [d, e] L2 →
                        L2 = ⋆ ∨ (d = 0 ∧ e = 0).
 /2 width=3/ qed-.
 
-fact lsubs_inv_abbr1_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
-                          ∀K1,V. L1 = K1.ⓓV → d = 0 → 0 < e →
-                          ∃∃K2. K1 ≼ [0, e - 1] K2 & L2 = K2.ⓓV.
+fact lsubs_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
+[ #d #e #I1 #K1 #V1 #H destruct
+| #L1 #L2 #I1 #K1 #V1 #_ #H
+  elim (lt_zero_false … H)
+| #L1 #L2 #W #e #_ #I1 #K1 #V1 #_ #H
+  elim (lt_zero_false … H)
+| #L1 #L2 #I #W1 #W2 #e #_ #I1 #K1 #V1 #_ #H
+  elim (lt_zero_false … H)
+| #L1 #L2 #J1 #J2 #W1 #W2 #d #e #HL12 #I1 #K1 #V1 #H #_ destruct /2 width=5/
+]
+qed.
+
+lemma lsubs_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 = ⋆ →
+                          L1 = ⋆ ∨ (d = 0 ∧ e = 0).
+#L1 #L2 #d #e * -L1 -L2 -d -e
+[ /2 width=1/
+| /3 width=1/
+| #L1 #L2 #W #e #_ #H destruct
+| #L1 #L2 #I #W1 #W2 #e #_ #H destruct
+| #L1 #L2 #I1 #I2 #W1 #W2 #d #e #_ #H destruct
+]
+qed.
+
+lemma lsubs_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 →
+                          ∀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
 [ #d #e #K1 #V #H destruct
 | #L1 #L2 #K1 #V #_ #_ #H
@@ -106,13 +140,13 @@ fact lsubs_inv_abbr1_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
 ]
 qed.
 
-lemma lsubs_inv_abbr1: ∀K1,L2,V,e. K1.ⓓV ≼ [0, e] L2 → 0 < e →
-                       ∃∃K2. K1 ≼ [0, e - 1] K2 & L2 = K2.ⓓV.
+lemma lsubs_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_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.
+fact lsubs_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
 [ #d #e #I1 #K1 #V1 #H destruct
 | #L1 #L2 #I1 #K1 #V1 #_ #H
@@ -125,8 +159,8 @@ 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 →
-                       ∃∃I2,K2,V2. K1 ≼ [d - 1, e] K2 & L2 = K2.ⓑ{I2}V2.
+lemma lsubs_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 *****************************************************)
diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/lsubs_sfr.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/lsubs_sfr.ma
index fb71a175c..2b71621fa 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/substitution/lsubs_sfr.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/lsubs_sfr.ma
@@ -16,53 +16,53 @@ include "basic_2/substitution/lsubs.ma".
 
 (* LOCAL ENVIRONMENT REFINEMENT FOR SUBSTITUTION ****************************)
 
-(* top element of the refinement *)
+(* bottom element of the refinement *)
 definition sfr: nat → nat → predicate lenv ≝
-   λd,e. NF … (lsubs d e) (lsubs d e …).
+   λd,e. NF_sn … (lsubs d e) (lsubs d e …).
 
 interpretation
    "local environment full refinement (substitution)"
-   'SubEqTop d e L = (sfr d e L).
+   'SubEqBottom d e L = (sfr d e L).
 
 (* Basic properties *********************************************************)
 
-lemma sfr_atom: ∀d,e. ≼ [d, e] ⋆.
+lemma sfr_atom: ∀d,e. ≽ [d, e] ⋆.
 #d #e #L #H
-elim (lsubs_inv_atom1 … H) -H
+elim (lsubs_inv_atom2 … H) -H
 [ #H destruct //
 | * #H1 #H2 destruct //
 ]
 qed.
 
-lemma sfr_OO: ∀L. ≼ [0, 0] L.
+lemma sfr_OO: ∀L. ≽ [0, 0] L.
 // qed.
 
-lemma sfr_abbr: ∀L,V,e. ≼ [0, e] L → ≼ [0, e + 1] L.ⓓV.
+lemma sfr_abbr: ∀L,V,e. ≽ [0, e] L → ≽ [0, e + 1] L.ⓓV.
 #L #V #e #HL #K #H
-elim (lsubs_inv_abbr1 … H ?) -H // <minus_plus_m_m #X #HLX #H destruct
+elim (lsubs_inv_abbr2 … H ?) -H // <minus_plus_m_m #X #HLX #H destruct
 lapply (HL … HLX) -HL -HLX /2 width=1/
 qed.
 
-lemma sfr_skip: ∀I,L,V,d,e. ≼ [d, e] L → ≼ [d + 1, e] L.ⓑ{I}V.
+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_skip1 … H ?) -H // <minus_plus_m_m #J #X #W #HLX #H destruct
+elim (lsubs_inv_skip2 … H ?) -H // <minus_plus_m_m #J #X #W #HLX #H destruct
 lapply (HL … HLX) -HL -HLX /2 width=1/
 qed.
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma sfr_inv_bind: ∀I,L,V,e. ≼ [0, e] L.ⓑ{I}V → 0 < e →
-                    ≼ [0, e - 1] L ∧ I = Abbr.
+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_abbr1 … H ?) -H // #K #_ #H destruct
+elim (lsubs_inv_abbr2 … H ?) -H // #K #_ #H destruct
 @conj // #L #HKL
 lapply (HL (L.ⓓV) ?) -HL /2 width=1/ -HKL #H
-elim (lsubs_inv_abbr1 … H ?) -H // -He #X #HLX #H destruct //
+elim (lsubs_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.
+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_skip1 … H ?) -H // -Hd #J #X #W #HKX #H destruct //
+elim (lsubs_inv_skip2 … H ?) -H // -Hd #J #X #W #HKX #H destruct //
 qed-.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/tps.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/tps.ma
index f1cc2d9ee..d284060f1 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/substitution/tps.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/tps.ma
@@ -34,12 +34,12 @@ interpretation "parallel substritution (term)"
 
 (* Basic properties *********************************************************)
 
-lemma tps_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶ [d, e] T2 →
-                      ∀L2. L1 ≼ [d, e] L2 → L2 ⊢ T1 ▶ [d, e] T2.
+lemma tps_lsubs_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_ldrop1_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /2 width=4/
+  elim (ldrop_lsubs_ldrop2_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /2 width=4/
 | /4 width=1/
 | /3 width=1/
 ]
@@ -115,7 +115,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_conf … HT1 (L. ⓑ{I} V) ?) -HT1 /3 width=5/
+  lapply (tps_lsubs_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/
@@ -138,7 +138,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_conf … HT1 (L. ⓑ{I} V) ?) -HT1 /3 width=5/
+  lapply (tps_lsubs_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/lambda_delta/basic_2/substitution/tps_tps.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/tps_tps.ma
index 98f34529b..6bbb15a76 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/substitution/tps_tps.ma
+++ b/matita/matita/contribs/lambda_delta/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 #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_conf … HT02 (L. ⓑ{I} V1) ?) -HT02 /2 width=1/ #HT02
+  lapply (tps_lsubs_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_conf … HT1 (L. ⓑ{I} V) ?) -HT1 /2 width=1/
-  lapply (tps_lsubs_conf … HT2 (L. ⓑ{I} V) ?) -HT2 /3 width=5/
+  lapply (tps_lsubs_trans … HT1 (L. ⓑ{I} V) ?) -HT1 /2 width=1/
+  lapply (tps_lsubs_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_conf … HT1 (L2. ⓑ{I} V) ?) -HT1 /2 width=1/
-    lapply (tps_lsubs_conf … HT2 (L1. ⓑ{I} V) ?) -HT2 /2 width=1/ /3 width=5/
+    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/
   | -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 #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_conf … HT02 (L. ⓑ{I} V0) ?) -HT02 /2 width=1/ #HT02
+  lapply (tps_lsubs_trans … HT02 (L. ⓑ{I} V0) ?) -HT02 /2 width=1/ #HT02
   lapply (IHT10 … HT02 He) -T0 #HT12
-  lapply (tps_lsubs_conf … HT12 (L. ⓑ{I} V2) ?) -HT12 /2 width=1/ /3 width=1/
+  lapply (tps_lsubs_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 /4 width=4/
 | #L #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_conf … HT02 (L. ⓑ{I} V0) ?) -HT02 /2 width=1/ #HT02
+  lapply (tps_lsubs_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_conf … HT1 (L. ⓑ{I} V) ?) -HT1 /2 width=1/
-  lapply (tps_lsubs_conf … HT2 (L. ⓑ{I} V2) ?) -HT2 /2 width=1/ /3 width=6/
+  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/
 | #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/lambda_delta/basic_2/unfold/delift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma
index 82cd0c87f..2608f02ce 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma
@@ -31,8 +31,8 @@ lemma lift_delift: ∀T1,T2,d,e. ⇧[d, e] T1 ≡ T2 →
 lemma delift_refl_O2: ∀L,T,d. L ⊢ T ▼*[d, 0] ≡ T.
 /2 width=3/ qed.
 
-lemma delift_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▼*[d, e] ≡ T2 →
-                         ∀L2. L1 ≼ [d, e] L2 → L2 ⊢ T1 ▼*[d, e] ≡ T2.
+lemma delift_lsubs_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 * /3 width=3/
 qed.
 
@@ -52,7 +52,7 @@ lemma delift_bind: ∀I,L,V1,V2,T1,T2,d,e.
                    L ⊢ V1 ▼*[d, e] ≡ V2 → L. ⓑ{I} V2 ⊢ T1 ▼*[d+1, e] ≡ T2 →
                    L ⊢ ⓑ{I} V1. T1 ▼*[d, e] ≡ ⓑ{I} V2. T2.
 #I #L #V1 #V2 #T1 #T2 #d #e * #V #HV1 #HV2 * #T #HT1 #HT2
-lapply (tpss_lsubs_conf … HT1 (L. ⓑ{I} V) ?) -HT1 /2 width=1/ /3 width=5/
+lapply (tpss_lsubs_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: ∀I,L,V1,T1,U2,d,e. L ⊢ ⓑ{I} V1. T1 ▼*[d, e] ≡
 #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_conf … HT1 (L. ⓑ{I} V2) ?) -HT1 /2 width=1/ /3 width=5/
+lapply (tpss_lsubs_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 ⊢ ⓕ{I} V1. T1 ▼*[d, e] ≡ U2 →
diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_alt.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_alt.ma
index 0cc9f55b5..4332ec249 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_alt.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_alt.ma
@@ -38,11 +38,11 @@ interpretation "inverse basic relocation (term) alternative"
 
 (* Basic properties *********************************************************)
 
-lemma delifta_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▼▼*[d, e] ≡ T2 →
-                          ∀L2. L1 ≼ [d, e] L2 → L2 ⊢ T1 ▼▼*[d, e] ≡ T2.
+lemma delifta_lsubs_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 // /2 width=1/
 [ #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
-  elim (ldrop_lsubs_ldrop1_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /3 width=6/
+  elim (ldrop_lsubs_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 ⊢ T1 ▼*[d, e] ≡ T2 → L ⊢ T1 
   ]
 | * #I #V1 #T1 #_ #_ #IH #X #d #e #H
   [ elim (delift_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
-    lapply (delift_lsubs_conf … HT12 (L.ⓑ{I}V1) ?) -HT12 /2 width=1/ #HT12
+    lapply (delift_lsubs_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_conf … HT12 (L.ⓑ{I}V2) ?) -HT12 /2 width=1/
+    lapply (delifta_lsubs_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/lambda_delta/basic_2/unfold/ltpss_ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ltpss.ma
index ac4d17815..1d1d91018 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ltpss.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ltpss.ma
@@ -59,10 +59,10 @@ fact ltpss_tpss_trans_eq_aux: ∀Y1,X2,L1,T2,U2,d,e.
   lapply (IH … HV02 … HK01 ? ?) -IH -HV02 -HK01
   [1,3: // |2,4: skip | normalize /2 width=1/ | /2 width=6/ ]
 | #L #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #_ #_ #L0 #HL0 #H1 #H2 destruct
-  lapply (tpss_lsubs_conf … HT12 (L. ⓑ{I} V1) ?) -HT12 /2 width=1/ #HT12
+  lapply (tpss_lsubs_trans … HT12 (L. ⓑ{I} V1) ?) -HT12 /2 width=1/ #HT12
   lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3: // |2,4: skip |5: /2 width=2/ ] #HV12
   lapply (IH … HT12 (L0. ⓑ{I} V1) ? ? ?) -IH -HT12 [1,3,5: /2 width=2/ |2,4: skip | normalize // ] -HL0 #HT12
-  lapply (tpss_lsubs_conf … HT12 (L0. ⓑ{I} V2) ?) -HT12 /2 width=1/
+  lapply (tpss_lsubs_trans … HT12 (L0. ⓑ{I} V2) ?) -HT12 /2 width=1/
 | #L #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #_ #_ #L0 #HL0 #H1 #H2 destruct
   lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3: // |2,4: skip |5: /2 width=3/ ]
   lapply (IH … HT12 … HL0 ? ?) -IH -HT12 [1,3,5: normalize // |2,4: skip ] -HL0 /2 width=1/
diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma
index 7631985bb..0e98ece73 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma
@@ -44,8 +44,8 @@ lemma tpss_strap: ∀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_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶* [d, e] T2 →
-                       ∀L2. L1 ≼ [d, e] L2 → L2 ⊢ T1 ▶* [d, e] T2.
+lemma tpss_lsubs_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.
 
 lemma tpss_refl: ∀d,e,L,T. L ⊢ T ▶* [d, e] T.
@@ -60,7 +60,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 #I #T1 #T2 #HT12
-  lapply (tpss_lsubs_conf … HT12 (L. ⓑ{I} V) ?) -HT12 /2 width=1/ #HT12
+  lapply (tpss_lsubs_trans … HT12 (L. ⓑ{I} V) ?) -HT12 /2 width=1/ #HT12
   lapply (IHV … HT12) -IHV -HT12 #HT12 @step /2 width=5/ (**) (* /3 width=5/ is too slow *)
 ]
 qed.
@@ -132,7 +132,7 @@ lemma tpss_inv_bind1: ∀d,e,L,I,V1,T1,U2. L ⊢ ⓑ{I} V1. T1 ▶* [d, e] U2 
 [ /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_conf … HT1 (L. ⓑ{I} V2) ?) -HT1 /2 width=1/ /3 width=5/
+  lapply (tpss_lsubs_trans … HT1 (L. ⓑ{I} V2) ?) -HT1 /2 width=1/ /3 width=5/
 ]
 qed-.
 
diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_alt.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_alt.ma
index 0a5a5c290..30b7e80ac 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_alt.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_alt.ma
@@ -35,12 +35,12 @@ interpretation "parallel unfold (term) alternative"
 
 (* Basic properties *********************************************************)
 
-lemma tpssa_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶▶* [d, e] T2 →
-                        ∀L2. L1 ≼ [d, e] L2 → L2 ⊢ T1 ▶▶* [d, e] T2.
+lemma tpssa_lsubs_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_ldrop1_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /3 width=6/
+  elim (ldrop_lsubs_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 #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_conf … HT2 (L.ⓑ{I}V) ?) -HT2 /2 width=1/ #HT2
+  lapply (tps_lsubs_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_conf … HT12 (L.ⓑ{I}V2) ?) -HT12 /2 width=1/
+  lapply (tpssa_lsubs_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/lambda_delta/ground_2/star.ma b/matita/matita/contribs/lambda_delta/ground_2/star.ma
index c951ddac0..18f028acc 100644
--- a/matita/matita/contribs/lambda_delta/ground_2/star.ma
+++ b/matita/matita/contribs/lambda_delta/ground_2/star.ma
@@ -110,3 +110,16 @@ lemma NF_to_SN: ∀A,R,S,a. NF A R S a → SN A R S a.
 @SN_intro #a2 #HRa12 #HSa12
 elim (HSa12 ?) -HSa12 /2 width=1/
 qed.
+
+definition NF_sn: ∀A. relation A → relation A → predicate A ≝
+   λA,R,S,a2. ∀a1. R a1 a2 → S a2 a1.
+
+inductive SN_sn (A) (R,S:relation A): predicate A ≝
+| SN_sn_intro: ∀a2. (∀a1. R a1 a2 → (S a2 a1 → ⊥) → SN_sn A R S a1) → SN_sn A R S a2
+.
+
+lemma NF_to_SN_sn: ∀A,R,S,a. NF_sn A R S a → SN_sn A R S a.
+#A #R #S #a2 #Ha2
+@SN_sn_intro #a1 #HRa12 #HSa12
+elim (HSa12 ?) -HSa12 /2 width=1/
+qed.
diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml
index ad10ca4ad..0fd1dcd32 100644
--- a/matita/matita/predefined_virtuals.ml
+++ b/matita/matita/predefined_virtuals.ml
@@ -1524,7 +1524,8 @@ let predefined_classes = [
  ["}"; "❵"; "⦄" ] ;
  ["□"; "◽"; "▪"; "◾"; ];
  ["◊"; "♢"; "⧫"; "♦"; "⟐"; "⟠"; ] ;
- [">"; "〉"; "»"; "❭"; "❯"; "❱"; "▸"; "►"; "▶"; ] ;       
+ [">"; "〉"; "»"; "❭"; "❯"; "❱"; "▸"; "►"; "▶"; ] ;
+ ["≥"; "≽"; ]; 
  ["a"; "α"; "𝕒"; "𝐚"; "𝛂"; "ⓐ"; ] ;
  ["A"; "ℵ"; "𝔸"; "𝐀"; "Ⓐ"; ] ;
  ["b"; "β"; "ß"; "𝕓"; "𝐛"; "𝛃"; "ⓑ"; ] ;
-- 
2.39.2