From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 16 May 2013 14:35:06 +0000 (+0000)
Subject: - some renaming
X-Git-Tag: make_still_working~1154
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=947126ce0618ffdfc39cdc7e198c1edbf3b1a926;p=helm.git

- some renaming
- finally we issue the "dynamic" component
---

diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/notation.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/notation.ma
index 1c60d6c18..f830afff1 100644
--- a/matita/matita/contribs/lambdadelta/apps_2/functional/notation.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/functional/notation.ma
@@ -14,6 +14,10 @@
 
 (* NOTATION FOR THE "functional" COMPONENT ********************************)
 
+notation "hvbox( T . break ④ { term 46 I } break { term 46 T1 , break term 46 T2 , break term 46 T3 } )"
+ non associative with precedence 50
+ for @{ 'DxItem4 $T $I $T1 $T2 $T3 }.
+
 notation "hvbox( ↑ [ term 46 d , break term 46 e ] break term 46 T )"
    non associative with precedence 46
    for @{ 'Lift $d $e $T }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_dxprs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_dxprs.ma
index 9666bffdd..04af871fe 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_dxprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_dxprs.ma
@@ -19,9 +19,9 @@ include "basic_2/dynamic/lsubsv_ssta.ma".
 
 (* Properties for the preservation results **********************************)
 
-fact sstas_lsubsv_aux: ∀h,g,L0,T0.
-                       (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) →
-                       (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) →
+fact lsubsv_sstas_aux: ∀h,g,L0,T0.
+                       (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) →
+                       (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) →
                        (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) →
                        (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_lsubsv h g L1 T1) →
                        ∀L2,T. h ⊢ ⦃L0, T0⦄ >[g] ⦃L2, T⦄ → ⦃h, L2⦄ ⊢ T ¡[g] →
@@ -35,14 +35,14 @@ lapply (snv_sstas_aux … IH2 … HTU2) // #H
 lapply (IH1 … H … HL12) [ /3 width=4 by ygt_yprs_trans, sstas_yprs/ ] -H #HU2
 elim (snv_fwd_ssta … HU1) #l1 #W1 #HUW1
 elim (lsubsv_ssta_trans … HU2W … HL12) -HU2W #W2 #HUW2 #HW2
-elim (ssta_ltpr_cpcs_aux … IH4 IH3 … HU1 HU2 … HUW1 … HUW2 … HU12) -HU1 -HU2 -HUW2 -HU12 //
+elim (ssta_cpcs_lpr_aux … IH4 IH3 … HU1 HU2 … HUW1 … HUW2 … HU12 L1) -HU1 -HU2 -HUW2 -HU12 //
 [2,3: /4 width=4 by ygt_yprs_trans, sstas_yprs, lsubsv_yprs/ ] -L2 -L0 -T0 -U2 #H #HW12 destruct
 lapply (cpcs_trans … HW12 … HW2) -W2 /3 width=4/
 qed-.
 
-fact dxprs_lsubsv_aux: ∀h,g,L0,T0.
-                       (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) →
-                       (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) →
+fact lsubsv_dxprs_aux: ∀h,g,L0,T0.
+                       (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) →
+                       (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) →
                        (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) →
                        (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_lsubsv h g L1 T1) →
                        ∀L2,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L2, T1⦄ → ⦃h, L2⦄ ⊢ T1 ¡[g] →
@@ -50,7 +50,7 @@ fact dxprs_lsubsv_aux: ∀h,g,L0,T0.
                        ∃∃T. ⦃h, L1⦄ ⊢ T1 •*➡*[g] T & L1 ⊢ T2 ➡* T.
 #h #g #L0 #T0 #IH4 #IH3 #IH2 #IH1 #L2 #T1 #HLT0 #HT1 #L1 #HL12 #T2 * #T #HT1T #HTT2
 lapply (lsubsv_cprs_trans … HL12 … HTT2) -HTT2 #HTT2
-elim (sstas_lsubsv_aux … IH4 IH3 IH2 IH1 … HLT0 … HL12 … HT1T) // -L2 -L0 -T0 #T0 #HT10 #HT0
+elim (lsubsv_sstas_aux … IH4 IH3 IH2 IH1 … HLT0 … HL12 … HT1T) // -L2 -L0 -T0 #T0 #HT10 #HT0
 lapply (cpcs_cprs_strap1 … HT0 … HTT2) -T #HT02
 elim (cpcs_inv_cprs … HT02) -HT02 /3 width=3/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma
index 1482dd986..896875371 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma
@@ -22,8 +22,8 @@ include "basic_2/dynamic/lsubsv_cpcs.ma".
 (* Properties concerning stratified native validity *************************)
 
 fact snv_lsubsv_aux: ∀h,g,L0,T0.
-                     (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) →
-                     (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) →
+                     (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) →
+                     (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) →
                      (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) →
                      (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_lsubsv h g L1 T1) →
                      ∀L1,T1. L0 = L1 → T0 = T1 → IH_snv_lsubsv h g L1 T1.
@@ -45,8 +45,8 @@ fact snv_lsubsv_aux: ∀h,g,L0,T0.
   lapply (lsubsv_cprs_trans … HL12 … HW0) -HW0 #HW0
   elim (lsubsv_ssta_trans … HVW … HL12) -HVW #W1 #HVW1 #HW1
   lapply (cpcs_cprs_strap1 … HW1 … HW0) -W #HW10
-  elim (dxprs_lsubsv_aux … IH4 IH3 IH2 IH1 … HL12 … HTU) -IH4 -IH3 -IH2 -HTU // /2 width=1/ #X #HTU #H
-  elim (cprs_inv_abst1 Abst W0 … H) -H #W #U2 #HW0 #HU2 #H destruct
+  elim (lsubsv_dxprs_aux … IH4 IH3 IH2 IH1 … HL12 … HTU) -IH4 -IH3 -IH2 -HTU // /2 width=1/ #X #HTU #H
+  elim (cprs_fwd_abst1 … H Abst W0) -H #W #U2 #HW0 #HU2 #H destruct
   lapply (cpcs_cprs_strap1 … HW10 … HW0) -W0 #H
   elim (cpcs_inv_cprs … H) -H #W0 #HW10 #HW0
   lapply (dxprs_cprs_trans … (ⓛ{a}W0.U2) HTU ?) [ /2 width=1/ ] -HTU -HW0
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma
index 643bf6569..f00ae1832 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma
@@ -29,11 +29,11 @@ definition IH_ssta_cpr_lpr: ∀h:sh. sd h → relation2 lenv term ≝
                             λh,g,L1,T1. ⦃h, L1⦄ ⊢ T1 ¡[g] →
                             ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l, U1⦄ →
                             ∀T2. L1 ⊢ T1 ➡ T2 → ∀L2. L1 ⊢ ➡ L2 →
-                            ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l, U2⦄ & L1 ⊢ U1 ⬌* U2.
+                            ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l, U2⦄ & L2 ⊢ U1 ⬌* U2.
 
 definition IH_snv_ssta: ∀h:sh. sd h → relation2 lenv term ≝
-                        λh,g,L1,T1. ⦃h, L1⦄ ⊢ T1 ¡[g] →
-                        ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l+1, U1⦄ → ⦃h, L1⦄ ⊢ U1 ¡[g].
+                        λh,g,L,T. ⦃h, L⦄ ⊢ T ¡[g] →
+                        ∀U,l. ⦃h, L⦄ ⊢ T •[g] ⦃l+1, U⦄ → ⦃h, L⦄ ⊢ U ¡[g].
 
 definition IH_snv_lsubsv: ∀h:sh. sd h → relation2 lenv term ≝
                           λh,g,L2,T. ⦃h, L2⦄ ⊢ T ¡[g] →
@@ -55,41 +55,51 @@ fact ssta_cprs_lpr_aux: ∀h,g,L0,T0.
                         (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) →
                         ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[g] →
                         ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l, U1⦄ →
-                        ∀T2. L1 ⊢ T1 ➡* T2 → ∀L2. L1 ⊢ ➡ L2 → 
-                        ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l, U2⦄ & L1 ⊢ U1 ⬌* U2.
+                        ∀T2. L1 ⊢ T1 ➡* T2 → ∀L2. L1 ⊢ ➡ L2 →
+                        ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l, U2⦄ & L2 ⊢ U1 ⬌* U2.
 #h #g #L0 #T0 #IH2 #IH1 #L1 #T1 #H01 #HT1 #U1 #l #HTU1 #T2 #H
-elim H -T2 [ /2 width=5/ ]
+elim H -T2 [ /2 width=7/ ]
 #T #T2 #HT1T #HTT2 #IHT1 #L2 #HL12
 elim (IHT1 L1) // -IHT1 #U #HTU #HU1
-elim (IH1 … HTU … HTT2 … HL12) -IH1 -HTU -HTT2 -HL12
+elim (IH1 … HTU … HTT2 … HL12) -IH1 -HTU -HTT2
 [2: /3 width=9 by snv_cprs_lpr_aux/
 |3: /5 width=6 by ygt_yprs_trans, cprs_yprs/
 ] -L0 -T0 -T1 -T #U2 #HTU2 #HU2
+lapply (cpcs_lpr_conf … HL12 … HU1) -L1 #HU1
 lapply (cpcs_trans … HU1 … HU2) -U /2 width=3/
 qed-.
 
-fact ssta_cpcs_aux: ∀h,g,L0,T0.
-                    (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) →
-                    (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) →
-                    ∀L,T1,T2. h ⊢ ⦃L0, T0⦄ >[g] ⦃L, T1⦄ → h ⊢ ⦃L0, T0⦄ >[g] ⦃L, T2⦄ →
-                        ⦃h, L⦄ ⊢ T1 ¡[g] → ⦃h, L⦄ ⊢ T2 ¡[g] →
-                    ∀U1,l1. ⦃h, L⦄ ⊢ T1 •[g] ⦃l1, U1⦄ →
-                    ∀U2,l2. ⦃h, L⦄ ⊢ T2 •[g] ⦃l2, U2⦄ →
-                    L ⊢ T1 ⬌* T2 → l1 = l2 ∧ L ⊢ U1 ⬌* U2.
-#h #g #L0 #T0 #IH2 #IH1 #L #T1 #T2 #HLT01 #HLT02 #HT1 #HT2 #U1 #l1 #HTU1 #U2 #l2 #HTU2 #H
+fact ssta_cpcs_lpr_aux: ∀h,g,L0,T0.
+                        (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) →
+                        (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) →
+                        ∀L1,T1,T2. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T2⦄ →
+                        ⦃h, L1⦄ ⊢ T1 ¡[g] → ⦃h, L1⦄ ⊢ T2 ¡[g] →
+                        ∀U1,l1. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l1, U1⦄ →
+                        ∀U2,l2. ⦃h, L1⦄ ⊢ T2 •[g] ⦃l2, U2⦄ →
+                        L1 ⊢ T1 ⬌* T2 → ∀L2. L1 ⊢ ➡ L2 →
+                        l1 = l2 ∧ L2 ⊢ U1 ⬌* U2.
+#h #g #L0 #T0 #IH2 #IH1 #L1 #T1 #T2 #H01 #H02 #HT1 #HT2 #U1 #l1 #HTU1 #U2 #l2 #HTU2 #H #L2 #HL12
 elim (cpcs_inv_cprs … H) -H #T #H1 #H2
-elim (ssta_cprs_lpr_aux … HLT01 HT1 … HTU1 … H1 L) -T1 // /2 width=1/ #W1 #H1 #HUW1
-elim (ssta_cprs_lpr_aux … HLT02 HT2 … HTU2 … H2 L) -T2 // /2 width=1/ #W2 #H2 #HUW2 -L0 -T0
+elim (ssta_cprs_lpr_aux … H01 HT1 … HTU1 … H1 … HL12) -T1 /2 width=1/ #W1 #H1 #HUW1
+elim (ssta_cprs_lpr_aux … H02 HT2 … HTU2 … H2 … HL12) -T2 /2 width=1/ #W2 #H2 #HUW2 -L0 -T0
 elim (ssta_mono … H1 … H2) -h -T #H1 #H2 destruct
 lapply (cpcs_canc_dx … HUW1 … HUW2) -W2 /2 width=1/
 qed-.
 
 fact snv_sstas_aux: ∀h,g,L0,T0.
                     (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) →
-                    ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[g] →
-                    ∀U1. ⦃h, L1⦄ ⊢ T1 •*[g] U1 → ⦃h, L1⦄ ⊢ U1 ¡[g].
-#h #g #L0 #T0 #IH #L1 #T1 #HLT0 #HT1 #U1 #H
-@(sstas_ind … H) -U1 // -HT1 /4 width=5 by ygt_yprs_trans, sstas_yprs/
+                    ∀L,T. h ⊢ ⦃L0, T0⦄ >[g] ⦃L, T⦄ → ⦃h, L⦄ ⊢ T ¡[g] →
+                    ∀U. ⦃h, L⦄ ⊢ T •*[g] U → ⦃h, L⦄ ⊢ U ¡[g].
+#h #g #L0 #T0 #IH #L #T #H01 #HT #U #H
+@(sstas_ind … H) -U // -HT /4 width=5 by ygt_yprs_trans, sstas_yprs/
+qed-.
+
+fact snv_sstas_lpr_aux: ∀h,g,L0,T0.
+                        (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) →
+                        (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) →
+                        ∀L1,T. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T⦄ → ⦃h, L1⦄ ⊢ T ¡[g] →
+                        ∀U. ⦃h, L1⦄ ⊢ T •*[g] U → ∀L2. L1 ⊢ ➡ L2 → ⦃h, L2⦄ ⊢ U ¡[g].
+/4 width=7 by snv_sstas_aux, ygt_yprs_trans, sstas_yprs/
 qed-.
 
 fact sstas_cprs_lpr_aux: ∀h,g,L0,T0.
@@ -97,45 +107,50 @@ fact sstas_cprs_lpr_aux: ∀h,g,L0,T0.
                          (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) →
                          (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) →
                          ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[g] →
-                         ∀T2. L1 ⊢ T1 ➡* T2 → ∀U1. ⦃h, L1⦄ ⊢ T1 •*[g] U1 → ∀L2. L1 ⊢ ➡ L2 →
-                         ∃∃U2. ⦃h, L2⦄ ⊢ T2 •*[g] U2 & L1 ⊢ U1 ⬌* U2.
-#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 #T1 #H01 #HT1 #L2 #HL12 #T2 #HT12 #U1 #H
-@(sstas_ind … H) -U1 [ /3 width=3/ ]
-#U1 #W1 #l1 #HTU1 #HUW1 * #U2 #HTU2 #HU12
-lapply (snv_ltpr_cprs_aux … IH2 … HT1 … HT12) // #HT2
+                         ∀U1. ⦃h, L1⦄ ⊢ T1 •*[g] U1 → ∀T2. L1 ⊢ T1 ➡* T2 → ∀L2. L1 ⊢ ➡ L2 →
+                         ∃∃U2. ⦃h, L2⦄ ⊢ T2 •*[g] U2 & L2 ⊢ U1 ⬌* U2.
+#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 #T1 #H01 #HT1 #U1 #H
+@(sstas_ind … H) -U1 [ /3 width=5 by cprs_lpr_conf, ex2_intro/ ]
+#U1 #W1 #l1 #HTU1 #HUW1 #IHTU1 #T2 #HT12 #L2 #HL12
+elim (IHTU1 … HT12 … HL12) -IHTU1 #U2 #HTU2 #HU12
+lapply (snv_cprs_lpr_aux … IH2 … HT1 … HT12 … HL12) // #HT2
 elim (snv_sstas_fwd_correct … HTU2) // #W2 #l2 #HUW2
-elim (ssta_ltpr_cpcs_aux … IH2 IH1 … HUW1 … HUW2 … HU12) -IH2 -IH1 -HUW1 -HU12 //
-[2: /4 width=8 by snv_sstas_aux, ygt_yprs_trans, ltpr_cprs_yprs/
-|3: /3 width=7 by snv_sstas_aux, ygt_yprs_trans, cprs_yprs/
-|4: /4 width=5 by ygt_yprs_trans, ltpr_cprs_yprs, sstas_yprs/
-|5: /3 width=4 by ygt_yprs_trans, cprs_yprs, sstas_yprs/
-] -L0 -T0 -T1 -HT2 #H #HW12 destruct /3 width=4/
+elim (IH1 … HUW1 U1 … HL12) -HUW1 //
+[2: /3 width=7 by snv_sstas_aux/
+|3: /3 width=4 by ygt_yprs_trans, sstas_yprs/
+] #W #HU1W #HW1
+elim (ssta_cpcs_lpr_aux … IH2 IH1 … HU1W … HUW2 … HU12 L2) // -IH1 -HU1W -HU12
+[2: /4 width=8 by snv_sstas_aux, ygt_yprs_trans, cprs_lpr_yprs/
+|3: /3 width=10 by snv_sstas_lpr_aux/
+|4,5: /4 width=5 by ygt_yprs_trans, cprs_lpr_yprs, sstas_yprs/
+] -L0 -T0 -L1 -T1 -HT2 #H #HW12 destruct
+lapply (cpcs_trans … HW1 … HW12) -W /3 width=4/
 qed-.
 
-fact dxprs_ltpr_cprs_aux: ∀h,g,L0,T0.
-                          (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) →
-                          (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) →
-                          (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) →
-                          ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[g] →
-                          ∀U1. ⦃h, L1⦄ ⊢ T1 •*➡*[g] U1 →
-                          ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡* T2 →
-                          ∃∃U2. ⦃h, L2⦄ ⊢ T2 •*➡*[g] U2 & L2 ⊢ U1 ➡* U2.
-#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 #T1 #H01 #HT1 #U1 * #W1 #HTW1 #HWU1 #L2 #HL12 #T2 #HT12
-elim (sstas_ltpr_cprs_aux … IH3 IH2 IH1 … H01 … HT12 … HTW1) // -L0 -T0 -T1 #W2 #HTW2 #HW12
-lapply (ltpr_cprs_conf … HL12 … HWU1) -L1 #HWU1
+fact dxprs_cprs_lpr_aux: ∀h,g,L0,T0.
+                         (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) →
+                         (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) →
+                         (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) →
+                         ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[g] →
+                         ∀U1. ⦃h, L1⦄ ⊢ T1 •*➡*[g] U1 →
+                         ∀T2. L1 ⊢ T1 ➡* T2 → ∀L2. L1 ⊢ ➡ L2 →
+                         ∃∃U2. ⦃h, L2⦄ ⊢ T2 •*➡*[g] U2 & L2 ⊢ U1 ➡* U2.
+#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 #T1 #H01 #HT1 #U1 * #W1 #HTW1 #HWU1 #T2 #HT12 #L2 #HL12
+elim (sstas_cprs_lpr_aux … IH3 IH2 IH1 … H01 … HTW1 … HT12 … HL12) // -L0 -T0 -T1 #W2 #HTW2 #HW12
+lapply (cprs_lpr_conf … HL12 … HWU1) -L1 #HWU1
 lapply (cpcs_canc_sn … HW12 HWU1) -W1 #H
 elim (cpcs_inv_cprs … H) -H /3 width=3/
 qed-.
 
 fact ssta_dxprs_aux: ∀h,g,L0,T0.
-                     (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) →
-                     (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) →
-                     ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[g] →
-                     ∀l,U1. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l+1, U1⦄ → ∀T2. ⦃h, L1⦄ ⊢ T1 •*➡*[g] T2 →
-                     ∃∃U,U2. ⦃h, L1⦄ ⊢ U1 •*[g] U & ⦃h, L1⦄ ⊢ T2 •*[g] U2 & L1 ⊢ U ⬌* U2.
-#h #g #L0 #T0 #IH2 #IH1 #L1 #T1 #H01 #HT1 #l #U1 #HTU1 #T2 * #T #HT1T #HTT2
+                     (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) →
+                     (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) →
+                     ∀L,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L, T1⦄ → ⦃h, L⦄ ⊢ T1 ¡[g] →
+                     ∀l,U1. ⦃h, L⦄ ⊢ T1 •[g] ⦃l+1, U1⦄ → ∀T2. ⦃h, L⦄ ⊢ T1 •*➡*[g] T2 →
+                     ∃∃U,U2. ⦃h, L⦄ ⊢ U1 •*[g] U & ⦃h, L⦄ ⊢ T2 •*[g] U2 & L ⊢ U ⬌* U2.
+#h #g #L0 #T0 #IH2 #IH1 #L #T1 #H01 #HT1 #l #U1 #HTU1 #T2 * #T #HT1T #HTT2
 elim (sstas_strip … HT1T … HTU1) #HU1T destruct [ -HT1T | -L0 -T0 -T1 ]
-[ elim (ssta_ltpr_cprs_aux … IH2 IH1 … HTU1 L1 … HTT2) // -L0 -T0 -T /3 width=5/
+[ elim (ssta_cprs_lpr_aux … IH2 IH1 … HTU1 … HTT2 L) // -L0 -T0 -T /3 width=5/
 | @(ex3_2_intro …T2 HU1T) // /2 width=1/
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma
new file mode 100644
index 000000000..44a77627c
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma
@@ -0,0 +1,140 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/computation/dxprs_dxprs.ma".
+include "basic_2/dynamic/snv_lift.ma".
+include "basic_2/dynamic/snv_cpcs.ma".
+
+(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
+
+(* Properties on context-free parallel reduction for local environments *****)
+
+fact snv_cpr_lpr_aux: ∀h,g,L0,T0.
+                      (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_lsubsv h g L1 T1) →
+                      (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) →
+                      (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) →
+                      (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) →
+                      ∀L1,T1. L0 = L1 → T0 = T1 → IH_snv_cpr_lpr h g L1 T1.
+#h #g #L0 #T0 #IH4 #IH3 #IH2 #IH1 #L1 * * [||||*]
+[ #k #HL0 #HT0 #H1 #X #H2 #L2 #_ destruct -IH4 -IH3 -IH2 -IH1 -H1
+  >(cpr_inv_sort1 … H2) -X //
+| #i #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 -IH3 -IH2
+  elim (snv_inv_lref … H1) -H1 #I #K1 #V1 #HLK1 #HV1
+  elim (lpr_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2
+  elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct
+  lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) #HKL
+  elim (cpr_inv_lref1 … H2) -H2
+  [ #H destruct -HLK1
+    lapply (IH1 … HV12 … HK12) -IH1 -HV12 -HK12 // -HV1 [ /2 width=1/ ] -HKL /2 width=5/
+  | * #K0 #V0 #W0 #H #HVW0 #W0 -HV12
+    lapply (ldrop_mono … H … HLK1) -HLK1 -H #H destruct 
+    lapply (ldrop_fwd_ldrop2 … HLK2) -HLK2 #HLK2
+    lapply (IH1 … HVW0 … HK12) -IH1 -HVW0 -HK12 // -HV1 [ /2 width=1/ ] -HKL /3 width=7/
+  ]
+| #p #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 -IH3 -IH2 -IH1
+  elim (snv_inv_gref … H1)
+| #a #I #V1 #T1 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 -IH3 -IH2
+  elim (snv_inv_bind … H1) -H1 #HV1 #HT1
+  elim (cpr_inv_bind1 … H2) -H2 *
+  [ #V2 #T2 #HV12 #HT12 #H destruct
+    lapply (IH1 … HV12 … HL12) // -HV1 [ /2 width=1/ ] #HV2
+    lapply (IH1 … HT12  (L2.ⓑ{I}V2) ?) // -IH1 /2 width=1/
+  | #T2 #HT12 #HXT2 #H1 #H2 destruct -HV1
+    lapply (IH1 … HT1 … HT12 (L2.ⓓV1) ?) -IH1 [1,2: /2 width=1/ ] -L1 -T1 #HT2
+    lapply (snv_inv_lift … HT2 L2 … HXT2) -T2 // /2 width=1/
+  ]
+| #V1 #T1 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct
+  elim (snv_inv_appl … H1) -H1 #a #W10 #W1 #U1 #l #HV1 #HT1 #HVW1 #HW10 #HTU1
+  elim (cpr_inv_appl1 … H2) -H2 *
+  [ #V2 #T2 #HV12 #HT12 #H destruct -IH4
+    lapply (IH1 … HV1 … HV12 … HL12) [ /2 width=1/ ] #HV2
+    lapply (IH1 … HT1 … HT12 … HL12) [ /2 width=1/ ] #HT2
+    elim (IH3 … HVW1 … HV12 … HL12) -HVW1 -HV12 // -HV1 [2: /2 width=1/ ] #W2 #HVW2 #HW12
+    elim (dxprs_cprs_lpr_aux … IH2 IH1 IH3 … HTU1 … T2 … HL12) // [2,3: /2 width=1/ ] -IH2 -IH1 -IH3 -HT1 -HT12 -HTU1 #X #HTU2 #H
+    elim (cprs_fwd_abst1 … H Abst W1) -H #W20 #U2 #HW120 #_ #H destruct
+    lapply (cprs_lpr_conf … HL12 … HW10) -L1 #HW10
+    lapply (cpcs_cprs_strap1 … HW10 … HW120) -W1 #HW120
+    lapply (cpcs_canc_sn … HW12 HW120) -W10 #HW20
+    elim (cpcs_inv_cprs … HW20) -HW20 #W0 #HW20 #HW200
+    lapply (dxprs_cprs_trans … (ⓛ{a}W0.U2) HTU2 ?) [ /2 width=1/ ] -HW200 -HTU2 /2 width=8/
+  | #b #V2 #W20 #T20 #T2 #HV12 #HT202 #H1 #H2 destruct
+    elim (snv_inv_bind … HT1) -HT1 #HW20 #HT20
+    elim (dxprs_inv_abst1 … HTU1) -HTU1 #W30 #T30 #HW230 #_ #H destruct -T30
+    lapply (cprs_div … HW10 … HW230) -W30 #HW120
+    lapply (cpcs_lpr_conf … HL12 … HW120) -HW120 #HW120
+    elim (IH3 … HVW1 … HV12 … HL12) // [2: /2 width=1/ ] -HVW1 #W2 #HVW2 #HW102
+    lapply (cpcs_canc_sn … HW102 … HW120) -W10 #HW220
+    lapply (IH1 … HV12 … HL12) // [ /2 width=1/ ] #HV2 -HV1
+    lapply (IH1 … HW20 … W20 … HL12) // [ /2 width=1/ ] -HW20 #HW20
+    lapply (IH1 … HT20 … HT202 … (L2.ⓛW20) ?) [1,2: /2 width=1/ ] -HT20 #HT2
+    lapply (IH2 … HVW2) //
+    [ @(ygt_yprs_trans … L1 L1 … V1) (**) (* auto /4 width=5/ is a bit slow even with trace *)
+      [ /2 width=1 by fw_ygt/
+      | /3 width=1 by cprs_lpr_yprs, cpr_cprs/
+      ]
+    ] #HW2
+    elim (snv_fwd_ssta … HW20) #l0 #U20 #HWU20
+    elim (ssta_fwd_correct … HVW2) <minus_plus_m_m #U2 #HWU2
+    elim (ssta_cpcs_lpr_aux … IH1 IH3 … HWU2 … HWU20 … HW220 … L2) // -IH3
+    [2: /4 width=4 by ygt_yprs_trans, fw_ygt, ypr_yprs, ypr_lpr/
+    |3: @(ygt_yprs_trans … L1 L2 … V2) (**) (* auto not tried *)
+        [ @(ygt_yprs_trans … L1 L1 … V1)
+          [ /2 width=1 by fw_ygt/
+          | /3 width=1 by cprs_lpr_yprs, cpr_cprs/
+          ]
+        | /3 width=2 by ypr_ssta, ypr_yprs/
+        ]
+    ] #H #_  destruct -IH2 -U2
+    lapply (IH4 … HT2 (L2.ⓓV2) ?)
+    [ /2 width=6/
+    | @(ygt_yprs_trans … (L1.ⓛW20) … T2) (**) (* auto /5 width=5/ is too slow even with trace timeout=35 *)
+      [ /4 width=4 by ygt_yprs_trans, fw_ygt, ypr_yprs, ypr_cpr/
+      | /4 width=1 by ypr_yprs, ypr_lpr, lpr_pair/
+      ]
+    ] -L1 -V1 -W2 -T20 -U20 -W20 -l0 /2 width=1/
+  | #b #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HV02 #HW02 #HT02 #H1 #H2 destruct -IH4
+    elim (snv_inv_bind … HT1) -HT1 #HW0 #HT0
+    elim (dxprs_inv_abbr_abst … HTU1) -HTU1 #X #HTU0 #HX #H destruct
+    elim (lift_inv_bind1 … HX) -HX #W3 #U3 #HW13 #_ #H destruct
+    lapply (cprs_lpr_conf … HL12 … HW10) -HW10 #HW10
+    elim (dxprs_cprs_lpr_aux … IH2 IH1 IH3 … HTU0 T2 … (L2.ⓓW2) ?) // [2,3,4: /2 width=1/ ] -IH2 -HTU0 #X #HTU2 #H
+    elim (cprs_fwd_abst1 … H Abst W3) -H #W #U2 #HW1 #_ #H destruct -U3
+    elim (IH3 … HVW1 … HV10 … HL12) // /2 width=1/ -IH3 -HVW1 #X #H1 #H2
+    lapply (cpcs_canc_sn … H2 HW10) -W10 #H2
+    elim (lift_total X 0 1) #W20 #H3
+    lapply (ssta_lift … H1 (L2.ⓓW2) … HV02 … H3) /2 width=1/ -H1 #HVW20
+    lapply (cpcs_lift (L2.ⓓW2) … H3 … HW13 H2) /2 width=1/ -HW13 -H3 -H2 #HW320
+    lapply (cpcs_cprs_strap1 … HW320 … HW1) -W3 #HW20
+    elim (cpcs_inv_cprs … HW20) -HW20 #W3 #HW203 #HW3
+    lapply (dxprs_cprs_trans … (ⓛ{a}W3.U2) HTU2 ?) [ /2 width=1/ ] -HW3 -HTU2 #HTU2
+    lapply (IH1 … HW02 … HL12) // [ /2 width=1/ ] -HW0 #HW2
+    lapply (IH1 … HV10 … HL12) // [ /2 width=1/ ] -HV1 -HV10 #HV0
+    lapply (IH1 … HT02 (L2.ⓓW2) ?) // [1,2: /2 width=1/ ] -L1 #HT2
+    lapply (snv_lift … HV0 (L2.ⓓW2) … HV02) /2 width=1/ -HV0 -HV02 /3 width=8/
+  ]
+| #W1 #T1 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 -IH2
+  elim (snv_inv_cast … H1) -H1 #U1 #l #HW1 #HT1 #HTU1 #HUW1
+  elim (cpr_inv_cast1 … H2) -H2
+  [ * #W2 #T2 #HW12 #HT12 #H destruct
+    lapply (cpcs_cprs_strap1 … HUW1 W2 ?) [ /2 width=1/ ] -HUW1 #H1
+    lapply (IH1 … HW12 … HL12) // /2 width=1/ -HW1 -HW12 #HW2
+    lapply (IH1 … HT12 … HL12) // /2 width=1/ -IH1 #HT2
+    elim (IH3 … HTU1 … HT12 … HL12) // /2 width=1/ -IH3 -HT1 -HT12 -HTU1 #U2 #HTU2 #HU12
+    lapply (cpcs_lpr_conf … HL12 … H1) -L1 #H1
+    lapply (cpcs_canc_sn … HU12 H1) -U1 /2 width=4/
+  | #H -IH3 -HW1 -HTU1 -HUW1
+    lapply (IH1 … H … HL12) // /2 width=1/
+  ]
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma
deleted file mode 100644
index 6a0be5953..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma
+++ /dev/null
@@ -1,113 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/computation/dxprs_dxprs.ma".
-include "basic_2/dynamic/snv_cpcs.ma".
-
-(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
-
-(* Properties on context-free parallel reduction for local environments *****)
-
-fact snv_ltpr_tpr_aux: ∀h,g,L0,T0.
-                       (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_lsubsv h g L1 T1) →
-                       (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) →
-                       (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) →
-                       (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) →
-                       ∀L1,T1. L0 = L1 → T0 = T1 → IH_snv_ltpr_tpr h g L1 T1.
-#h #g #L0 #T0 #IH4 #IH3 #IH2 #IH1 #L1 * * [||||*]
-[ #k #HL0 #HT0 #H1 #L2 #_ #X #H2 destruct -IH4 -IH3 -IH2 -IH1 -L1
-  >(tpr_inv_atom1 … H2) -X //
-| #i #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct -IH4 -IH3 -IH2
-  elim (snv_inv_lref … H1) -H1 #I #K1 #V1 #HLK1 #HV1
-  >(tpr_inv_atom1 … H2) -X
-  elim (ltpr_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2
-  elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct
-  lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) -HLK1 #HLK1
-  lapply (IH1 … HK12 … HV12) -IH1 -HV12 -HK12 // -HV1 [ /2 width=1/ ] -HLK1 /2 width=5/
-| #p #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct -IH4 -IH3 -IH2 -IH1
-  elim (snv_inv_gref … H1)
-| #a #I #V1 #T1 #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct -IH4 -IH3 -IH2
-  elim (snv_inv_bind … H1) -H1 #HV1 #HT1
-  elim (tpr_inv_bind1 … H2) -H2 *
-  [ #V2 #T0 #T2 #HV12 #HT10 #HT02 #H destruct
-    lapply (tps_lsubr_trans … HT02 (L2.ⓑ{I}V2) ?) -HT02 /2 width=1/ #HT02
-    lapply (IH1 … HL12 … HV12) // [ /2 width=1/ ] #HV2
-    lapply (snv_ltpr_cpr_aux … HT1  (L2.ⓑ{I}V2) … T2 ?) -HT1
-    [ /3 width=5 by cpr_intro, tps_tpss/ | /2 width=1/ | /3 width=1/ ] -IH1 -T0 /2 width=1/
-  | #T2 #HT12 #HXT2 #H1 #H2 destruct
-    lapply (IH1 … HT1 (L2.ⓓV1) … HT12) -IH1 -HT1 -HT12 [1,2: /2 width=1/ ] -HL12 #HT2
-    lapply (snv_inv_lift … HT2 L2 … HXT2) -T2 // /2 width=1/
-  ]
-| #V1 #T1 #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct
-  elim (snv_inv_appl … H1) -H1 #a #W10 #W1 #U1 #l #HV1 #HT1 #HVW1 #HW10 #HTU1
-  elim (tpr_inv_appl1 … H2) -H2 *
-  [ #V2 #T2 #HV12 #HT12 #H destruct -IH4
-    lapply (IH1 … HV1 … HL12 … HV12) [ /2 width=1/ ] #HV2
-    lapply (IH1 … HT1 … HL12 … HT12) [ /2 width=1/ ] #HT2
-    elim (IH3 … HVW1 … HL12 … HV12) -HVW1 -HV12 // -HV1 [2: /2 width=1/ ] #W2 #HVW2 #HW12
-    elim (dxprs_ltpr_cprs_aux … IH2 IH1 IH3 … HTU1 … HL12 T2) // [2: /3 width=1/ |3: /2 width=1/ ] -IH2 -IH1 -IH3 -HT1 -HT12 -HTU1 #X #HTU2 #H
-    elim (cprs_inv_abst1 Abst W1 … H) -H #W20 #U2 #HW120 #_ #H destruct
-    lapply (ltpr_cprs_conf … HL12 … HW10) -L1 #HW10
-    lapply (cpcs_cprs_strap1 … HW10 … HW120) -W1 #HW120
-    lapply (cpcs_canc_sn … HW12 HW120) -W10 #HW20
-    elim (cpcs_inv_cprs … HW20) -HW20 #W0 #HW20 #HW200
-    lapply (dxprs_cprs_trans … (ⓛ{a}W0.U2) HTU2 ?) [ /2 width=1/ ] -HW200 -HTU2 /2 width=8/
-  | #b #V2 #W20 #T20 #T2 #HV12 #HT202 #H1 #H2 destruct
-    elim (snv_inv_bind … HT1) -HT1 #HW20 #HT20
-    elim (dxprs_inv_abst1 … HTU1) -HTU1 #W30 #T30 #HW230 #_ #H destruct -T30
-    lapply (cprs_div … HW10 … HW230) -W30 #HW120
-    elim (snv_fwd_ssta … HW20) #l0 #U20 #HWU20
-    elim (ssta_fwd_correct … HVW1) <minus_plus_m_m #U10 #HWU10
-    elim (ssta_ltpr_cpcs_aux … IH1 IH3 … HW20 … HWU10 … HWU20) // -IH3 -HWU10
-    [2: /3 width=5/ |3: /2 width=1/
-    |4: /4 width=4 by ygt_yprs_trans, fw_ygt, sstas_yprs, ssta_sstas/
-    ] #H #_ -IH2 -U10 destruct
-    lapply (IH4 … HT20 (L1.ⓓV1) ?) [ /2 width=6/ | /2 width=1/ ] -U20 -W10 -l0 -IH4 -HT20 -HW20 #HT20
-    lapply (IH1 … HL12 … HV12) // [ /2 width=1/ ] #HV2
-    lapply (IH1 … HT20 … (L2.ⓓV2) … HT202) [1,2: /2 width=1/ ] -L1 -V1 -W20 -T20 /2 width=1/
-  | #b #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HW02 #HT02 #HV02 #H1 #H2 destruct -IH4
-    elim (snv_inv_bind … HT1) -HT1 #HW0 #HT0
-    elim (dxprs_inv_abbr_abst … HTU1) -HTU1 #X #HTU0 #HX #H destruct
-    elim (lift_inv_bind1 … HX) -HX #W3 #U3 #HW13 #_ #H destruct
-    lapply (ltpr_cprs_conf … HL12 … HW10) -HW10 #HW10
-    elim (dxprs_ltpr_cprs_aux … IH2 IH1 IH3 … HTU0 (L2.ⓓW2) … T2 ?) // [2: /3 width=1/ |3,4: /2 width=1/ ] -IH2 -HTU0 #X #HTU2 #H
-    elim (cprs_inv_abst1 Abst W3 … H) -H #W #U2 #HW1 #_ #H destruct -U3
-    elim (IH3 … HVW1 … HL12 … HV10) // /2 width=1/ -IH3 -HVW1 #X #H1 #H2
-    lapply (cpcs_canc_sn … H2 HW10) -W10 #H2
-    elim (lift_total X 0 1) #W20 #H3
-    lapply (ssta_lift … H1 (L2.ⓓW2) … HV02 … H3) /2 width=1/ -H1 #HVW20
-    lapply (cpcs_lift (L2.ⓓW2) … H3 … HW13 H2) /2 width=1/ -HW13 -H3 -H2 #HW320
-    lapply (cpcs_cprs_strap1 … HW320 … HW1) -W3 #HW20
-    elim (cpcs_inv_cprs … HW20) -HW20 #W3 #HW203 #HW3
-    lapply (dxprs_cprs_trans … (ⓛ{a}W3.U2) HTU2 ?) [ /2 width=1/ ] -HW3 -HTU2 #HTU2
-    lapply (IH1 … HL12 … HW02) // [ /2 width=1/ ] -HW0 #HW2
-    lapply (IH1 … HL12 … HV10) // [ /2 width=1/ ] -HV1 -HV10 #HV0
-    lapply (IH1 … HT0 … (L2.ⓓW2) … HT02) [1,2: /2 width=1/ ] -L1 -HT02 -HW02 #HT2
-    lapply (snv_lift … HV0 (L2.ⓓW2) … HV02) /2 width=1/ -HV0 -HV02 /3 width=8/
-  ]
-| #W1 #T1 #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct -IH4 -IH2
-  elim (snv_inv_cast … H1) -H1 #U1 #l #HW1 #HT1 #HTU1 #HUW1
-  elim (tpr_inv_cast1 … H2) -H2
-  [ * #W2 #T2 #HW12 #HT12 #H destruct
-    lapply (cpcs_cprs_strap1 … HUW1 W2 ?) [ /3 width=1/ ] -HUW1 #H1
-    lapply (IH1 … HL12 … HW12) // /2 width=1/ -HW1 -HW12 #HW2
-    lapply (IH1 … HL12 … HT12) // /2 width=1/ -IH1 #HT2
-    elim (IH3 … HTU1 … HL12 … HT12) // /2 width=1/ -IH3 -HT1 -HT12 -HTU1 #U2 #HTU2 #HU12
-    lapply (ltpr_cpcs_conf … HL12 … H1) -L1 #H1
-    lapply (cpcs_canc_sn … HU12 H1) -U1 /2 width=4/
-  | #H -IH3 -HW1 -HTU1 -HUW1
-    lapply (IH1 … HL12 … H) // /2 width=1/
-  ]
-]  
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta.ma
index f6d753d22..b656dbd54 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basic_2/dynamic/snv_lift.ma".
 include "basic_2/dynamic/snv_cpcs.ma".
 
 (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
@@ -19,8 +20,8 @@ include "basic_2/dynamic/snv_cpcs.ma".
 (* Properties on stratified static type assignment for terms ****************)
 
 fact snv_ssta_aux: ∀h,g,L0,T0.
-                   (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) →
-                   (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) →
+                   (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) →
+                   (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) →
                    (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) →
                    ∀L1,T1. L0 = L1 → T0 = T1 → IH_snv_ssta h g L1 T1.
 #h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 * * [||||*]
@@ -44,7 +45,7 @@ fact snv_ssta_aux: ∀h,g,L0,T0.
   elim (ssta_dxprs_aux … IH3 IH2 … HTU1 … HT10) -IH3 -IH2 // /2 width=2/ -T1 #U #X #HU1U #H #HU0
   elim (sstas_inv_bind1 … H) -H #U0 #HTU0 #H destruct
   elim (cpcs_inv_abst2 … HU0) -HU0 #W2 #U2 #HU2 #HU02
-  elim (cprs_inv_abst … HU02 Abst W0) -HU02 #HW02 #_
+  elim (cprs_fwd_abst … HU02 Abst W0) -HU02 #HW02 #_
   lapply (cprs_trans … HW10 … HW02) -W0 /3 width=10 by snv_appl, ex2_intro/ (**) (* auto is too slow without trace *)
 | #W1 #T1 #HL0 #HT0 #H1 #X #l #H2 destruct -IH3 -IH2
   elim (snv_inv_cast … H1) -H1 #U1 #l0 #HW1 #HT1 #HTU1 #HUW1
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta_lpr.ma
new file mode 100644
index 000000000..e03920285
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta_lpr.ma
@@ -0,0 +1,126 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/lsubss_ssta.ma".
+include "basic_2/dynamic/snv_cpcs.ma".
+
+(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
+
+(* Properties on sn parallel reduction for local environments ***************)
+
+fact ssta_cpr_lpr_aux: ∀h,g,L0,T0.
+                       (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) →
+                       (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) →
+                       (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) →
+                       ∀L1,T1. L0 = L1 → T0 = T1 → IH_ssta_cpr_lpr h g L1 T1.
+#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 * * [|||| *]
+[ #k #_ #_ #_ #X2 #l #H2 #X3 #H3 #L2 #HL12 -IH3 -IH2 -IH1
+  elim (ssta_inv_sort1 … H2) -H2 #Hkl #H destruct
+  >(cpr_inv_sort1 … H3) -X3 /4 width=6/
+| #i #HL0 #HT0 #H1 #X2 #l #H2 #X3 #H3 #L2 #HL12 destruct -IH3 -IH2
+  elim (snv_inv_lref … H1) -H1 #I0 #K0 #V0 #H #HV1
+  elim (ssta_inv_lref1 … H2) -H2 * #K1
+  #V1 #W1 [| #l0 ] #HLK1 #HVW1 #HWU1 [| #H destruct ]
+  lapply (ldrop_mono … H … HLK1) -H #H destruct
+  lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) #HKV1
+  elim (lpr_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2
+  elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct
+  lapply (ldrop_fwd_ldrop2 … HLK2) #H2
+  elim (cpr_inv_lref1 … H3) -H3
+  [1,3: #H destruct -HLK1
+  |2,4: * #K0 #V0 #W0 #H #HVW0 #HW0
+        lapply (ldrop_mono … H … HLK1) -H -HLK1 #H destruct
+  ]
+  [ elim (IH1 … HVW1 … HV12 … HK12) -IH1 -HVW1 // [2: /2 width=1/ ] -K1 -V1 #W2 #HVW2 #HW12
+    elim (lift_total W2 0 (i+1)) #U2 #HWU2
+    lapply (cpcs_lift … H2 … HWU1 … HWU2 HW12) -H2 -W1 /3 width=6/
+  | elim (IH1 … HVW1 … HV12 … HK12) -IH1 -HVW1 // [2: /2 width=1/ ] #W2 #HVW2 #_
+    elim (lift_total V2 0 (i+1)) #U2 #HVU2
+    lapply (lpr_cpr_conf … HK12 … HV12) -HV12 #HV12
+    lapply (cpcs_lift … H2 … HWU1 … HVU2 HV12) -H2 -V1 /3 width=6/
+  | elim (IH1 … HVW1 … HVW0 … HK12) -IH1 -HVW1 // [2: /2 width=1/ ] -K1 -V1 #W2 #HVW2 #HW12
+    elim (lift_total W2 0 (i+1)) #U2 #HWU2
+    lapply (ssta_lift … HVW2 … H2 … HW0 … HWU2) -HVW2 -HW0
+    lapply (cpcs_lift … H2 … HWU1 … HWU2 HW12) -H2 -W1 /3 width=6/
+  ]
+| #p #_ #HT0 #H1 destruct -IH3 -IH2 -IH1
+  elim (snv_inv_gref … H1)
+| #a #I #V1 #T1 #HL0 #HT0 #H1 #X2 #l #H2 #X3 #H3 #L2 #HL12 destruct -IH3 -IH2
+  elim (snv_inv_bind … H1) -H1 #_ #HT1
+  elim (ssta_inv_bind1 … H2) -H2 #U1 #HTU1 #H destruct
+  elim (cpr_inv_bind1 … H3) -H3 *
+  [ #V2 #T2 #HV12 #HT12 #H destruct
+    elim (IH1 … HTU1 … HT12 (L2.ⓑ{I}V2)) // [2,3: /2 width=1/ ] -T1
+    lapply (lpr_cpr_conf … HL12 … HV12) -L1 /3 width=5/
+  | #T2 #HT12 #HT2 #H1 #H2 destruct
+    elim (IH1 … HTU1 … HT12 (L2.ⓓV1)) -IH1 -HTU1 // [2,3: /2 width=1/ ] -T1 -HL12 #U2 #HTU2 #HU12
+    elim (ssta_inv_lift1 … HTU2 … HT2) -T2 [3: /2 width=1/ |2: skip ] #U #HXU #HU2
+    lapply (cpcs_bind1 true … V1 V1 … HU12) // -HU12 #HU12
+    lapply (cpcs_cpr_strap1 … HU12 U ?) -HU12 /2 width=3/
+  ]
+| #V1 #T1 #HL0 #HT0 #H1 #X2 #l #H2 #X3 #H3 #L2 #HL12 destruct
+  elim (snv_inv_appl … H1) -H1 #a #W1 #W10 #U10 #l0 #HV1 #HT1 #HVW1 #HW10 #HTU10
+  elim (ssta_inv_appl1 … H2) -H2 #U1 #HTU1 #H destruct
+  elim (cpr_inv_appl1 … H3) -H3 *
+  [ #V2 #T2 #HV12 #HT12 #H destruct -a -l0 -W1 -W10 -U10 -HV1 -IH3 -IH2
+    elim (IH1 … HTU1 … HT12 … HL12) -IH1 -HTU1 // [2: /2 width=1/ ] -T1 #U2 #HTU2 #HU12
+    lapply (lpr_cpr_conf … HL12 … HV12) -L1 /3 width=5/
+  | #b #V2 #W #T2 #T20 #HV12 #HT20 #H1 #H2 destruct
+    elim (snv_inv_bind … HT1) -HT1 #HW #HT2
+    elim (ssta_inv_bind1 … HTU1) -HTU1 #U2 #HTU2 #H destruct
+    elim (dxprs_inv_abst1 … HTU10) -HTU10 #W0 #U0 #HW0 #_ #H destruct
+    lapply (cprs_div … HW10 … HW0) -W0 #HW1W
+    elim (ssta_fwd_correct … HVW1) <minus_plus_m_m #X1 #HWX1
+    elim (snv_fwd_ssta … HW) #l1 #V #HWV
+    lapply (IH3 … HVW1) -IH3 // [ /2 width=1/ ] #HW1
+    elim (ssta_cpcs_lpr_aux … IH2 IH1 … HWX1 … HWV … L1) -IH2 -HWX1 //
+    [2: /2 width=1/
+    |3: /4 width=4 by ygt_yprs_trans, fw_ygt, sstas_yprs, ssta_sstas/
+    ] #H #_ destruct -X1
+    elim (IH1 … HVW1 … HV12 … HL12) -HVW1 // -HV1 [2: /2 width=1/ ] #W2 #HVW2 #HW12
+    elim (IH1 … HWV W … HL12) -HWV // -HW [2: /2 width=1/ ] #V0 #HWV0 #_
+    elim (IH1 … HTU2 … HT20 (L2.ⓛW)) -IH1 -HTU2 -HT20 // [2,3: /2 width=1/ ] -HT2 #U20 #HTU20 #HU20
+    lapply (cpcs_lpr_conf … HL12 … HW1W) #HW1W
+    lapply (lpr_cpr_conf … HL12 … HV12) -L1 #HV12
+    lapply (cpcs_ext_bind … HV12 … HU20 b Abbr) -HV12 -HU20 #HU20
+    lapply (cpcs_canc_sn … HW12 HW1W) -W1 #HW2
+    elim (lsubss_ssta_trans … HTU20 (L2.ⓓV2) ?) -HTU20
+    [ #U #HTU20 #HUU20 -HWV0 -W2
+      lapply (cpcs_bind1 b … V2 V2 … HUU20) // -HUU20 #HUU20
+      lapply (cpcs_canc_dx … HU20 … HUU20) -U20 #HU2
+      lapply (cpcs_cpr_strap2 … (ⓐV1.ⓛ{b}W.U2) … HU2) [ /2 width=1/ ] /3 width=3/
+    | -b -l -V -V1 -T2 -T20 -U0 -U2 -U20 /2 width=6/
+    ]
+  | #b #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HV02 #HW02 #HT02 #H1 #H2 destruct -a -l0 -W1 -W10 -HV1 -IH3 -IH2
+    elim (ssta_inv_bind1 … HTU1) -HTU1 #U0 #HTU0 #H destruct
+    elim (snv_inv_bind … HT1) -HT1 #_ #HT0
+    elim (IH1 … HTU0 … HT02 (L2.ⓓW2)) -IH1 -HTU0 // [2,3: /2 width=1/ ] -T0 #U2 #HTU2 #HU02
+    lapply (lpr_cpr_conf … HL12 … HV10) -HV10 #HV10
+    lapply (lpr_cpr_conf … HL12 … HW02) -L1 #HW02
+    lapply (cpcs_bind2 b … HW02 … HU02) -HW02 -HU02 #HU02
+    lapply (cpcs_flat … HV10 … HU02 Appl) -HV10 -HU02 #HU02
+    lapply (cpcs_cpr_strap1 … HU02 (ⓓ{b}W2.ⓐV2.U2) ?) [ /2 width=3/ ] -V0 /4 width=3/
+  ]
+| #U0 #T1 #HL0 #HT0 #H1 #X2 #l #H2 #X3 #H3 #L2 #HL12 destruct -IH3 -IH2
+  elim (snv_inv_cast … H1) -H1 #T0 #l0 #_ #HT1 #HT10 #_
+  lapply (ssta_inv_cast1 … H2) -H2 #HTU1
+  elim (ssta_mono … HT10 … HTU1) -HT10 #H1 #H2 destruct
+  elim (cpr_inv_cast1 … H3) -H3
+  [ * #U2 #T2 #_ #HT12 #H destruct
+    elim (IH1 … HTU1 … HT12 … HL12) -IH1 -HTU1 -HL12 // [2: /2 width=1/ ] -T1 -U0 /3 width=3/
+  | #HT1X3
+    elim (IH1 … HTU1 … HT1X3 … HL12) -IH1 -HTU1 -HL12 // [2: /2 width=1/ ] -U0 -T1 /2 width=3/
+  ]
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta_ltpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta_ltpr.ma
deleted file mode 100644
index e7f402513..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta_ltpr.ma
+++ /dev/null
@@ -1,120 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/equivalence/lsubss_ssta.ma".
-include "basic_2/dynamic/snv_cpcs.ma".
-
-(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
-
-(* Properties on context-free parallel reduction for local environments *****)
-
-fact ssta_ltpr_tpr_aux: ∀h,g,L0,T0.
-                        (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) →
-                        (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) →
-                        (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) →
-                        ∀L1,T1. L0 = L1 → T0 = T1 → IH_ssta_ltpr_tpr h g L1 T1.
-#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 * * [|||| *]
-[ #k #_ #_ #_ #X2 #l #H2 #L2 #HL12 #X3 #H3 -IH3 -IH2 -IH1
-  elim (ssta_inv_sort1 … H2) -H2 #Hkl #H destruct
-  >(tpr_inv_atom1 … H3) -X3 /4 width=6/
-| #i #HL0 #HT0 #H1 #X2 #l #H2 #L2 #HL12 #X3 #H3 destruct -IH3 -IH2
-  elim (snv_inv_lref … H1) -H1 #I0 #K0 #V0 #H #HV1
-  elim (ssta_inv_lref1 … H2) -H2 * #K1
-  >(tpr_inv_atom1 … H3) -X3
-  [ #V1 #W1 #HLK1 #HVW1 #HWU1
-    lapply (ldrop_mono … H … HLK1) -H #H destruct
-    lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) #HKV1
-    elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #H #HLK2
-    elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct
-    elim (IH1 … HVW1 … HK12 … HV12) -IH1 -HVW1 -HV12 // [2: /2 width=1/ ] -V1 #W2 #HVW2 #HW12
-    lapply (ldrop_fwd_ldrop2 … HLK2) #H2
-    elim (lift_total W2 0 (i+1)) #U2 #HWU2
-    lapply (cpcs_lift … H2 … HWU1 … HWU2 HW12) -H2 -W1 /3 width=6/
-  | #V1 #W1 #l0 #HLK1 #HVW1 #HVU1 #H destruct
-    lapply (ldrop_mono … H … HLK1) -H #H destruct
-    lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) #HKV1
-    elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 #X #H #HLK2
-    elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct
-    elim (IH1 … HVW1 … HK12 … HV12) -IH1 -HVW1 -HK12 // [2: /2 width=1/ ] -HV1 -HKV1 #W2 #HVW2 #_ -W1
-    elim (lift_total V2 0 (i+1)) #U2 #HVU2
-    lapply (tpr_lift … HV12 … HVU1 … HVU2) -V1 /4 width=6/
-  ]
-| #p #_ #HT0 #H1 destruct -IH3 -IH2 -IH1
-  elim (snv_inv_gref … H1)
-| #a #I #V1 #T1 #HL0 #HT0 #H1 #X2 #l #H2 #L2 #HL12 #X3 #H3 destruct -IH3 -IH2
-  elim (snv_inv_bind … H1) -H1 #_ #HT1
-  elim (ssta_inv_bind1 … H2) -H2 #U1 #HTU1 #H destruct
-  elim (tpr_inv_bind1 … H3) -H3 *
-  [ #V2 #T0 #T2 #HV12 #HT10 #HT02 #H destruct
-    lapply (tps_lsubr_trans … HT02 (L2.ⓑ{I}V2) ?) -HT02 [ /2 width=1/ ] #HT02
-    elim (ssta_ltpr_cpr_aux … HT1 … HTU1 (L2.ⓑ{I}V2) … T2) -HT1 -HTU1
-    [2: /3 width=5 by cpr_intro, tps_tpss/ |3: /2 width=1/ |4: /3 width=1/ ] -IH1 -T0 -HL12 #U2 #HTU2 #HU12
-    lapply (cpcs_bind2 … V1 … HU12 … a) -HU12 [ /2 width=1/ ] -HV12 /3 width=3/
-  | #T2 #HT12 #HT2 #H1 #H2 destruct
-    elim (IH1 … HTU1 (L2.ⓓV1) … T2) -IH1 -HTU1 // [2,3: /2 width=1/ ] -T1 -HL12 #U2 #HTU2 #HU12
-    lapply (cpcs_bind1 … HU12 … V1 … true) // -HU12 #HU12
-    elim (ssta_inv_lift1 … HTU2 … HT2) -T2 [3: /2 width=1/ |2: skip ] #U #HXU #HU2
-    lapply (cpcs_cpr_strap1 … HU12 U ?) -HU12 [ /3 width=3/ ] -U2 /2 width=3/
-  ]
-| #V1 #T1 #HL0 #HT0 #H1 #X2 #l #H2 #L2 #HL12 #X3 #H3 destruct
-  elim (snv_inv_appl … H1) -H1 #a #W1 #W10 #U10 #l0 #HV1 #HT1 #HVW1 #HW10 #HTU10
-  elim (ssta_inv_appl1 … H2) -H2 #U1 #HTU1 #H destruct
-  elim (tpr_inv_appl1 … H3) -H3 *
-  [ #V2 #T2 #HV12 #HT12 #H destruct -a -l0 -W1 -W10 -U10 -HV1 -IH3 -IH2
-    elim (IH1 … HTU1 … HL12 … HT12) -IH1 -HTU1 -HL12 // [2: /2 width=1/ ] -T1 #U2 #HTU2 #HU12
-    lapply (cpcs_flat … V1 V2 … HU12) -HU12 [ /2 width=1/ ] -HV12 /3 width=3/
-  | #b #V2 #W #T2 #T20 #HV12 #HT20 #H1 #H2 destruct
-    elim (snv_inv_bind … HT1) -HT1 #HW #HT2
-    elim (ssta_inv_bind1 … HTU1) -HTU1 #U2 #HTU2 #H destruct
-    elim (dxprs_inv_abst1 … HTU10) -HTU10 #W0 #U0 #HW0 #_ #H destruct
-    lapply (cprs_div … HW10 … HW0) -W0 #HW1W
-    elim (ssta_fwd_correct … HVW1) <minus_plus_m_m #X1 #HWX1
-    elim (snv_fwd_ssta … HW) #l1 #V #HWV
-    lapply (IH3 … HVW1) -IH3 // [ /2 width=1/ ] #HW1
-    elim (ssta_ltpr_cpcs_aux … IH2 IH1 … HWX1 … HWV …) -IH2 -HWX1 //
-    [2: /2 width=1/
-    |3: /4 width=4 by ygt_yprs_trans, fw_ygt, sstas_yprs, ssta_sstas/
-    ] #H #_ destruct -X1
-    elim (IH1 … HVW1 … HL12 … HV12) -HVW1 // -HV1 [2: /2 width=1/ ] #W2 #HVW2 #HW12
-    elim (IH1 … HWV … HL12 W) -HWV // -HW [2: /2 width=1/ ] #V0 #HWV0 #_
-    elim (IH1 … HTU2 (L2.ⓛW) … HT20) -IH1 -HTU2 -HT20 // [2,3: /2 width=1/ ] -HT2 #U20 #HTU20 #HU20
-    lapply (ltpr_cpcs_conf … HL12 … HW1W) -L1 #HW1W
-    lapply (cpcs_canc_sn … HW12 HW1W) -W1 #HW2
-    elim (lsubss_ssta_trans … HTU20 (L2.ⓓV2) ?) -HTU20
-    [ #U #HTU20 #HUU20 -HWV0 -W2
-      @(ex2_intro … (ⓓ{b}V2.U)) [ /2 width=1/ ] -h -l -l1 -V -V0 -T2 -T20 -U0
-      @(cpcs_cprs_strap2 … (ⓓ{b}V2.U2)) [ /3 width=1/ ] -V1
-      @(cpcs_canc_dx … (ⓓ{b}V2.U20)) /2 width=2/
-    | -b -l -V -V1 -T2 -T20 -U0 -U2 -U20 /2 width=6/
-    ]
-  | #b #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HW02 #HT02 #HV02 #H1 #H2 destruct -a -l0 -W1 -W10 -HV1 -IH3 -IH2
-    elim (ssta_inv_bind1 … HTU1) -HTU1 #U0 #HTU0 #H destruct
-    elim (snv_inv_bind … HT1) -HT1 #_ #HT0
-    elim (IH1 … HTU0 (L2.ⓓW2) … HT02) -IH1 -HTU0 // [2,3: /2 width=1/ ] -T0 -HL12 #U2 #HTU2 #HU02
-    lapply (cpcs_bind2 … W0 … HU02 b) -HU02 [ /2 width=1/ ] #HU02
-    lapply (cpcs_flat … V1 V0 … HU02 Appl) [ /2 width=1/ ] -HV10 -HU02 #HU02
-    lapply (cpcs_cpr_strap1 … HU02 (ⓓ{b}W2.ⓐV2.U2) ?) -HU02 [ /3 width=3/ ] -V0 -HW02 /4 width=3/
-  ]
-| #U0 #T1 #HL0 #HT0 #H1 #X2 #l #H2 #L2 #HL12 #X3 #H3 destruct -IH3 -IH2
-  elim (snv_inv_cast … H1) -H1 #T0 #l0 #_ #HT1 #HT10 #_
-  lapply (ssta_inv_cast1 … H2) -H2 #HTU1
-  elim (ssta_mono … HT10 … HTU1) -HT10 #H1 #H2 destruct
-  elim (tpr_inv_cast1 … H3) -H3
-  [ * #U2 #T2 #_ #HT12 #H destruct
-    elim (IH1 … HTU1 … HL12 … HT12) -IH1 -HTU1 -HL12 // [2: /2 width=1/ ] -T1 -U0 /3 width=3/
-  | #HT1X3
-    elim (IH1 … HTU1 … HL12 … HT1X3) -IH1 -HTU1 -HL12 // [2: /2 width=1/ ] -U0 -T1 /2 width=3/
-  ]
-]
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma
index bb4daf0be..2bf1ae018 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma
@@ -72,7 +72,7 @@ qed.
 lemma lsubsv_yprs: ∀h,g,L1,L2,T. h ⊢ L2 ¡⊑[g] L1 → h ⊢ ⦃L1, T⦄ ≥[g] ⦃L2, T⦄.
 /3 width=1/ qed.
 
-lemma lpr_cprs_yprs: ∀h,g,L1,L2,T1,T2. L1 ⊢ ➡ L2 → L2 ⊢ T1 ➡* T2 →
+lemma cprs_lpr_yprs: ∀h,g,L1,L2,T1,T2. L1 ⊢ T1 ➡* T2 → L1 ⊢ ➡ L2 →
                      h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L2, T2⦄.
-/3 width=4 by yprs_strap2, ypr_lpr, cprs_yprs/
+/3 width=4 by yprs_strap1, ypr_lpr, cprs_yprs/
 qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma
index 199e49b07..784c75470 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma
@@ -211,13 +211,13 @@ qed.
 
 (* Basic_1: was: pc3_wcpr0_t *)
 (* Basic_1: note: pc3_wcpr0_t should be renamed *)
-lemma lpr_cprs_conf: ∀L1,L2. L1 ⊢ ➡ L2 → ∀T1,T2. L1 ⊢ T1 ➡* T2 → L2 ⊢ T1 ⬌* T2.
+lemma cprs_lpr_conf: ∀L1,L2. L1 ⊢ ➡ L2 → ∀T1,T2. L1 ⊢ T1 ➡* T2 → L2 ⊢ T1 ⬌* T2.
 #L1 #L2 #HL12 #T1 #T2 #H @(cprs_ind … H) -T2 //
 /3 width=5 by cpcs_trans, lpr_cpr_conf/
 qed-.
 
 (* Basic_1: was: pc3_wcpr0 *)
-lemma lpr_cpcs_conf: ∀L1,L2. L1 ⊢ ➡ L2 → ∀T1,T2. L1 ⊢ T1 ⬌* T2 → L2 ⊢ T1 ⬌* T2.
+lemma cpcs_lpr_conf: ∀L1,L2. L1 ⊢ ➡ L2 → ∀T1,T2. L1 ⊢ T1 ⬌* T2 → L2 ⊢ T1 ⬌* T2.
 #L1 #L2 #HL12 #T1 #T2 #H
-elim (cpcs_inv_cprs … H) -H /3 width=5 by cpcs_canc_dx, lpr_cprs_conf/
+elim (cpcs_inv_cprs … H) -H /3 width=5 by cpcs_canc_dx, cprs_lpr_conf/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpc.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpc.etc
index f552d5818..ee362471b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpc.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpc.etc
@@ -12,6 +12,14 @@
 (*                                                                        *)
 (**************************************************************************)
 
+notation "hvbox( ⦃ term 46 L1 , break term 46 T1 ⦄ ⬌ break ⦃ term 46 L2 , break term 46 T2 ⦄ )"
+   non associative with precedence 45
+   for @{ 'FocalizedPConv $L1 $T1 $L2 $T2 }.
+
+notation "hvbox( ⦃ term 46 L1 , break term 46 T1 ⦄ ⬌ ⬌ break ⦃ term 46 L2 , break term 46 T2 ⦄ )"
+   non associative with precedence 45
+   for @{ 'FocalizedPConvAlt $L1 $T1 $L2 $T2 }.
+
 include "basic_2/reducibility/fpr.ma".
 
 (* CONTEXT-FREE PARALLEL CONVERSION ON CLOSURES *****************************)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpcs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpcs.etc
index 45be26781..68c946ce8 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpcs.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpcs.etc
@@ -12,6 +12,14 @@
 (*                                                                        *)
 (**************************************************************************)
 
+notation "hvbox( ⦃ term 46 L1 , break term 46 T1 ⦄ ⬌ * break ⦃ term 46 L2 , break term 46 T2 ⦄ )"
+   non associative with precedence 45
+   for @{ 'FocalizedPConvStar $L1 $T1 $L2 $T2 }.
+
+notation "hvbox( ⦃ term 46 L1 , break term 46 T1 ⦄ ⬌ ⬌ * break ⦃ term 46 L2 , break term 46 T2 ⦄ )"
+   non associative with precedence 45
+   for @{ 'FocalizedPConvStarAlt $L1 $T1 $L2 $T2 }.
+
 include "basic_2/conversion/fpc.ma".
 
 (* CONTEXT-FREE PARALLEL EQUIVALENCE ON CLOSURES ****************************)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpc.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpc.etc
index 273873abd..b80b290b6 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpc.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpc.etc
@@ -12,6 +12,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
+notation "hvbox( ⦃ term 46 L1 ⦄ ⬌ ⬌ break ⦃ term 46 L2 ⦄ )"
+   non associative with precedence 45
+   for @{ 'FocalizedPConvAlt $L1 $L2 }.
+
 include "basic_2/reducibility/lfpr.ma".
 
 (* FOCALIZED PARALLEL CONVERSION ON LOCAL ENVIRONMENTS **********************)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpcs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpcs.etc
index 5ad9180ac..3674637dd 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpcs.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpcs.etc
@@ -12,6 +12,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
+notation "hvbox( ⦃ term 46 L1 ⦄ ⬌ ⬌ * break ⦃ term 46 L2 ⦄ )"
+   non associative with precedence 45
+   for @{ 'FocalizedPConvStarAlt $L1 $L2 }.
+
 include "basic_2/conversion/lfpc.ma".
 
 (* FOCALIZED PARALLEL EQUIVALENCE ON LOCAL ENVIRONMENTS *********************)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/preservation/snv_cpcs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/preservation/snv_cpcs.etc
new file mode 100644
index 000000000..9451e34d2
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/preservation/snv_cpcs.etc
@@ -0,0 +1,161 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/unwind/sstas_sstas.ma".
+include "basic_2/equivalence/cpcs_ltpr.ma".
+include "basic_2/dynamic/snv_ltpss_dx.ma".
+include "basic_2/dynamic/snv_sstas.ma".
+include "basic_2/dynamic/ygt.ma".
+
+(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
+
+(* Inductive premises for the preservation results **************************)
+
+definition IH_snv_ltpr_tpr: ∀h:sh. sd h → relation2 lenv term ≝
+                            λh,g,L1,T1. ⦃h, L1⦄ ⊢ T1 ¡[g] →
+                            ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → ⦃h, L2⦄ ⊢ T2 ¡[g].
+
+definition IH_ssta_ltpr_tpr: ∀h:sh. sd h → relation2 lenv term ≝
+                             λh,g,L1,T1. ⦃h, L1⦄ ⊢ T1 ¡[g] →
+                             ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l, U1⦄ →
+                             ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 →
+                             ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l, U2⦄ & L2 ⊢ U1 ⬌* U2.
+
+definition IH_snv_ssta: ∀h:sh. sd h → relation2 lenv term ≝
+                        λh,g,L1,T1. ⦃h, L1⦄ ⊢ T1 ¡[g] →
+                        ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l+1, U1⦄ → ⦃h, L1⦄ ⊢ U1 ¡[g].
+
+definition IH_snv_lsubsv: ∀h:sh. sd h → relation2 lenv term ≝
+                          λh,g,L2,T. ⦃h, L2⦄ ⊢ T ¡[g] →
+                          ∀L1. h ⊢ L1 ¡⊑[g] L2 → ⦃h, L1⦄ ⊢ T ¡[g].
+
+(* Properties for the preservation results **********************************)
+
+fact snv_ltpr_cpr_aux: ∀h,g,L1,T1. IH_snv_ltpr_tpr h g L1 T1 →
+                       ⦃h, L1⦄ ⊢ T1 ¡[g] →
+                       ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡ T2 → ⦃h, L2⦄ ⊢ T2 ¡[g].
+#h #g #L1 #T1 #IH #HT1 #L2 #HL12 #T2 * #T #HT1T #HTT2
+lapply (IH … HL12 … HT1T) -HL12 // -T1 #HT0
+lapply (snv_tpss_conf … HT0 … HTT2) -T //
+qed-.
+
+fact ssta_ltpr_cpr_aux: ∀h,g,L1,T1. IH_ssta_ltpr_tpr h g L1 T1 →
+                        ⦃h, L1⦄ ⊢ T1 ¡[g] →
+                        ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l, U1⦄ →
+                        ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡ T2 →
+                        ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l, U2⦄ & L2 ⊢ U1 ⬌* U2.
+#h #g #L1 #T1 #IH #HT1 #U1 #l #HTU1 #L2 #HL12 #T2 * #T #HT1T #HTT2
+elim (IH … HTU1 … HL12 … HT1T) // -L1 -T1 #U #HTU #HU1
+elim (ssta_tpss_conf … HTU … HTT2) -T #U2 #HTU2 #HU2
+lapply (cpcs_cpr_strap1 … HU1 U2 ?) /2 width=3/
+qed-.
+
+fact snv_ltpr_cprs_aux: ∀h,g,L0,T0.
+                        (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) →
+                        ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[g] →
+                        ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡* T2 → ⦃h, L2⦄ ⊢ T2 ¡[g].
+#h #g #L0 #T0 #IH #L1 #T1 #HLT0 #HT1 #L2 #HL12 #T2 #H
+@(cprs_ind … H) -T2 [ /2 width=6 by snv_ltpr_cpr_aux/ ] -HT1
+/5 width=6 by snv_ltpr_cpr_aux, ygt_yprs_trans, ltpr_cprs_yprs/
+qed-.
+
+fact ssta_ltpr_cprs_aux: ∀h,g,L0,T0.
+                         (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) →
+                         (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) →
+                         ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[g] →
+                         ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l, U1⦄ →
+                         ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡* T2 →
+                         ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l, U2⦄ & L2 ⊢ U1 ⬌* U2.
+#h #g #L0 #T0 #IH2 #IH1 #L1 #T1 #H01 #HT1 #U1 #l #HTU1 #L2 #HL12 #T2 #H
+@(cprs_ind … H) -T2 [ /2 width=7 by ssta_ltpr_cpr_aux/ ]
+#T #T2 #HT1T #HTT2 * #U #HTU #HU1
+elim (ssta_ltpr_cpr_aux … HTU … HTT2) //
+[2: /3 width=9 by snv_ltpr_cprs_aux/
+|3: /5 width=6 by ygt_yprs_trans, ltpr_cprs_yprs/
+] -L0 -L1 -T0 -T1 -T #U2 #HTU2 #HU2
+lapply (cpcs_trans … HU1 … HU2) -U /2 width=3/
+qed-.
+
+fact ssta_ltpr_cpcs_aux: ∀h,g,L0,T0.
+                         (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) →
+                         (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) →
+                         ∀L1,L2,T1,T2. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → h ⊢ ⦃L0, T0⦄ >[g] ⦃L2, T2⦄ →
+                         ⦃h, L1⦄ ⊢ T1 ¡[g] → ⦃h, L2⦄ ⊢ T2 ¡[g] →
+                         ∀U1,l1. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l1, U1⦄ →
+                         ∀U2,l2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l2, U2⦄ →
+                         L1 ➡ L2 → L2 ⊢ T1 ⬌* T2 →
+                         l1 = l2 ∧ L2 ⊢ U1 ⬌* U2.
+#h #g #L0 #T0 #IH2 #IH1 #L1 #L2 #T1 #T2 #HLT01 #HLT02 #HT1 #HT2 #U1 #l1 #HTU1 #U2 #l2 #HTU2 #HL12 #H
+elim (cpcs_inv_cprs … H) -H #T #H1 #H2
+elim (ssta_ltpr_cprs_aux … HLT01 HT1 … HTU1 … H1) -T1 /2 width=1/ #W1 #H1 #HUW1
+elim (ssta_ltpr_cprs_aux … HLT02 HT2 … HTU2 … H2) -T2 /2 width=1/ #W2 #H2 #HUW2 -L1 -L0 -T0
+elim (ssta_mono … H1 … H2) -h -T #H1 #H2 destruct
+lapply (cpcs_canc_dx … HUW1 … HUW2) -W2 /2 width=1/
+qed-.
+
+fact snv_sstas_aux: ∀h,g,L0,T0.
+                    (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) →
+                    ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[g] →
+                    ∀U1. ⦃h, L1⦄ ⊢ T1 •*[g] U1 → ⦃h, L1⦄ ⊢ U1 ¡[g].
+#h #g #L0 #T0 #IH #L1 #T1 #HLT0 #HT1 #U1 #H
+@(sstas_ind … H) -U1 // -HT1 /4 width=5 by ygt_yprs_trans, sstas_yprs/
+qed-.
+
+fact sstas_ltpr_cprs_aux: ∀h,g,L0,T0.
+                          (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) →
+                          (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) →
+                          (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) →
+                          ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[g] →
+                          ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡* T2 → ∀U1. ⦃h, L1⦄ ⊢ T1 •*[g] U1 →
+                          ∃∃U2. ⦃h, L2⦄ ⊢ T2 •*[g] U2 & L2 ⊢ U1 ⬌* U2.
+#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 #T1 #H01 #HT1 #L2 #HL12 #T2 #HT12 #U1 #H
+@(sstas_ind … H) -U1 [ /3 width=3/ ]
+#U1 #W1 #l1 #HTU1 #HUW1 * #U2 #HTU2 #HU12
+lapply (snv_ltpr_cprs_aux … IH2 … HT1 … HT12) // #HT2
+elim (snv_sstas_fwd_correct … HTU2) // #W2 #l2 #HUW2
+elim (ssta_ltpr_cpcs_aux … IH2 IH1 … HUW1 … HUW2 … HU12) -IH2 -IH1 -HUW1 -HU12 //
+[2: /4 width=8 by snv_sstas_aux, ygt_yprs_trans, ltpr_cprs_yprs/
+|3: /3 width=7 by snv_sstas_aux, ygt_yprs_trans, cprs_yprs/
+|4: /4 width=5 by ygt_yprs_trans, ltpr_cprs_yprs, sstas_yprs/
+|5: /3 width=4 by ygt_yprs_trans, cprs_yprs, sstas_yprs/
+] -L0 -T0 -T1 -HT2 #H #HW12 destruct /3 width=4/
+qed-.
+
+fact dxprs_ltpr_cprs_aux: ∀h,g,L0,T0.
+                          (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) →
+                          (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) →
+                          (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) →
+                          ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[g] →
+                          ∀U1. ⦃h, L1⦄ ⊢ T1 •*➡*[g] U1 →
+                          ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡* T2 →
+                          ∃∃U2. ⦃h, L2⦄ ⊢ T2 •*➡*[g] U2 & L2 ⊢ U1 ➡* U2.
+#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 #T1 #H01 #HT1 #U1 * #W1 #HTW1 #HWU1 #L2 #HL12 #T2 #HT12
+elim (sstas_ltpr_cprs_aux … IH3 IH2 IH1 … H01 … HT12 … HTW1) // -L0 -T0 -T1 #W2 #HTW2 #HW12
+lapply (ltpr_cprs_conf … HL12 … HWU1) -L1 #HWU1
+lapply (cpcs_canc_sn … HW12 HWU1) -W1 #H
+elim (cpcs_inv_cprs … H) -H /3 width=3/
+qed-.
+
+fact ssta_dxprs_aux: ∀h,g,L0,T0.
+                     (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) →
+                     (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) →
+                     ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[g] →
+                     ∀l,U1. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l+1, U1⦄ → ∀T2. ⦃h, L1⦄ ⊢ T1 •*➡*[g] T2 →
+                     ∃∃U,U2. ⦃h, L1⦄ ⊢ U1 •*[g] U & ⦃h, L1⦄ ⊢ T2 •*[g] U2 & L1 ⊢ U ⬌* U2.
+#h #g #L0 #T0 #IH2 #IH1 #L1 #T1 #H01 #HT1 #l #U1 #HTU1 #T2 * #T #HT1T #HTT2
+elim (sstas_strip … HT1T … HTU1) #HU1T destruct [ -HT1T | -L0 -T0 -T1 ]
+[ elim (ssta_ltpr_cprs_aux … IH2 IH1 … HTU1 L1 … HTT2) // -L0 -T0 -T /3 width=5/
+| @(ex3_2_intro …T2 HU1T) // /2 width=1/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/preservation/snv_ltpr.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/preservation/snv_ltpr.etc
new file mode 100644
index 000000000..6a0be5953
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/preservation/snv_ltpr.etc
@@ -0,0 +1,113 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/computation/dxprs_dxprs.ma".
+include "basic_2/dynamic/snv_cpcs.ma".
+
+(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
+
+(* Properties on context-free parallel reduction for local environments *****)
+
+fact snv_ltpr_tpr_aux: ∀h,g,L0,T0.
+                       (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_lsubsv h g L1 T1) →
+                       (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) →
+                       (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) →
+                       (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) →
+                       ∀L1,T1. L0 = L1 → T0 = T1 → IH_snv_ltpr_tpr h g L1 T1.
+#h #g #L0 #T0 #IH4 #IH3 #IH2 #IH1 #L1 * * [||||*]
+[ #k #HL0 #HT0 #H1 #L2 #_ #X #H2 destruct -IH4 -IH3 -IH2 -IH1 -L1
+  >(tpr_inv_atom1 … H2) -X //
+| #i #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct -IH4 -IH3 -IH2
+  elim (snv_inv_lref … H1) -H1 #I #K1 #V1 #HLK1 #HV1
+  >(tpr_inv_atom1 … H2) -X
+  elim (ltpr_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2
+  elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct
+  lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) -HLK1 #HLK1
+  lapply (IH1 … HK12 … HV12) -IH1 -HV12 -HK12 // -HV1 [ /2 width=1/ ] -HLK1 /2 width=5/
+| #p #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct -IH4 -IH3 -IH2 -IH1
+  elim (snv_inv_gref … H1)
+| #a #I #V1 #T1 #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct -IH4 -IH3 -IH2
+  elim (snv_inv_bind … H1) -H1 #HV1 #HT1
+  elim (tpr_inv_bind1 … H2) -H2 *
+  [ #V2 #T0 #T2 #HV12 #HT10 #HT02 #H destruct
+    lapply (tps_lsubr_trans … HT02 (L2.ⓑ{I}V2) ?) -HT02 /2 width=1/ #HT02
+    lapply (IH1 … HL12 … HV12) // [ /2 width=1/ ] #HV2
+    lapply (snv_ltpr_cpr_aux … HT1  (L2.ⓑ{I}V2) … T2 ?) -HT1
+    [ /3 width=5 by cpr_intro, tps_tpss/ | /2 width=1/ | /3 width=1/ ] -IH1 -T0 /2 width=1/
+  | #T2 #HT12 #HXT2 #H1 #H2 destruct
+    lapply (IH1 … HT1 (L2.ⓓV1) … HT12) -IH1 -HT1 -HT12 [1,2: /2 width=1/ ] -HL12 #HT2
+    lapply (snv_inv_lift … HT2 L2 … HXT2) -T2 // /2 width=1/
+  ]
+| #V1 #T1 #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct
+  elim (snv_inv_appl … H1) -H1 #a #W10 #W1 #U1 #l #HV1 #HT1 #HVW1 #HW10 #HTU1
+  elim (tpr_inv_appl1 … H2) -H2 *
+  [ #V2 #T2 #HV12 #HT12 #H destruct -IH4
+    lapply (IH1 … HV1 … HL12 … HV12) [ /2 width=1/ ] #HV2
+    lapply (IH1 … HT1 … HL12 … HT12) [ /2 width=1/ ] #HT2
+    elim (IH3 … HVW1 … HL12 … HV12) -HVW1 -HV12 // -HV1 [2: /2 width=1/ ] #W2 #HVW2 #HW12
+    elim (dxprs_ltpr_cprs_aux … IH2 IH1 IH3 … HTU1 … HL12 T2) // [2: /3 width=1/ |3: /2 width=1/ ] -IH2 -IH1 -IH3 -HT1 -HT12 -HTU1 #X #HTU2 #H
+    elim (cprs_inv_abst1 Abst W1 … H) -H #W20 #U2 #HW120 #_ #H destruct
+    lapply (ltpr_cprs_conf … HL12 … HW10) -L1 #HW10
+    lapply (cpcs_cprs_strap1 … HW10 … HW120) -W1 #HW120
+    lapply (cpcs_canc_sn … HW12 HW120) -W10 #HW20
+    elim (cpcs_inv_cprs … HW20) -HW20 #W0 #HW20 #HW200
+    lapply (dxprs_cprs_trans … (ⓛ{a}W0.U2) HTU2 ?) [ /2 width=1/ ] -HW200 -HTU2 /2 width=8/
+  | #b #V2 #W20 #T20 #T2 #HV12 #HT202 #H1 #H2 destruct
+    elim (snv_inv_bind … HT1) -HT1 #HW20 #HT20
+    elim (dxprs_inv_abst1 … HTU1) -HTU1 #W30 #T30 #HW230 #_ #H destruct -T30
+    lapply (cprs_div … HW10 … HW230) -W30 #HW120
+    elim (snv_fwd_ssta … HW20) #l0 #U20 #HWU20
+    elim (ssta_fwd_correct … HVW1) <minus_plus_m_m #U10 #HWU10
+    elim (ssta_ltpr_cpcs_aux … IH1 IH3 … HW20 … HWU10 … HWU20) // -IH3 -HWU10
+    [2: /3 width=5/ |3: /2 width=1/
+    |4: /4 width=4 by ygt_yprs_trans, fw_ygt, sstas_yprs, ssta_sstas/
+    ] #H #_ -IH2 -U10 destruct
+    lapply (IH4 … HT20 (L1.ⓓV1) ?) [ /2 width=6/ | /2 width=1/ ] -U20 -W10 -l0 -IH4 -HT20 -HW20 #HT20
+    lapply (IH1 … HL12 … HV12) // [ /2 width=1/ ] #HV2
+    lapply (IH1 … HT20 … (L2.ⓓV2) … HT202) [1,2: /2 width=1/ ] -L1 -V1 -W20 -T20 /2 width=1/
+  | #b #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HW02 #HT02 #HV02 #H1 #H2 destruct -IH4
+    elim (snv_inv_bind … HT1) -HT1 #HW0 #HT0
+    elim (dxprs_inv_abbr_abst … HTU1) -HTU1 #X #HTU0 #HX #H destruct
+    elim (lift_inv_bind1 … HX) -HX #W3 #U3 #HW13 #_ #H destruct
+    lapply (ltpr_cprs_conf … HL12 … HW10) -HW10 #HW10
+    elim (dxprs_ltpr_cprs_aux … IH2 IH1 IH3 … HTU0 (L2.ⓓW2) … T2 ?) // [2: /3 width=1/ |3,4: /2 width=1/ ] -IH2 -HTU0 #X #HTU2 #H
+    elim (cprs_inv_abst1 Abst W3 … H) -H #W #U2 #HW1 #_ #H destruct -U3
+    elim (IH3 … HVW1 … HL12 … HV10) // /2 width=1/ -IH3 -HVW1 #X #H1 #H2
+    lapply (cpcs_canc_sn … H2 HW10) -W10 #H2
+    elim (lift_total X 0 1) #W20 #H3
+    lapply (ssta_lift … H1 (L2.ⓓW2) … HV02 … H3) /2 width=1/ -H1 #HVW20
+    lapply (cpcs_lift (L2.ⓓW2) … H3 … HW13 H2) /2 width=1/ -HW13 -H3 -H2 #HW320
+    lapply (cpcs_cprs_strap1 … HW320 … HW1) -W3 #HW20
+    elim (cpcs_inv_cprs … HW20) -HW20 #W3 #HW203 #HW3
+    lapply (dxprs_cprs_trans … (ⓛ{a}W3.U2) HTU2 ?) [ /2 width=1/ ] -HW3 -HTU2 #HTU2
+    lapply (IH1 … HL12 … HW02) // [ /2 width=1/ ] -HW0 #HW2
+    lapply (IH1 … HL12 … HV10) // [ /2 width=1/ ] -HV1 -HV10 #HV0
+    lapply (IH1 … HT0 … (L2.ⓓW2) … HT02) [1,2: /2 width=1/ ] -L1 -HT02 -HW02 #HT2
+    lapply (snv_lift … HV0 (L2.ⓓW2) … HV02) /2 width=1/ -HV0 -HV02 /3 width=8/
+  ]
+| #W1 #T1 #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct -IH4 -IH2
+  elim (snv_inv_cast … H1) -H1 #U1 #l #HW1 #HT1 #HTU1 #HUW1
+  elim (tpr_inv_cast1 … H2) -H2
+  [ * #W2 #T2 #HW12 #HT12 #H destruct
+    lapply (cpcs_cprs_strap1 … HUW1 W2 ?) [ /3 width=1/ ] -HUW1 #H1
+    lapply (IH1 … HL12 … HW12) // /2 width=1/ -HW1 -HW12 #HW2
+    lapply (IH1 … HL12 … HT12) // /2 width=1/ -IH1 #HT2
+    elim (IH3 … HTU1 … HL12 … HT12) // /2 width=1/ -IH3 -HT1 -HT12 -HTU1 #U2 #HTU2 #HU12
+    lapply (ltpr_cpcs_conf … HL12 … H1) -L1 #H1
+    lapply (cpcs_canc_sn … HU12 H1) -U1 /2 width=4/
+  | #H -IH3 -HW1 -HTU1 -HUW1
+    lapply (IH1 … HL12 … H) // /2 width=1/
+  ]
+]  
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/preservation/snv_ssta_ltpr.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/preservation/snv_ssta_ltpr.etc
new file mode 100644
index 000000000..e7f402513
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/preservation/snv_ssta_ltpr.etc
@@ -0,0 +1,120 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/lsubss_ssta.ma".
+include "basic_2/dynamic/snv_cpcs.ma".
+
+(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
+
+(* Properties on context-free parallel reduction for local environments *****)
+
+fact ssta_ltpr_tpr_aux: ∀h,g,L0,T0.
+                        (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) →
+                        (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) →
+                        (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) →
+                        ∀L1,T1. L0 = L1 → T0 = T1 → IH_ssta_ltpr_tpr h g L1 T1.
+#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 * * [|||| *]
+[ #k #_ #_ #_ #X2 #l #H2 #L2 #HL12 #X3 #H3 -IH3 -IH2 -IH1
+  elim (ssta_inv_sort1 … H2) -H2 #Hkl #H destruct
+  >(tpr_inv_atom1 … H3) -X3 /4 width=6/
+| #i #HL0 #HT0 #H1 #X2 #l #H2 #L2 #HL12 #X3 #H3 destruct -IH3 -IH2
+  elim (snv_inv_lref … H1) -H1 #I0 #K0 #V0 #H #HV1
+  elim (ssta_inv_lref1 … H2) -H2 * #K1
+  >(tpr_inv_atom1 … H3) -X3
+  [ #V1 #W1 #HLK1 #HVW1 #HWU1
+    lapply (ldrop_mono … H … HLK1) -H #H destruct
+    lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) #HKV1
+    elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #H #HLK2
+    elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct
+    elim (IH1 … HVW1 … HK12 … HV12) -IH1 -HVW1 -HV12 // [2: /2 width=1/ ] -V1 #W2 #HVW2 #HW12
+    lapply (ldrop_fwd_ldrop2 … HLK2) #H2
+    elim (lift_total W2 0 (i+1)) #U2 #HWU2
+    lapply (cpcs_lift … H2 … HWU1 … HWU2 HW12) -H2 -W1 /3 width=6/
+  | #V1 #W1 #l0 #HLK1 #HVW1 #HVU1 #H destruct
+    lapply (ldrop_mono … H … HLK1) -H #H destruct
+    lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) #HKV1
+    elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 #X #H #HLK2
+    elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct
+    elim (IH1 … HVW1 … HK12 … HV12) -IH1 -HVW1 -HK12 // [2: /2 width=1/ ] -HV1 -HKV1 #W2 #HVW2 #_ -W1
+    elim (lift_total V2 0 (i+1)) #U2 #HVU2
+    lapply (tpr_lift … HV12 … HVU1 … HVU2) -V1 /4 width=6/
+  ]
+| #p #_ #HT0 #H1 destruct -IH3 -IH2 -IH1
+  elim (snv_inv_gref … H1)
+| #a #I #V1 #T1 #HL0 #HT0 #H1 #X2 #l #H2 #L2 #HL12 #X3 #H3 destruct -IH3 -IH2
+  elim (snv_inv_bind … H1) -H1 #_ #HT1
+  elim (ssta_inv_bind1 … H2) -H2 #U1 #HTU1 #H destruct
+  elim (tpr_inv_bind1 … H3) -H3 *
+  [ #V2 #T0 #T2 #HV12 #HT10 #HT02 #H destruct
+    lapply (tps_lsubr_trans … HT02 (L2.ⓑ{I}V2) ?) -HT02 [ /2 width=1/ ] #HT02
+    elim (ssta_ltpr_cpr_aux … HT1 … HTU1 (L2.ⓑ{I}V2) … T2) -HT1 -HTU1
+    [2: /3 width=5 by cpr_intro, tps_tpss/ |3: /2 width=1/ |4: /3 width=1/ ] -IH1 -T0 -HL12 #U2 #HTU2 #HU12
+    lapply (cpcs_bind2 … V1 … HU12 … a) -HU12 [ /2 width=1/ ] -HV12 /3 width=3/
+  | #T2 #HT12 #HT2 #H1 #H2 destruct
+    elim (IH1 … HTU1 (L2.ⓓV1) … T2) -IH1 -HTU1 // [2,3: /2 width=1/ ] -T1 -HL12 #U2 #HTU2 #HU12
+    lapply (cpcs_bind1 … HU12 … V1 … true) // -HU12 #HU12
+    elim (ssta_inv_lift1 … HTU2 … HT2) -T2 [3: /2 width=1/ |2: skip ] #U #HXU #HU2
+    lapply (cpcs_cpr_strap1 … HU12 U ?) -HU12 [ /3 width=3/ ] -U2 /2 width=3/
+  ]
+| #V1 #T1 #HL0 #HT0 #H1 #X2 #l #H2 #L2 #HL12 #X3 #H3 destruct
+  elim (snv_inv_appl … H1) -H1 #a #W1 #W10 #U10 #l0 #HV1 #HT1 #HVW1 #HW10 #HTU10
+  elim (ssta_inv_appl1 … H2) -H2 #U1 #HTU1 #H destruct
+  elim (tpr_inv_appl1 … H3) -H3 *
+  [ #V2 #T2 #HV12 #HT12 #H destruct -a -l0 -W1 -W10 -U10 -HV1 -IH3 -IH2
+    elim (IH1 … HTU1 … HL12 … HT12) -IH1 -HTU1 -HL12 // [2: /2 width=1/ ] -T1 #U2 #HTU2 #HU12
+    lapply (cpcs_flat … V1 V2 … HU12) -HU12 [ /2 width=1/ ] -HV12 /3 width=3/
+  | #b #V2 #W #T2 #T20 #HV12 #HT20 #H1 #H2 destruct
+    elim (snv_inv_bind … HT1) -HT1 #HW #HT2
+    elim (ssta_inv_bind1 … HTU1) -HTU1 #U2 #HTU2 #H destruct
+    elim (dxprs_inv_abst1 … HTU10) -HTU10 #W0 #U0 #HW0 #_ #H destruct
+    lapply (cprs_div … HW10 … HW0) -W0 #HW1W
+    elim (ssta_fwd_correct … HVW1) <minus_plus_m_m #X1 #HWX1
+    elim (snv_fwd_ssta … HW) #l1 #V #HWV
+    lapply (IH3 … HVW1) -IH3 // [ /2 width=1/ ] #HW1
+    elim (ssta_ltpr_cpcs_aux … IH2 IH1 … HWX1 … HWV …) -IH2 -HWX1 //
+    [2: /2 width=1/
+    |3: /4 width=4 by ygt_yprs_trans, fw_ygt, sstas_yprs, ssta_sstas/
+    ] #H #_ destruct -X1
+    elim (IH1 … HVW1 … HL12 … HV12) -HVW1 // -HV1 [2: /2 width=1/ ] #W2 #HVW2 #HW12
+    elim (IH1 … HWV … HL12 W) -HWV // -HW [2: /2 width=1/ ] #V0 #HWV0 #_
+    elim (IH1 … HTU2 (L2.ⓛW) … HT20) -IH1 -HTU2 -HT20 // [2,3: /2 width=1/ ] -HT2 #U20 #HTU20 #HU20
+    lapply (ltpr_cpcs_conf … HL12 … HW1W) -L1 #HW1W
+    lapply (cpcs_canc_sn … HW12 HW1W) -W1 #HW2
+    elim (lsubss_ssta_trans … HTU20 (L2.ⓓV2) ?) -HTU20
+    [ #U #HTU20 #HUU20 -HWV0 -W2
+      @(ex2_intro … (ⓓ{b}V2.U)) [ /2 width=1/ ] -h -l -l1 -V -V0 -T2 -T20 -U0
+      @(cpcs_cprs_strap2 … (ⓓ{b}V2.U2)) [ /3 width=1/ ] -V1
+      @(cpcs_canc_dx … (ⓓ{b}V2.U20)) /2 width=2/
+    | -b -l -V -V1 -T2 -T20 -U0 -U2 -U20 /2 width=6/
+    ]
+  | #b #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HW02 #HT02 #HV02 #H1 #H2 destruct -a -l0 -W1 -W10 -HV1 -IH3 -IH2
+    elim (ssta_inv_bind1 … HTU1) -HTU1 #U0 #HTU0 #H destruct
+    elim (snv_inv_bind … HT1) -HT1 #_ #HT0
+    elim (IH1 … HTU0 (L2.ⓓW2) … HT02) -IH1 -HTU0 // [2,3: /2 width=1/ ] -T0 -HL12 #U2 #HTU2 #HU02
+    lapply (cpcs_bind2 … W0 … HU02 b) -HU02 [ /2 width=1/ ] #HU02
+    lapply (cpcs_flat … V1 V0 … HU02 Appl) [ /2 width=1/ ] -HV10 -HU02 #HU02
+    lapply (cpcs_cpr_strap1 … HU02 (ⓓ{b}W2.ⓐV2.U2) ?) -HU02 [ /3 width=3/ ] -V0 -HW02 /4 width=3/
+  ]
+| #U0 #T1 #HL0 #HT0 #H1 #X2 #l #H2 #L2 #HL12 #X3 #H3 destruct -IH3 -IH2
+  elim (snv_inv_cast … H1) -H1 #T0 #l0 #_ #HT1 #HT10 #_
+  lapply (ssta_inv_cast1 … H2) -H2 #HTU1
+  elim (ssta_mono … HT10 … HTU1) -HT10 #H1 #H2 destruct
+  elim (tpr_inv_cast1 … H3) -H3
+  [ * #U2 #T2 #_ #HT12 #H destruct
+    elim (IH1 … HTU1 … HL12 … HT12) -IH1 -HTU1 -HL12 // [2: /2 width=1/ ] -T1 -U0 /3 width=3/
+  | #HT1X3
+    elim (IH1 … HTU1 … HL12 … HT1X3) -IH1 -HTU1 -HL12 // [2: /2 width=1/ ] -U0 -T1 /2 width=3/
+  ]
+]
+qed-.
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 753cddf6f..96b64d882 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
@@ -44,7 +44,7 @@ table {
           }
         ]
         [ { "stratified native validity" * } {
-             [ "snv ( ⦃?,?⦄ ⊢ ? ¡[?] )" "snv_lift" + "snv_lpss" + "snv_aaa" + "snv_ssta" + "snv_sstas" + "snv_ssta_ltpr" + "snv_ltpr" + "snv_cpcs" * ]
+             [ "snv ( ⦃?,?⦄ ⊢ ? ¡[?] )" "snv_lift" + "snv_lpss" + "snv_aaa" + "snv_ssta" + "snv_sstas" + "snv_ssta_lpr" + "snv_lpr" + "snv_cpcs" * ]
           }
         ]
      }