From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 6 Aug 2014 18:52:13 +0000 (+0000)
Subject: - some renaming and minor updates
X-Git-Tag: make_still_working~861
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=5902d6da146ca78b0ed5d062e3968f52868147c5

- some renaming and minor updates
---

diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile
index 15c38d009..5dc025fc3 100644
--- a/matita/matita/contribs/lambdadelta/Makefile
+++ b/matita/matita/contribs/lambdadelta/Makefile
@@ -247,7 +247,7 @@ trim: $(TRIMS:%=%.trimmed)
 # contrib ####################################################################
 
 contrib:
-	@echo "  TAR -czf $(CONTRIB).tar.gz root *.ma"
+	@echo "  TAR -czf $(CONTRIB).tar.gz root $(XPACKAGES)"
 	$(H)tar -czf $(CONTRIB).tar.gz root $(XMAS)
 
 ##############################################################################
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma
index a7281d511..f5b3f6a05 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma
@@ -124,22 +124,22 @@ lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) 
   | #H @(cp2 … H1RP … k) @(s1 … IHA) //
   ]
 | #G #L #Vs #HVs #T #H1T #H2T #L0 #V0 #X #des #HB #HL0 #H
-  elim (lifts_inv_appls1 … H) -H #V0s #T0 #HV0s #HT0 #H destruct
+  elim (lifts_inv_applv1 … H) -H #V0s #T0 #HV0s #HT0 #H destruct
   lapply (s1 … IHB … HB) #HV0
   @(s2 … IHA … (V0 @ V0s))
   /3 width=14 by rp_liftsv_all, acp_lifts, cp0, lifts_simple_dx, conj/
 | #a #G #L #Vs #U #T #W #HA #L0 #V0 #X #des #HB #HL0 #H
-  elim (lifts_inv_appls1 … H) -H #V0s #Y #HV0s #HY #H destruct
+  elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
   elim (lifts_inv_flat1 … HY) -HY #U0 #X #HU0 #HX #H destruct
   elim (lifts_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT0 #H destruct
-  @(s3 … IHA … (V0 @ V0s)) /5 width=6 by lifts_appls, lifts_flat, lifts_bind/
+  @(s3 … IHA … (V0 @ V0s)) /5 width=6 by lifts_applv, lifts_flat, lifts_bind/
 | #G #L #Vs #HVs #k #L0 #V0 #X #des #HB #HL0 #H
-  elim (lifts_inv_appls1 … H) -H #V0s #Y #HV0s #HY #H destruct
+  elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
   >(lifts_inv_sort1 … HY) -Y
   lapply (s1 … IHB … HB) #HV0
   @(s4 … IHA … (V0 @ V0s)) /3 width=7 by rp_liftsv_all, conj/
 | #I #G #L #K #Vs #V1 #V2 #i #HA #HV12 #HLK #L0 #V0 #X #des #HB #HL0 #H
-  elim (lifts_inv_appls1 … H) -H #V0s #Y #HV0s #HY #H destruct
+  elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
   elim (lifts_inv_lref1 … HY) -HY #i0 #Hi0 #H destruct
   elim (drops_drop_trans … HL0 … HLK) #X #des0 #i1 #HL02 #H #Hi1 #Hdes0
   >(at_mono … Hi1 … Hi0) in HL02; -i1 #HL02
@@ -147,23 +147,23 @@ lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) 
   elim (lift_total W1 0 (i0 + 1)) #W2 #HW12
   elim (lifts_lift_trans  … Hdes0 … HVW1 … HW12) // -Hdes0 -Hi0 #V3 #HV13 #HVW2
   >(lift_mono … HV13 … HV12) in HVW2; -V3 #HVW2
-  @(s5 … IHA … (V0 @ V0s) … HW12 HL02) /3 width=5 by lifts_appls/
+  @(s5 … IHA … (V0 @ V0s) … HW12 HL02) /3 width=5 by lifts_applv/
 | #G #L #V1s #V2s #HV12s #a #V #T #HA #HV #L0 #V10 #X #des #HB #HL0 #H
-  elim (lifts_inv_appls1 … H) -H #V10s #Y #HV10s #HY #H destruct
+  elim (lifts_inv_applv1 … H) -H #V10s #Y #HV10s #HY #H destruct
   elim (lifts_inv_bind1 … HY) -HY #V0 #T0 #HV0 #HT0 #H destruct
   elim (lift_total V10 0 1) #V20 #HV120
   elim (liftv_total 0 1 V10s) #V20s #HV120s
   @(s6 … IHA … (V10 @ V10s) (V20 @ V20s)) /3 width=7 by rp_lifts, liftv_cons/
   @(HA … (des + 1)) /2 width=2 by drops_skip/
   [ @(s0 … IHB … HB … HV120) /2 width=2 by drop_drop/
-  | @lifts_appls //
+  | @lifts_applv //
     elim (liftsv_liftv_trans_le … HV10s … HV120s) -V10s #V10s #HV10s #HV120s
     >(liftv_mono … HV12s … HV10s) -V1s //
   ]
 | #G #L #Vs #T #W #HA #HW #L0 #V0 #X #des #HB #HL0 #H
-  elim (lifts_inv_appls1 … H) -H #V0s #Y #HV0s #HY #H destruct
+  elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
   elim (lifts_inv_flat1 … HY) -HY #W0 #T0 #HW0 #HT0 #H destruct
-  @(s7 … IHA … (V0 @ V0s)) /3 width=5 by lifts_appls/
+  @(s7 … IHA … (V0 @ V0s)) /3 width=5 by lifts_applv/
 ]
 qed.
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpds.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpds.ma
deleted file mode 100644
index a2eb23483..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpds.ma
+++ /dev/null
@@ -1,58 +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/notation/relations/dpredstar_7.ma".
-include "basic_2/static/da.ma".
-include "basic_2/unfold/lstas.ma".
-include "basic_2/computation/cprs.ma".
-
-(* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************)
-
-definition cpds: ∀h. sd h → nat → relation4 genv lenv term term ≝
-                 λh,g,l2,G,L,T1,T2.
-                 ∃∃T,l1. l2 ≤ l1 & ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 & ⦃G, L⦄ ⊢ T1 •*[h, l2] T & ⦃G, L⦄ ⊢ T ➡* T2.
-
-interpretation "decomposed extended parallel computation (term)"
-   'DPRedStar h g l G L T1 T2 = (cpds h g l G L T1 T2).
-
-(* Basic properties *********************************************************)
-
-lemma sta_cprs_cpds: ∀h,g,G,L,T1,T,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T1 •[h] T →
-                     ⦃G, L⦄ ⊢ T ➡* T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g, 1] T2.
-/3 width=6 by sta_lstas, ex4_2_intro/ qed.
-
-lemma lstas_cpds: ∀h,g,G,L,T1,T2,l1. ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 →
-                  ∀l2. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 •*[h, l2] T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l2] T2.
-/2 width=6 by ex4_2_intro/ qed.
-
-lemma cprs_cpds: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l → ⦃G, L⦄ ⊢ T1 ➡* T2 →
-                 ⦃G, L⦄ ⊢ T1 •*➡*[h, g, 0] T2.
-/2 width=6 by lstar_O, ex4_2_intro/ qed.
-
-lemma cpds_refl: ∀h,g,G,L,T,l. ⦃G, L⦄ ⊢ T ▪[h, g] l → ⦃G, L⦄ ⊢ T •*➡*[h, g, 0] T.
-/2 width=2 by cprs_cpds/ qed.
-
-lemma cpds_strap1: ∀h,g,G,L,T1,T,T2,l.
-                   ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l] T → ⦃G, L⦄ ⊢ T ➡ T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l] T2.
-#h #g #G #L #T1 #T #T2 #l * /3 width=8 by cprs_strap1, ex4_2_intro/
-qed.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma cpds_fwd_cprs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 •*➡*[h, g, 0] T2 →
-                     ⦃G, L⦄ ⊢ T1 ➡* T2.
-#h #g #G #L #T1 #T2 *
-#T #l #_ #_ #H lapply (lstas_inv_O … H) -l -H
-#H destruct //
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpds_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpds_aaa.ma
deleted file mode 100644
index 8cc7d146e..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpds_aaa.ma
+++ /dev/null
@@ -1,25 +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/unfold/lstas_aaa.ma".
-include "basic_2/computation/cpxs_aaa.ma".
-include "basic_2/computation/cpds.ma".
-
-(* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************)
-
-(* Properties on atomic arity assignment for terms **************************)
-
-lemma cpds_aaa_conf: ∀h,g,G,L,l. Conf3 … (aaa G L) (cpds h g l G L).
-#h #g #G #L #l #A #T #HT #U * /3 width=6 by lstas_aaa_conf, cprs_aaa_conf/
-qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpds_cpds.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpds_cpds.ma
deleted file mode 100644
index d09fe1ebb..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpds_cpds.ma
+++ /dev/null
@@ -1,92 +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/unfold/lstas_lstas.ma".
-include "basic_2/computation/lprs_cprs.ma".
-include "basic_2/computation/cpxs_cpxs.ma".
-include "basic_2/computation/cpds.ma".
-
-(* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************)
-
-(* Advanced properties ******************************************************)
-
-lemma cpds_strap2: ∀h,g,G,L,T1,T,T2,l1,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l1+1 →
-                   ⦃G, L⦄ ⊢ T1 •[h] T → ⦃G, L⦄ ⊢ T •*➡*[h, g, l] T2 →
-                   ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l+1] T2.
-#h #g #G #L #T1 #T #T2 #l1 #l #Hl1 #HT1 *
-#T0 #l0 #Hl0 #HTl0 #HT0 #HT02
-lapply (da_sta_conf … HT1 … Hl1) <minus_plus_m_m #HTl1
-lapply (da_mono … HTl0 … HTl1) -HTl0 -HTl1 #H destruct
-/3 width=6 by lstas_step_sn, le_S_S, ex4_2_intro/
-qed.
-
-lemma cpds_cprs_trans: ∀h,g,G,L,T1,T,T2,l.
-                       ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l] T → ⦃G, L⦄ ⊢ T ➡* T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l] T2.
-#h #g #G #L #T1 #T #T2 #l * /3 width=8 by cprs_trans, ex4_2_intro/
-qed-.
-
-lemma lstas_cpds_trans: ∀h,g,G,L,T1,T,T2,l1,l2,l.
-                        l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 →
-                        ⦃G, L⦄ ⊢ T1 •*[h, l2] T → ⦃G, L⦄ ⊢ T •*➡*[h, g, l] T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l2+l] T2.
-#h #g #G #L #T1 #T #T2 #l1 #l2 #l #Hl21 #HTl1 #HT1 * #T0 #l0 #Hl0 #HTl0 #HT0 #HT02
-lapply (lstas_da_conf … HT1 … HTl1) #HTl12
-lapply (da_mono … HTl12 … HTl0) -HTl12 -HTl0 #H destruct
-lapply (le_minus_to_plus_r … Hl21 Hl0) -Hl21 -Hl0
-/3 width=7 by lstas_trans, ex4_2_intro/
-qed-.
-
-(* Advanced inversion lemmas ************************************************)
-
-lemma cpds_inv_abst1: ∀h,g,a,G,L,V1,T1,U2,l. ⦃G, L⦄ ⊢ ⓛ{a}V1.T1 •*➡*[h, g, l] U2 →
-                      ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡* V2 & ⦃G, L.ⓛV1⦄ ⊢ T1 •*➡*[h, g, l] T2 &
-                               U2 = ⓛ{a}V2.T2.
-#h #g #a #G #L #V1 #T1 #U2 #l2 * #X #l1 #Hl21 #Hl1 #H1 #H2
-lapply (da_inv_bind … Hl1) -Hl1 #Hl1
-elim (lstas_inv_bind1 … H1) -H1 #U #HTU1 #H destruct
-elim (cprs_inv_abst1 … H2) -H2 #V2 #T2 #HV12 #HUT2 #H destruct
-/3 width=6 by ex4_2_intro, ex3_2_intro/
-qed-.
-
-lemma cpds_inv_abbr_abst: ∀h,g,a1,a2,G,L,V1,W2,T1,T2,l. ⦃G, L⦄ ⊢ ⓓ{a1}V1.T1 •*➡*[h, g, l] ⓛ{a2}W2.T2 →
-                          ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 •*➡*[h, g, l] T & ⇧[0, 1] ⓛ{a2}W2.T2 ≡ T & a1 = true.
-#h #g #a1 #a2 #G #L #V1 #W2 #T1 #T2 #l2 * #X #l1 #Hl21 #Hl1 #H1 #H2
-lapply (da_inv_bind … Hl1) -Hl1 #Hl1
-elim (lstas_inv_bind1 … H1) -H1 #U1 #HTU1 #H destruct
-elim (cprs_inv_abbr1 … H2) -H2 *
-[ #V2 #U2 #HV12 #HU12 #H destruct
-| /3 width=6 by ex4_2_intro, ex3_intro/
-]
-qed-.
-
-lemma cpds_inv_lstas_eq: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l] T2 →
-                         ∀T. ⦃G, L⦄ ⊢ T1 •*[h, l] T → ⦃G, L⦄ ⊢ T ➡* T2.
-#h #g #G #L #T1 #T2 #l2 *
-#T0 #l1 #_ #_ #HT10 #HT02 #T #HT1
-lapply (lstas_mono … HT10 … HT1) #H destruct //
-qed-.
-
-(* Advanced forward lemmas **************************************************)
-
-lemma cpds_fwd_cpxs: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l] T2 → ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2.
-#h #g #G #L #T1 #T2 #l * /3 width=5 by cpxs_trans, lstas_cpxs, cprs_cpxs/
-qed-.
-
-(* Main properties **********************************************************)
-
-theorem cpds_conf_eq: ∀h,g,G,L,T0,T1,l. ⦃G, L⦄ ⊢ T0 •*➡*[h, g, l] T1 →
-                      ∀T2. ⦃G, L⦄ ⊢ T0 •*➡*[h, g, l] T2 →
-                      ∃∃T. ⦃G, L⦄ ⊢ T1 ➡* T & ⦃G, L⦄ ⊢ T2 ➡* T.
-#h #g #G #L #T0 #T1 #l0 * #U1 #l1 #_ #_ #H1 #HUT1 #T2 * #U2 #l2 #_ #_ #H2 #HUT2 -l1 -l2
-lapply (lstas_mono … H1 … H2) #H destruct -h -l0 /2 width=3 by cprs_conf/
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpds_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpds_lift.ma
deleted file mode 100644
index ad37046ed..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpds_lift.ma
+++ /dev/null
@@ -1,36 +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/static/da_lift.ma".
-include "basic_2/unfold/lstas_lift.ma".
-include "basic_2/computation/cprs_lift.ma".
-include "basic_2/computation/cpds.ma".
-
-(* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************)
-
-(* Relocation properties ****************************************************)
-
-lemma cpds_lift: ∀h,g,G,l. l_liftable (cpds h g l G).
-#h #g #G #l2 #K #T1 #T2 * #T #l1 #Hl21 #Hl1 #HT1 #HT2 #L #s #d #e
-elim (lift_total T d e)
-/3 width=15 by cprs_lift, da_lift, lstas_lift, ex4_2_intro/
-qed.
-
-lemma cpds_inv_lift1: ∀h,g,G,l. l_deliftable_sn (cpds h g l G).
-#h #g #G #l2 #L #U1 #U2 * #U #l1 #Hl21 #Hl1 #HU1 #HU2 #K #s #d #e #HLK #T1 #HTU1
-lapply (da_inv_lift … Hl1 … HLK … HTU1) -Hl1 #Hl1
-elim (lstas_inv_lift1 … HU1 … HLK … HTU1) -U1 #T #HTU #HT1
-elim (cprs_inv_lift1 … HU2 … HLK … HTU) -U -L
-/3 width=8 by ex4_2_intro, ex2_intro/
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
index e4c5460d0..a8eb52ab5 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
@@ -140,5 +140,5 @@ qed-.
    pr1_head_1 pr1_head_2 pr1_comp
    clear_pr3_trans pr3_cflat pr3_gen_bind
    pr3_head_1 pr3_head_2 pr3_head_21 pr3_head_12
-   pr3_iso_appl_bind pr3_iso_appls_appl_bind pr3_iso_appls_bind
+   pr3_iso_appl_bind pr3_iso_applv_appl_bind pr3_iso_applv_bind
 *)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc_vector.ma
index 425a7f82a..bb225f6c7 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc_vector.ma
@@ -20,7 +20,7 @@ include "basic_2/computation/cpxs_tstc.ma".
 
 (* Vector form of forward lemmas involving same top term constructor ********)
 
-(* Basic_1: was just: nf2_iso_appls_lref *)
+(* Basic_1: was just: nf2_iso_applv_lref *)
 lemma cpxs_fwd_cnx_vector: ∀h,g,G,L,T.  𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ →
                            ∀Vs,U. ⦃G, L⦄ ⊢ ⒶVs.T ➡*[h, g] U → ⒶVs.T ≂ U.
 #h #g #G #L #T #H1T #H2T #Vs elim Vs -Vs [ @(cpxs_fwd_cnx … H2T) ] (**) (* /2 width=3 by cpxs_fwd_cnx/ does not work *)
@@ -29,10 +29,10 @@ elim (cpxs_inv_appl1 … H) -H *
 [ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by tstc_pair/
 | #a #W0 #T0 #HT0 #HU
   lapply (IHVs … HT0) -IHVs -HT0 #HT0
-  elim (tstc_inv_bind_appls_simple … HT0) //
+  elim (tstc_inv_bind_applv_simple … HT0) //
 | #a #V1 #V2 #V0 #T0 #HV1 #HV12 #HT0 #HU
   lapply (IHVs … HT0) -IHVs -HT0 #HT0
-  elim (tstc_inv_bind_appls_simple … HT0) //
+  elim (tstc_inv_bind_applv_simple … HT0) //
 ]
 qed-.
 
@@ -44,14 +44,14 @@ elim (cpxs_inv_appl1 … H) -H *
 [ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1 by tstc_pair, or_introl/
 | #a #W1 #T1 #HT1 #HU
   elim (IHVs … HT1) -IHVs -HT1 #HT1
-  [ elim (tstc_inv_bind_appls_simple … HT1) //
+  [ elim (tstc_inv_bind_applv_simple … HT1) //
   | @or_intror (**) (* explicit constructor *)
     @(cpxs_trans … HU) -U
     @(cpxs_strap1 … (ⓐV.ⓛ{a}W1.T1)) /3 width=1 by cpxs_flat_dx, cpr_cpx, cpr_beta/
   ]
 | #a #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU
   elim (IHVs … HT1) -IHVs -HT1 #HT1
-  [ elim (tstc_inv_bind_appls_simple … HT1) //
+  [ elim (tstc_inv_bind_applv_simple … HT1) //
   | @or_intror (**) (* explicit constructor *)
     @(cpxs_trans … HU) -U
     @(cpxs_strap1 … (ⓐV1.ⓓ{a}V3.T1)) /3 width=3 by cpxs_flat, cpr_cpx, cpr_theta/
@@ -60,7 +60,7 @@ elim (cpxs_inv_appl1 … H) -H *
 qed-.
 
 
-(* Basic_1: was just: pr3_iso_appls_beta *)
+(* Basic_1: was just: pr3_iso_applv_beta *)
 lemma cpxs_fwd_beta_vector: ∀h,g,a,G,L,Vs,V,W,T,U. ⦃G, L⦄ ⊢ ⒶVs.ⓐV.ⓛ{a}W.T ➡*[h, g] U →
                             ⒶVs. ⓐV. ⓛ{a}W. T ≂ U ∨ ⦃G, L⦄ ⊢ ⒶVs.ⓓ{a}ⓝW.V.T ➡*[h, g] U.
 #h #g #a #G #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_beta/
@@ -69,14 +69,14 @@ elim (cpxs_inv_appl1 … H) -H *
 [ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1 by tstc_pair, or_introl/
 | #b #W1 #T1 #HT1 #HU
   elim (IHVs … HT1) -IHVs -HT1 #HT1
-  [ elim (tstc_inv_bind_appls_simple … HT1) //
+  [ elim (tstc_inv_bind_applv_simple … HT1) //
   | @or_intror (**) (* explicit constructor *)
     @(cpxs_trans … HU) -U
     @(cpxs_strap1 … (ⓐV0.ⓛ{b}W1.T1)) /3 width=1 by cpxs_flat_dx, cpr_cpx, cpr_beta/
   ]
 | #b #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU
   elim (IHVs … HT1) -IHVs -HT1 #HT1
-  [ elim (tstc_inv_bind_appls_simple … HT1) //
+  [ elim (tstc_inv_bind_applv_simple … HT1) //
   | @or_intror (**) (* explicit constructor *)
     @(cpxs_trans … HU) -U
     @(cpxs_strap1 … (ⓐV1.ⓓ{b}V3.T1)) /3 width=3 by cpxs_flat, cpr_cpx, cpr_theta/
@@ -94,14 +94,14 @@ elim (cpxs_inv_appl1 … H) -H *
 [ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by tstc_pair, or_introl/
 | #b #W0 #T0 #HT0 #HU
   elim (IHVs … HT0) -IHVs -HT0 #HT0
-  [ elim (tstc_inv_bind_appls_simple … HT0) //
+  [ elim (tstc_inv_bind_applv_simple … HT0) //
   | @or_intror -i (**) (* explicit constructor *)
     @(cpxs_trans … HU) -U
     @(cpxs_strap1 … (ⓐV.ⓛ{b}W0.T0)) /3 width=1 by cpxs_flat_dx, cpr_cpx, cpr_beta/
   ]
 | #b #V0 #V1 #V3 #T0 #HV0 #HV01 #HT0 #HU
   elim (IHVs … HT0) -IHVs -HT0 #HT0
-  [ elim (tstc_inv_bind_appls_simple … HT0) //
+  [ elim (tstc_inv_bind_applv_simple … HT0) //
   | @or_intror -i (**) (* explicit constructor *)
     @(cpxs_trans … HU) -U
     @(cpxs_strap1 … (ⓐV0.ⓓ{b}V3.T0)) /3 width=3 by cpxs_flat, cpr_cpx, cpr_theta/
@@ -109,7 +109,7 @@ elim (cpxs_inv_appl1 … H) -H *
 ]
 qed-.
 
-(* Basic_1: was just: pr3_iso_appls_abbr *)
+(* Basic_1: was just: pr3_iso_applv_abbr *)
 lemma cpxs_fwd_theta_vector: ∀h,g,G,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
                              ∀a,V,T,U. ⦃G, L⦄ ⊢ ⒶV1s.ⓓ{a}V.T ➡*[h, g] U →
                              ⒶV1s. ⓓ{a}V. T ≂ U ∨ ⦃G, L⦄ ⊢ ⓓ{a}V.ⒶV2s.T ➡*[h, g] U.
@@ -158,7 +158,7 @@ elim (cpxs_inv_appl1 … H) -H *
 ]
 qed-.
 
-(* Basic_1: was just: pr3_iso_appls_cast *)
+(* Basic_1: was just: pr3_iso_applv_cast *)
 lemma cpxs_fwd_cast_vector: ∀h,g,G,L,Vs,W,T,U. ⦃G, L⦄ ⊢ ⒶVs.ⓝW.T ➡*[h, g] U →
                             ∨∨ ⒶVs. ⓝW. T ≂ U
                              | ⦃G, L⦄ ⊢ ⒶVs.T ➡*[h, g] U
@@ -168,7 +168,7 @@ lemma cpxs_fwd_cast_vector: ∀h,g,G,L,Vs,W,T,U. ⦃G, L⦄ ⊢ ⒶVs.ⓝW.T ➡
 elim (cpxs_inv_appl1 … H) -H *
 [ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by tstc_pair, or3_intro0/
 | #b #W0 #T0 #HT0 #HU elim (IHVs … HT0) -IHVs -HT0 #HT0
-  [ elim (tstc_inv_bind_appls_simple … HT0) //
+  [ elim (tstc_inv_bind_applv_simple … HT0) //
   | @or3_intro1 -W (**) (* explicit constructor *)
     @(cpxs_trans … HU) -U
     @(cpxs_strap1 … (ⓐV.ⓛ{b}W0.T0)) /2 width=1 by cpxs_flat_dx, cpx_beta/
@@ -178,7 +178,7 @@ elim (cpxs_inv_appl1 … H) -H *
   ]
 | #b #V0 #V1 #V2 #T0 #HV0 #HV01 #HT0 #HU
   elim (IHVs … HT0) -IHVs -HT0 #HT0
-  [ elim (tstc_inv_bind_appls_simple … HT0) //
+  [ elim (tstc_inv_bind_applv_simple … HT0) //
   | @or3_intro1 -W (**) (* explicit constructor *)
     @(cpxs_trans … HU) -U
     @(cpxs_strap1 … (ⓐV0.ⓓ{b}V2.T0)) /2 width=3 by cpxs_flat, cpx_theta/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx.ma
index cd28a524b..426ae47fa 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx.ma
@@ -129,5 +129,5 @@ lemma csx_fwd_flat: ∀h,g,I,G,L,V,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓕ{I}V.T →
             sn3_cdelta
             sn3_gen_cflat sn3_cflat sn3_cpr3_trans sn3_shift sn3_change
             sn3_appl_cast sn3_appl_beta sn3_appl_lref sn3_appl_abbr
-            sn3_appl_appls sn3_bind sn3_appl_bind sn3_appls_bind
+            sn3_appl_applv sn3_bind sn3_appl_bind sn3_applv_bind
 *)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma
index 765bece71..736b21f3b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma
@@ -21,26 +21,26 @@ include "basic_2/computation/csx_vector.ma".
 
 (* Advanced properties ******************************************************)
 
-(* Basic_1: was just: sn3_appls_lref *)
-lemma csx_appls_cnx: ∀h,g,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ →
+(* Basic_1: was just: sn3_applv_lref *)
+lemma csx_applv_cnx: ∀h,g,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ →
                      ∀Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] Vs → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.T.
 #h #g #G #L #T #H1T #H2T #Vs elim Vs -Vs [ #_ @(cnx_csx … H2T) ] (**) (* /2 width=1/ does not work *)
 #V #Vs #IHV #H
 elim (csxv_inv_cons … H) -H #HV #HVs
-@csx_appl_simple_tstc /2 width=1 by appls_simple/ -IHV -HV -HVs
+@csx_appl_simple_tstc /2 width=1 by applv_simple/ -IHV -HV -HVs
 #X #H #H0
 lapply (cpxs_fwd_cnx_vector … H) -H // -H1T -H2T #H
 elim (H0) -H0 //
 qed.
 
-lemma csx_appls_sort: ∀h,g,G,L,k,Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] Vs → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.⋆k.
+lemma csx_applv_sort: ∀h,g,G,L,k,Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] Vs → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.⋆k.
 #h #g #G #L #k elim (deg_total h g k)
-#l generalize in match k; -k @(nat_ind_plus … l) -l [ /3 width=6 by csx_appls_cnx, cnx_sort, simple_atom/ ]
+#l generalize in match k; -k @(nat_ind_plus … l) -l [ /3 width=6 by csx_applv_cnx, cnx_sort, simple_atom/ ]
 #l #IHl #k #Hkl lapply (deg_next_SO … Hkl) -Hkl
 #Hkl #Vs elim Vs -Vs /2 width=1 by/
 #V #Vs #IHVs #HVVs
 elim (csxv_inv_cons … HVVs) #HV #HVs
-@csx_appl_simple_tstc /2 width=1 by appls_simple, simple_atom/ -IHVs -HV -HVs
+@csx_appl_simple_tstc /2 width=1 by applv_simple, simple_atom/ -IHVs -HV -HVs
 #X #H #H0
 elim (cpxs_fwd_sort_vector … H) -H #H
 [ elim H0 -H0 //
@@ -48,14 +48,14 @@ elim (cpxs_fwd_sort_vector … H) -H #H
 ]
 qed.
 
-(* Basic_1: was just: sn3_appls_beta *)
-lemma csx_appls_beta: ∀h,g,a,G,L,Vs,V,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.ⓓ{a}ⓝW.V.T →
+(* Basic_1: was just: sn3_applv_beta *)
+lemma csx_applv_beta: ∀h,g,a,G,L,Vs,V,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.ⓓ{a}ⓝW.V.T →
                       ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs. ⓐV.ⓛ{a}W.T.
 #h #g #a #G #L #Vs elim Vs -Vs /2 width=1 by csx_appl_beta/
 #V0 #Vs #IHV #V #W #T #H1T
 lapply (csx_fwd_pair_sn … H1T) #HV0
 lapply (csx_fwd_flat_dx … H1T) #H2T
-@csx_appl_simple_tstc /2 width=1 by appls_simple, simple_flat/ -IHV -HV0 -H2T
+@csx_appl_simple_tstc /2 width=1 by applv_simple, simple_flat/ -IHV -HV0 -H2T
 #X #H #H0
 elim (cpxs_fwd_beta_vector … H) -H #H
 [ -H1T elim H0 -H0 //
@@ -63,7 +63,7 @@ elim (cpxs_fwd_beta_vector … H) -H #H
 ]
 qed.
 
-lemma csx_appls_delta: ∀h,g,I,G,L,K,V1,i. ⇩[i] L ≡ K.ⓑ{I}V1 →
+lemma csx_applv_delta: ∀h,g,I,G,L,K,V1,i. ⇩[i] L ≡ K.ⓑ{I}V1 →
                        ∀V2. ⇧[0, i + 1] V1 ≡ V2 →
                        ∀Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] (ⒶVs.V2) → ⦃G, L⦄ ⊢ ⬊*[h, g] (ⒶVs.#i).
 #h #g #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs
@@ -71,7 +71,7 @@ lemma csx_appls_delta: ∀h,g,I,G,L,K,V1,i. ⇩[i] L ≡ K.ⓑ{I}V1 →
 | #V #Vs #IHV #H1T
   lapply (csx_fwd_pair_sn … H1T) #HV
   lapply (csx_fwd_flat_dx … H1T) #H2T
-  @csx_appl_simple_tstc /2 width=1 by appls_simple, simple_atom/ -IHV -HV  -H2T
+  @csx_appl_simple_tstc /2 width=1 by applv_simple, simple_atom/ -IHV -HV  -H2T
   #X #H #H0
   elim (cpxs_fwd_delta_vector … HLK … HV12 … H) -HLK -HV12 -H #H
   [ -H1T elim H0 -H0 //
@@ -80,8 +80,8 @@ lemma csx_appls_delta: ∀h,g,I,G,L,K,V1,i. ⇩[i] L ≡ K.ⓑ{I}V1 →
 ]
 qed.
 
-(* Basic_1: was just: sn3_appls_abbr *)
-lemma csx_appls_theta: ∀h,g,a,G,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
+(* Basic_1: was just: sn3_applv_abbr *)
+lemma csx_applv_theta: ∀h,g,a,G,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
                        ∀V,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}V.ⒶV2s.T →
                        ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶV1s.ⓓ{a}V.T.
 #h #g #a #G #L #V1s #V2s * -V1s -V2s /2 width=1 by/
@@ -99,15 +99,15 @@ elim (cpxs_fwd_theta_vector … (V2@V2s) … H1) -H1 /2 width=1 by liftv_cons/ -
 ]
 qed.
 
-(* Basic_1: was just: sn3_appls_cast *)
-lemma csx_appls_cast: ∀h,g,G,L,Vs,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.W → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.T →
+(* Basic_1: was just: sn3_applv_cast *)
+lemma csx_applv_cast: ∀h,g,G,L,Vs,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.W → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.T →
                       ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.ⓝW.T.
 #h #g #G #L #Vs elim Vs -Vs /2 width=1 by csx_cast/
 #V #Vs #IHV #W #T #H1W #H1T
 lapply (csx_fwd_pair_sn … H1W) #HV
 lapply (csx_fwd_flat_dx … H1W) #H2W
 lapply (csx_fwd_flat_dx … H1T) #H2T
-@csx_appl_simple_tstc /2 width=1 by appls_simple, simple_flat/ -IHV -HV -H2W -H2T
+@csx_appl_simple_tstc /2 width=1 by applv_simple, simple_flat/ -IHV -HV -H2W -H2T
 #X #H #H0
 elim (cpxs_fwd_cast_vector … H) -H #H
 [ -H1W -H1T elim H0 -H0 //
@@ -119,11 +119,11 @@ qed.
 theorem csx_acr: ∀h,g. acr (cpx h g) (eq …) (csx h g) (λG,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T).
 #h #g @mk_acr //
 [ /2 width=8 by csx_lift/
-| /3 width=1 by csx_appls_cnx/
-|3,4,7: /2 width=1 by csx_appls_beta, csx_appls_sort, csx_appls_cast/
-| /2 width=7 by csx_appls_delta/
+| /3 width=1 by csx_applv_cnx/
+|3,4,7: /2 width=1 by csx_applv_beta, csx_applv_sort, csx_applv_cast/
+| /2 width=7 by csx_applv_delta/
 | #G #L #V1s #V2s #HV12s #a #V #T #H #HV
-  @(csx_appls_theta … HV12s) -HV12s
+  @(csx_applv_theta … HV12s) -HV12s
   @csx_abbr //
 ]
 qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_vector.ma
index bd23ff8b6..733666659 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_vector.ma
@@ -32,7 +32,7 @@ normalize // qed-.
 
 (* Basic forward lemmas *****************************************************)
 
-lemma csx_fwd_appls: ∀h,g,G,L,T,Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] Ⓐ Vs.T →
+lemma csx_fwd_applv: ∀h,g,G,L,T,Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] Ⓐ Vs.T →
                      ⦃G, L⦄ ⊢ ⬊*[h, g] Vs ∧ ⦃G, L⦄ ⊢ ⬊*[h, g] T.
 #h #g #G #L #T #Vs elim Vs -Vs /2 width=1/
 #V #Vs #IHVs #HVs
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/scpds.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/scpds.ma
new file mode 100644
index 000000000..29a942fec
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/scpds.ma
@@ -0,0 +1,58 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/notation/relations/dpredstar_7.ma".
+include "basic_2/static/da.ma".
+include "basic_2/unfold/lstas.ma".
+include "basic_2/computation/cprs.ma".
+
+(* STRATIFIED DECOMPOSED PARALLEL COMPUTATION ON TERMS **********************)
+
+definition scpds: ∀h. sd h → nat → relation4 genv lenv term term ≝
+                  λh,g,l2,G,L,T1,T2.
+                  ∃∃T,l1. l2 ≤ l1 & ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 & ⦃G, L⦄ ⊢ T1 •*[h, l2] T & ⦃G, L⦄ ⊢ T ➡* T2.
+
+interpretation "stratified decomposed parallel computation (term)"
+   'DPRedStar h g l G L T1 T2 = (scpds h g l G L T1 T2).
+
+(* Basic properties *********************************************************)
+
+lemma sta_cprs_scpds: ∀h,g,G,L,T1,T,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T1 •[h] T →
+                      ⦃G, L⦄ ⊢ T ➡* T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g, 1] T2.
+/3 width=6 by sta_lstas, ex4_2_intro/ qed.
+
+lemma lstas_scpds: ∀h,g,G,L,T1,T2,l1. ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 →
+                   ∀l2. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 •*[h, l2] T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l2] T2.
+/2 width=6 by ex4_2_intro/ qed.
+
+lemma cprs_scpds: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l → ⦃G, L⦄ ⊢ T1 ➡* T2 →
+                  ⦃G, L⦄ ⊢ T1 •*➡*[h, g, 0] T2.
+/2 width=6 by lstar_O, ex4_2_intro/ qed.
+
+lemma scpds_refl: ∀h,g,G,L,T,l. ⦃G, L⦄ ⊢ T ▪[h, g] l → ⦃G, L⦄ ⊢ T •*➡*[h, g, 0] T.
+/2 width=2 by cprs_scpds/ qed.
+
+lemma scpds_strap1: ∀h,g,G,L,T1,T,T2,l.
+                    ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l] T → ⦃G, L⦄ ⊢ T ➡ T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l] T2.
+#h #g #G #L #T1 #T #T2 #l * /3 width=8 by cprs_strap1, ex4_2_intro/
+qed.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma scpds_fwd_cprs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 •*➡*[h, g, 0] T2 →
+                      ⦃G, L⦄ ⊢ T1 ➡* T2.
+#h #g #G #L #T1 #T2 *
+#T #l #_ #_ #H lapply (lstas_inv_O … H) -l -H
+#H destruct //
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/scpds_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/scpds_aaa.ma
new file mode 100644
index 000000000..ad534204f
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/scpds_aaa.ma
@@ -0,0 +1,25 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/unfold/lstas_aaa.ma".
+include "basic_2/computation/cpxs_aaa.ma".
+include "basic_2/computation/scpds.ma".
+
+(* STRATIFIED DECOMPOSED PARALLEL COMPUTATION ON TERMS **********************)
+
+(* Properties on atomic arity assignment for terms **************************)
+
+lemma scpds_aaa_conf: ∀h,g,G,L,l. Conf3 … (aaa G L) (scpds h g l G L).
+#h #g #G #L #l #A #T #HT #U * /3 width=6 by lstas_aaa_conf, cprs_aaa_conf/
+qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/scpds_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/scpds_lift.ma
new file mode 100644
index 000000000..794e5c60e
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/scpds_lift.ma
@@ -0,0 +1,36 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/static/da_lift.ma".
+include "basic_2/unfold/lstas_lift.ma".
+include "basic_2/computation/cprs_lift.ma".
+include "basic_2/computation/scpds.ma".
+
+(* STRATIFIED DECOMPOSED PARALLEL COMPUTATION ON TERMS **********************)
+
+(* Relocation properties ****************************************************)
+
+lemma scpds_lift: ∀h,g,G,l. l_liftable (scpds h g l G).
+#h #g #G #l2 #K #T1 #T2 * #T #l1 #Hl21 #Hl1 #HT1 #HT2 #L #s #d #e
+elim (lift_total T d e)
+/3 width=15 by cprs_lift, da_lift, lstas_lift, ex4_2_intro/
+qed.
+
+lemma scpds_inv_lift1: ∀h,g,G,l. l_deliftable_sn (scpds h g l G).
+#h #g #G #l2 #L #U1 #U2 * #U #l1 #Hl21 #Hl1 #HU1 #HU2 #K #s #d #e #HLK #T1 #HTU1
+lapply (da_inv_lift … Hl1 … HLK … HTU1) -Hl1 #Hl1
+elim (lstas_inv_lift1 … HU1 … HLK … HTU1) -U1 #T #HTU #HT1
+elim (cprs_inv_lift1 … HU2 … HLK … HTU) -U -L
+/3 width=8 by ex4_2_intro, ex2_intro/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/scpds_scpds.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/scpds_scpds.ma
new file mode 100644
index 000000000..1acbf9398
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/scpds_scpds.ma
@@ -0,0 +1,92 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/unfold/lstas_lstas.ma".
+include "basic_2/computation/lprs_cprs.ma".
+include "basic_2/computation/cpxs_cpxs.ma".
+include "basic_2/computation/scpds.ma".
+
+(* STRATIFIED DECOMPOSED PARALLEL COMPUTATION ON TERMS **********************)
+
+(* Advanced properties ******************************************************)
+
+lemma scpds_strap2: ∀h,g,G,L,T1,T,T2,l1,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l1+1 →
+                    ⦃G, L⦄ ⊢ T1 •[h] T → ⦃G, L⦄ ⊢ T •*➡*[h, g, l] T2 →
+                    ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l+1] T2.
+#h #g #G #L #T1 #T #T2 #l1 #l #Hl1 #HT1 *
+#T0 #l0 #Hl0 #HTl0 #HT0 #HT02
+lapply (da_sta_conf … HT1 … Hl1) <minus_plus_m_m #HTl1
+lapply (da_mono … HTl0 … HTl1) -HTl0 -HTl1 #H destruct
+/3 width=6 by lstas_step_sn, le_S_S, ex4_2_intro/
+qed.
+
+lemma scpds_cprs_trans: ∀h,g,G,L,T1,T,T2,l.
+                        ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l] T → ⦃G, L⦄ ⊢ T ➡* T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l] T2.
+#h #g #G #L #T1 #T #T2 #l * /3 width=8 by cprs_trans, ex4_2_intro/
+qed-.
+
+lemma lstas_scpds_trans: ∀h,g,G,L,T1,T,T2,l1,l2,l.
+                         l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 →
+                         ⦃G, L⦄ ⊢ T1 •*[h, l2] T → ⦃G, L⦄ ⊢ T •*➡*[h, g, l] T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l2+l] T2.
+#h #g #G #L #T1 #T #T2 #l1 #l2 #l #Hl21 #HTl1 #HT1 * #T0 #l0 #Hl0 #HTl0 #HT0 #HT02
+lapply (lstas_da_conf … HT1 … HTl1) #HTl12
+lapply (da_mono … HTl12 … HTl0) -HTl12 -HTl0 #H destruct
+lapply (le_minus_to_plus_r … Hl21 Hl0) -Hl21 -Hl0
+/3 width=7 by lstas_trans, ex4_2_intro/
+qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma scpds_inv_abst1: ∀h,g,a,G,L,V1,T1,U2,l. ⦃G, L⦄ ⊢ ⓛ{a}V1.T1 •*➡*[h, g, l] U2 →
+                       ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡* V2 & ⦃G, L.ⓛV1⦄ ⊢ T1 •*➡*[h, g, l] T2 &
+                                U2 = ⓛ{a}V2.T2.
+#h #g #a #G #L #V1 #T1 #U2 #l2 * #X #l1 #Hl21 #Hl1 #H1 #H2
+lapply (da_inv_bind … Hl1) -Hl1 #Hl1
+elim (lstas_inv_bind1 … H1) -H1 #U #HTU1 #H destruct
+elim (cprs_inv_abst1 … H2) -H2 #V2 #T2 #HV12 #HUT2 #H destruct
+/3 width=6 by ex4_2_intro, ex3_2_intro/
+qed-.
+
+lemma scpds_inv_abbr_abst: ∀h,g,a1,a2,G,L,V1,W2,T1,T2,l. ⦃G, L⦄ ⊢ ⓓ{a1}V1.T1 •*➡*[h, g, l] ⓛ{a2}W2.T2 →
+                           ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 •*➡*[h, g, l] T & ⇧[0, 1] ⓛ{a2}W2.T2 ≡ T & a1 = true.
+#h #g #a1 #a2 #G #L #V1 #W2 #T1 #T2 #l2 * #X #l1 #Hl21 #Hl1 #H1 #H2
+lapply (da_inv_bind … Hl1) -Hl1 #Hl1
+elim (lstas_inv_bind1 … H1) -H1 #U1 #HTU1 #H destruct
+elim (cprs_inv_abbr1 … H2) -H2 *
+[ #V2 #U2 #HV12 #HU12 #H destruct
+| /3 width=6 by ex4_2_intro, ex3_intro/
+]
+qed-.
+
+lemma scpds_inv_lstas_eq: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l] T2 →
+                          ∀T. ⦃G, L⦄ ⊢ T1 •*[h, l] T → ⦃G, L⦄ ⊢ T ➡* T2.
+#h #g #G #L #T1 #T2 #l2 *
+#T0 #l1 #_ #_ #HT10 #HT02 #T #HT1
+lapply (lstas_mono … HT10 … HT1) #H destruct //
+qed-.
+
+(* Advanced forward lemmas **************************************************)
+
+lemma scpds_fwd_cpxs: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l] T2 → ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2.
+#h #g #G #L #T1 #T2 #l * /3 width=5 by cpxs_trans, lstas_cpxs, cprs_cpxs/
+qed-.
+
+(* Main properties **********************************************************)
+
+theorem scpds_conf_eq: ∀h,g,G,L,T0,T1,l. ⦃G, L⦄ ⊢ T0 •*➡*[h, g, l] T1 →
+                       ∀T2. ⦃G, L⦄ ⊢ T0 •*➡*[h, g, l] T2 →
+                       ∃∃T. ⦃G, L⦄ ⊢ T1 ➡* T & ⦃G, L⦄ ⊢ T2 ➡* T.
+#h #g #G #L #T0 #T1 #l0 * #U1 #l1 #_ #_ #H1 #HUT1 #T2 * #U2 #l2 #_ #_ #H2 #HUT2 -l1 -l2
+lapply (lstas_mono … H1 … H2) #H destruct -h -l0 /2 width=3 by cprs_conf/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/hsnv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/hsnv.ma
deleted file mode 100644
index 03ab123bd..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/hsnv.ma
+++ /dev/null
@@ -1,48 +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/notation/relations/nativevalid_6.ma".
-include "basic_2/equivalence/cpes.ma".
-include "basic_2/dynamic/snv.ma".
-
-(* HIGHER ORDER STRATIFIED NATIVE VALIDITY FOR TERMS ************************)
-
-inductive hsnv (h) (g) (l1) (G) (L): predicate term ≝
-| hsnv_cast: ∀U,T. ⦃G, L⦄ ⊢ U ¡[h, g] → ⦃G, L⦄ ⊢ T ¡[h, g] →
-             (∀l2. l2 ≤ l1 → ⦃G, L⦄ ⊢ U •*⬌*[h, g, l2, l2+1] T) →
-             hsnv h g l1 G L (ⓝU.T)
-.
-
-interpretation "higher order stratified native validity (term)"
-   'NativeValid h g l G L T = (hsnv h g l G L T).
-
-(* Basic inversion lemmas ***************************************************)
-
-fact hsnv_inv_cast_aux: ∀h,g,G,L,X,l1. ⦃G, L⦄ ⊢ X ¡[h, g, l1] → ∀U,T. X = ⓝU.T →
-                        ∧∧ ⦃G, L⦄ ⊢ U ¡[h, g] & ⦃G, L⦄ ⊢ T ¡[h, g]
-                         & (∀l2. l2 ≤ l1 → ⦃G, L⦄ ⊢ U •*⬌*[h, g, l2, l2+1] T).
-#h #g #G #L #X #l1 * -X
-#U #T #HU #HT #HUT #U1 #T1 #H destruct /3 width=1 by and3_intro/
-qed-.
-
-lemma hsnv_inv_cast: ∀h,g,G,L,U,T,l1. ⦃G, L⦄ ⊢ ⓝU.T ¡[h, g, l1] →
-                     ∧∧ ⦃G, L⦄ ⊢ U ¡[h, g] & ⦃G, L⦄ ⊢ T ¡[h, g]
-                      & (∀l2. l2 ≤ l1 → ⦃G, L⦄ ⊢ U •*⬌*[h, g, l2, l2+1] T).
-/2 width=3 by hsnv_inv_cast_aux/ qed-.
-
-lemma hsnv_inv_snv: ∀h,g,G,L,T,l. ⦃G, L⦄ ⊢ T ¡[h, g, l] → ⦃G, L⦄ ⊢ T ¡[h, g].
-#h #g #G #L #T #l * -T
-#U #T #HU #HT #HUT elim (HUT 0) -HUT
-/3 width=3 by snv_cast, cpds_fwd_cprs/
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/hsnv_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/hsnv_aaa.ma
deleted file mode 100644
index c59393178..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/hsnv_aaa.ma
+++ /dev/null
@@ -1,27 +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/dynamic/snv_aaa.ma".
-include "basic_2/dynamic/hsnv.ma".
-
-(* HIGHER ORDER STRATIFIED NATIVE VALIDITY FOR TERMS ************************)
-
-(* Advanced properties ******************************************************)
-
-lemma snv_hsnv_cast: ∀h,g,G,L,U,T. ⦃G, L⦄ ⊢ ⓝU.T ¡[h, g] → ⦃G, L⦄ ⊢ ⓝU.T ¡[h, g, 0].
-#h #g #G #L #U #T #H elim (snv_inv_cast … H) -H
-#U0 #HU #HT #HU0 #HTU0 @hsnv_cast // -HT
-#l #H <(le_n_O_to_eq … H) -l
-elim (snv_fwd_da … HU) -HU /3 width=3 by cprs_cpds, cpds_div/
-qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma
index bb8b00742..c16f87bb0 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/notation/relations/lrsubeqv_5.ma".
-include "basic_2/dynamic/hsnv.ma".
+include "basic_2/dynamic/shnv.ma".
 
 (* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpds.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpds.ma
deleted file mode 100644
index 857c14b0c..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpds.ma
+++ /dev/null
@@ -1,30 +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/dynamic/lsubsv_lstas.ma".
-
-(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
-
-(* Properties on decomposed extended parallel computation on terms **********)
-
-lemma lsubsv_cpds_trans: ∀h,g,G,L2,T1,T2,l. ⦃G, L2⦄ ⊢ T1 •*➡*[h, g, l] T2 →
-                         ∀L1. G ⊢ L1 ⫃¡[h, g] L2 →
-                         ∃∃T. ⦃G, L1⦄ ⊢ T1 •*➡*[h, g, l] T & ⦃G, L1⦄ ⊢ T2 ➡* T.
-#h #g #G #L2 #T1 #T2 #l2 * #T #l1 #Hl21 #Hl1 #HT1 #HT2 #L1 #HL12
-lapply (lsubsv_cprs_trans … HL12 … HT2) -HT2 #HT2
-elim (lsubsv_lstas_trans … HT1 … Hl1 … HL12) // #T0 #HT10 #HT0
-lapply (cpcs_cprs_strap1 … HT0 … HT2) -T #HT02
-elim (cpcs_inv_cprs … HT02) -HT02
-/5 width=5 by lsubsv_fwd_lsubd, lsubd_da_trans, ex4_2_intro, ex2_intro/
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lstas.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lstas.ma
index 37aa2a845..5600eeaba 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lstas.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lstas.ma
@@ -14,7 +14,7 @@
 
 include "basic_2/static/lsubd_da.ma".
 include "basic_2/unfold/lstas_alt.ma".
-include "basic_2/equivalence/cpes_cpcs.ma".
+include "basic_2/equivalence/scpes_cpcs.ma".
 include "basic_2/dynamic/lsubsv_lsubd.ma".
 
 (* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
@@ -55,12 +55,12 @@ lemma lsubsv_lstas_trans: ∀h,g,G,L2,T,U2,l2. ⦃G, L2⦄ ⊢ T •*[h, l2] U2
     /3 width=12 by lstas_ldec, cpcs_lift, ex2_intro/
   | #V #l1 #HXV #_ #HV #HX #HK12 #_ #H destruct
     lapply (da_mono … HV0 … HX) -HX #H destruct
-    elim (hsnv_inv_cast … HXV) -HXV #_ #_ #H
+    elim (shnv_inv_cast … HXV) -HXV #_ #_ #H
     lapply (H … Hl21) -H #HXV
     elim (IHXY … Hl21 HV0 … HK12) -K2 -Hl21 #Y0 #HXY0 #HY0
     elim (da_inv_sta … HV) -HV #W #HVW
     elim (lstas_total … HVW (l2+1)) -W #W #HVW
-    lapply (cpes_inv_lstas_eq … HXV … HXY0 … HVW) -HXV -HXY0 #HY0W
+    lapply (scpes_inv_lstas_eq … HXV … HXY0 … HVW) -HXV -HXY0 #HY0W
     lapply (cpcs_canc_sn … HY0W … HY0) -Y0 #HYW
     elim (lift_total W 0 (i+1))
     lapply (drop_fwd_drop2 … HLK1)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsuba.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsuba.ma
index f9b2161df..54be766bc 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsuba.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsuba.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/equivalence/cpes_aaa.ma".
+include "basic_2/equivalence/scpes_aaa.ma".
 include "basic_2/dynamic/snv_aaa.ma".
 include "basic_2/dynamic/lsubsv.ma".
 
@@ -23,10 +23,10 @@ include "basic_2/dynamic/lsubsv.ma".
 lemma lsubsv_fwd_lsuba: ∀h,g,G,L1,L2. G ⊢ L1 ⫃¡[h, g] L2 → G ⊢ L1 ⫃⁝ L2.
 #h #g #G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsuba_pair/
 #L1 #L2 #W #V #l1 #H #_ #_ #_ #_ #IHL12
-elim (hsnv_inv_cast … H) -H #HW #HV #H
+elim (shnv_inv_cast … H) -H #HW #HV #H
 lapply (H 0 ?) // -l1 #HWV
 elim (snv_fwd_aaa … HW) -HW #B #HW
 elim (snv_fwd_aaa … HV) -HV #A #HV
-lapply (cpes_aaa_mono … HWV … HW … HV) #H destruct
+lapply (scpes_aaa_mono … HWV … HW … HV) #H destruct
 /4 width=5 by lsuba_aaa_conf, lsuba_beta, aaa_cast/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_scpds.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_scpds.ma
new file mode 100644
index 000000000..3edc47f41
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_scpds.ma
@@ -0,0 +1,30 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/dynamic/lsubsv_lstas.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
+
+(* Properties on decomposed extended parallel computation on terms **********)
+
+lemma lsubsv_scpds_trans: ∀h,g,G,L2,T1,T2,l. ⦃G, L2⦄ ⊢ T1 •*➡*[h, g, l] T2 →
+                          ∀L1. G ⊢ L1 ⫃¡[h, g] L2 →
+                          ∃∃T. ⦃G, L1⦄ ⊢ T1 •*➡*[h, g, l] T & ⦃G, L1⦄ ⊢ T2 ➡* T.
+#h #g #G #L2 #T1 #T2 #l2 * #T #l1 #Hl21 #Hl1 #HT1 #HT2 #L1 #HL12
+lapply (lsubsv_cprs_trans … HL12 … HT2) -HT2 #HT2
+elim (lsubsv_lstas_trans … HT1 … Hl1 … HL12) // #T0 #HT10 #HT0
+lapply (cpcs_cprs_strap1 … HT0 … HT2) -T #HT02
+elim (cpcs_inv_cprs … HT02) -HT02
+/5 width=5 by lsubsv_fwd_lsubd, lsubd_da_trans, ex4_2_intro, ex2_intro/
+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 2d9f6d5ff..a3f39fbf7 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/dynamic/lsubsv_cpds.ma".
+include "basic_2/dynamic/lsubsv_scpds.ma".
 
 (* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
 
@@ -26,18 +26,18 @@ lemma lsubsv_snv_trans: ∀h,g,G,L2,T. ⦃G, L2⦄ ⊢ T ¡[h, g] →
   elim (lsubsv_inv_pair2 … H) -H * #K1
   [ #HK12 #H destruct /3 width=5 by snv_lref/
   | #W #l #HVW #_ #_ #_ #_ #H1 #H2 destruct -IHV
-    /3 width=6 by hsnv_inv_snv, snv_lref/
+    /3 width=6 by shnv_inv_snv, snv_lref/
   ]
 | #a #I #G #L2 #V #T #_ #_ #IHV #IHT #L1 #HL12 destruct
   /4 width=1 by snv_bind, lsubsv_pair/
 | #a #G #L2 #V #W0 #T #U0 #l #_ #_ #HVW0 #HTU0 #IHV #IHT #L1 #HL12
-  elim (lsubsv_cpds_trans … HVW0 … HL12) -HVW0 #V0 #HV0 #HWV0
-  elim (lsubsv_cpds_trans … HTU0 … HL12) -HTU0 #X #HT0 #H
+  elim (lsubsv_scpds_trans … HVW0 … HL12) -HVW0 #V0 #HV0 #HWV0
+  elim (lsubsv_scpds_trans … HTU0 … HL12) -HTU0 #X #HT0 #H
   elim (cprs_inv_abst1 … H) -H #W #T0 #HW0 #_ #H destruct
   elim (cprs_conf … HWV0 … HW0) -W0
-  /4 width=10 by snv_appl, cpds_cprs_trans, cprs_bind/
+  /4 width=10 by snv_appl, scpds_cprs_trans, cprs_bind/
 | #G #L2 #U #T #U0 #_ #_ #HU0 #HTU0 #IHU #IHT #L1 #HL12
-  elim (lsubsv_cpds_trans … HTU0 … HL12) -HTU0
+  elim (lsubsv_scpds_trans … HTU0 … HL12) -HTU0
   /4 width=5 by lsubsv_cprs_trans, snv_cast, cprs_trans/
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/shnv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/shnv.ma
new file mode 100644
index 000000000..1cca09856
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/shnv.ma
@@ -0,0 +1,48 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/notation/relations/nativevalid_6.ma".
+include "basic_2/equivalence/scpes.ma".
+include "basic_2/dynamic/snv.ma".
+
+(* STRATIFIED HIGHER NATIVE VALIDITY FOR TERMS ******************************)
+
+inductive shnv (h) (g) (l1) (G) (L): predicate term ≝
+| shnv_cast: ∀U,T. ⦃G, L⦄ ⊢ U ¡[h, g] → ⦃G, L⦄ ⊢ T ¡[h, g] →
+             (∀l2. l2 ≤ l1 → ⦃G, L⦄ ⊢ U •*⬌*[h, g, l2, l2+1] T) →
+             shnv h g l1 G L (ⓝU.T)
+.
+
+interpretation "stratified higher native validity (term)"
+   'NativeValid h g l G L T = (shnv h g l G L T).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact shnv_inv_cast_aux: ∀h,g,G,L,X,l1. ⦃G, L⦄ ⊢ X ¡[h, g, l1] → ∀U,T. X = ⓝU.T →
+                        ∧∧ ⦃G, L⦄ ⊢ U ¡[h, g] & ⦃G, L⦄ ⊢ T ¡[h, g]
+                         & (∀l2. l2 ≤ l1 → ⦃G, L⦄ ⊢ U •*⬌*[h, g, l2, l2+1] T).
+#h #g #G #L #X #l1 * -X
+#U #T #HU #HT #HUT #U1 #T1 #H destruct /3 width=1 by and3_intro/
+qed-.
+
+lemma shnv_inv_cast: ∀h,g,G,L,U,T,l1. ⦃G, L⦄ ⊢ ⓝU.T ¡[h, g, l1] →
+                     ∧∧ ⦃G, L⦄ ⊢ U ¡[h, g] & ⦃G, L⦄ ⊢ T ¡[h, g]
+                      & (∀l2. l2 ≤ l1 → ⦃G, L⦄ ⊢ U •*⬌*[h, g, l2, l2+1] T).
+/2 width=3 by shnv_inv_cast_aux/ qed-.
+
+lemma shnv_inv_snv: ∀h,g,G,L,T,l. ⦃G, L⦄ ⊢ T ¡[h, g, l] → ⦃G, L⦄ ⊢ T ¡[h, g].
+#h #g #G #L #T #l * -T
+#U #T #HU #HT #HUT elim (HUT 0) -HUT
+/3 width=3 by snv_cast, scpds_fwd_cprs/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/shnv_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/shnv_aaa.ma
new file mode 100644
index 000000000..d928f6287
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/shnv_aaa.ma
@@ -0,0 +1,27 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/dynamic/snv_aaa.ma".
+include "basic_2/dynamic/shnv.ma".
+
+(* STRATIFIED HIGHER NATIVE VALIDITY FOR TERMS ******************************)
+
+(* Advanced properties ******************************************************)
+
+lemma snv_shnv_cast: ∀h,g,G,L,U,T. ⦃G, L⦄ ⊢ ⓝU.T ¡[h, g] → ⦃G, L⦄ ⊢ ⓝU.T ¡[h, g, 0].
+#h #g #G #L #U #T #H elim (snv_inv_cast … H) -H
+#U0 #HU #HT #HU0 #HTU0 @shnv_cast // -HT
+#l #H <(le_n_O_to_eq … H) -l
+elim (snv_fwd_da … HU) -HU /3 width=3 by cprs_scpds, scpds_div/
+qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma
index 51cf1d2d2..d58e5ac2a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/notation/relations/nativevalid_5.ma".
-include "basic_2/computation/cpds.ma".
+include "basic_2/computation/scpds.ma".
 
 (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma
index c289e2bbb..299070776 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma
@@ -15,7 +15,7 @@
 include "basic_2/static/da_aaa.ma".
 include "basic_2/unfold/lstas_lift.ma".
 include "basic_2/computation/csx_aaa.ma".
-include "basic_2/computation/cpds_aaa.ma".
+include "basic_2/computation/scpds_aaa.ma".
 include "basic_2/dynamic/snv.ma".
 
 (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
@@ -28,13 +28,13 @@ lemma snv_fwd_aaa: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → ∃A. ⦃G, L⦄
 | #I #G #L #K #V #i #HLK #_ * /3 width=6 by aaa_lref, ex_intro/
 | #a * #G #L #V #T #_ #_ * #B #HV * #A #HA /3 width=2 by aaa_abbr, aaa_abst, ex_intro/
 | #a #G #L #V #W0 #T #U0 #l #_ #_ #HVW0 #HTU0 * #B #HV * #X #HT
-  lapply (cpds_aaa_conf … HV … HVW0) -HVW0 #HW0
-  lapply (cpds_aaa_conf … HT … HTU0) -HTU0 #H
+  lapply (scpds_aaa_conf … HV … HVW0) -HVW0 #HW0
+  lapply (scpds_aaa_conf … HT … HTU0) -HTU0 #H
   elim (aaa_inv_abst … H) -H #B0 #A #H1 #HU #H2 destruct
   lapply (aaa_mono … H1 … HW0) -W0 #H destruct /3 width=4 by aaa_appl, ex_intro/
 | #G #L #U #T #U0 #_ #_ #HU0 #HTU0 * #B #HU * #A #HT
   lapply (cprs_aaa_conf … HU … HU0) -HU0 #HU0
-  lapply (cpds_aaa_conf … HT … HTU0) -HTU0 #H
+  lapply (scpds_aaa_conf … HT … HTU0) -HTU0 #H
   lapply (aaa_mono … H … HU0) -U0 #H destruct /3 width=3 by aaa_cast, ex_intro/
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpes.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpes.ma
deleted file mode 100644
index 6db1060e3..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpes.ma
+++ /dev/null
@@ -1,199 +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/fpbs_lift.ma".
-include "basic_2/computation/fpbg_fleq.ma".
-include "basic_2/equivalence/cpes_cpcs.ma".
-include "basic_2/equivalence/cpes_cpes.ma".
-include "basic_2/dynamic/snv.ma".
-
-(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
-
-(* Inductive premises for the preservation results **************************)
-
-definition IH_snv_cpr_lpr: ∀h:sh. sd h → relation3 genv lenv term ≝
-                           λh,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
-                           ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, g].
-
-definition IH_da_cpr_lpr: ∀h:sh. sd h → relation3 genv lenv term ≝
-                          λh,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
-                          ∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l →
-                          ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
-                          ⦃G, L2⦄ ⊢ T2 ▪[h, g] l.
-
-definition IH_lstas_cpr_lpr: ∀h:sh. sd h → relation3 genv lenv term ≝
-                             λh,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
-                             ∀l1,l2. l2 ≤ l1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 →
-                             ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, l2] U1 →
-                             ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
-                             ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, l2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2.
-
-definition IH_snv_lstas: ∀h:sh. sd h → relation3 genv lenv term ≝
-                         λh,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] →
-                         ∀l1,l2. l2 ≤ l1 → ⦃G, L⦄ ⊢ T ▪[h, g] l1 →
-                         ∀U. ⦃G, L⦄ ⊢ T •*[h, l2] U → ⦃G, L⦄ ⊢ U ¡[h, g].
-
-(* Properties for the preservation results **********************************)
-
-fact snv_cprs_lpr_aux: ∀h,g,G0,L0,T0.
-                       (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
-                       ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
-                       ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, g].
-#h #g #G0 #L0 #T0 #IH #G #L1 #T1 #HLT0 #HT1 #T2 #H
-@(cprs_ind … H) -T2 /4 width=6 by fpbg_fpbs_trans, cprs_fpbs/
-qed-.
-
-fact da_cprs_lpr_aux: ∀h,g,G0,L0,T0.
-                      (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
-                      (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
-                      ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
-                      ∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l →
-                      ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ▪[h, g] l.
-#h #g #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #HLT0 #HT1 #l #Hl #T2 #H
-@(cprs_ind … H) -T2 /4 width=10 by snv_cprs_lpr_aux, fpbg_fpbs_trans, cprs_fpbs/
-qed-.
-
-fact da_cpds_lpr_aux: ∀h,g,G0,L0,T0.
-                      (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lstas h g G1 L1 T1) →
-                      (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
-                      (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
-                      ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
-                      ∀l1. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 →
-                      ∀T2,l2. ⦃G, L1⦄ ⊢ T1 •*➡*[h, g, l2] T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
-                      l2 ≤ l1 ∧ ⦃G, L2⦄ ⊢ T2 ▪[h, g] l1-l2.
-#h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L1 #T1 #HLT0 #HT1 #l1 #Hl1 #T2 #l2 * #T #l0 #Hl20 #H #HT1 #HT2 #L2 #HL12
-lapply (da_mono … H … Hl1) -H #H destruct
-lapply (lstas_da_conf … HT1 … Hl1) #Hl12
-lapply (da_cprs_lpr_aux … IH2 IH1 … Hl12 … HT2 … HL12) -IH2 -IH1 -HT2 -HL12
-/3 width=8 by fpbg_fpbs_trans, lstas_fpbs, conj/
-qed-.
-
-fact da_cpes_aux: ∀h,g,G0,L0,T0.
-                  (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lstas h g G1 L1 T1) →
-                  (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
-                  (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
-                  ∀G,L,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, g] →
-                  ∀T2. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T2⦄ → ⦃G, L⦄ ⊢ T2 ¡[h, g] →
-                  ∀l11. ⦃G, L⦄ ⊢ T1 ▪[h, g] l11 → ∀l12. ⦃G, L⦄ ⊢ T2 ▪[h, g] l12 →
-                  ∀l21,l22. ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l21, l22] T2 →
-                  ∧∧ l21 ≤ l11 & l22 ≤ l12 & l11 - l21 = l12 - l22.
-#h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L #T1 #HLT01 #HT1 #T2 #HLT02 #HT2 #l11 #Hl11 #l12 #Hl12 #l21 #l22 * #T #HT1 #HT2
-elim (da_cpds_lpr_aux … IH3 IH2 IH1 … Hl11 … HT1 … L) -Hl11 -HT1 //
-elim (da_cpds_lpr_aux … IH3 IH2 IH1 … Hl12 … HT2 … L) -Hl12 -HT2 //
-/3 width=7 by da_mono, and3_intro/
-qed-.
-
-fact lstas_cprs_lpr_aux: ∀h,g,G0,L0,T0.
-                         (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
-                         (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
-                         (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) →
-                         ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
-                         ∀l1,l2. l2 ≤ l1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 →
-                         ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, l2] U1 →
-                         ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
-                         ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, l2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2.
-#h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #l1 #l2 #Hl21 #Hl1 #U1 #HTU1 #T2 #H
-@(cprs_ind … H) -T2 [ /2 width=10 by/ ]
-#T #T2 #HT1T #HTT2 #IHT1 #L2 #HL12
-elim (IHT1 L1) // -IHT1 #U #HTU #HU1
-elim (IH1 … Hl21 … HTU … HTT2 … HL12) -IH1 -HTU -HTT2
-[2: /3 width=12 by da_cprs_lpr_aux/
-|3: /3 width=10 by snv_cprs_lpr_aux/
-|4: /3 width=5 by fpbg_fpbs_trans, cprs_fpbs/
-] -G0 -L0 -T0 -T1 -T -l1
-/4 width=5 by lpr_cpcs_conf, cpcs_trans, ex2_intro/
-qed-.
-
-fact cpds_cpr_lpr_aux: ∀h,g,G0,L0,T0.
-                       (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
-                       (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) →
-                       ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
-                       ∀U1,l. ⦃G, L1⦄ ⊢ T1 •*➡*[h, g, l] U1 →
-                       ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
-                       ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*➡*[h, g, l] U2 & ⦃G, L2⦄ ⊢ U1 ➡* U2.
-#h #g #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #U1 #l2 * #W1 #l1 #Hl21 #HTl1 #HTW1 #HWU1 #T2 #HT12 #L2 #HL12
-elim (IH1 … H01 … HTW1 … HT12 … HL12) -IH1 // #W2 #HTW2 #HW12
-lapply (IH2 … H01 … HTl1 … HT12 … HL12) -L0 -T0 // -T1
-lapply (lpr_cprs_conf … HL12 … HWU1) -L1 #HWU1
-lapply (cpcs_canc_sn … HW12 HWU1) -W1 #H
-elim (cpcs_inv_cprs … H) -H /3 width=6 by ex4_2_intro, ex2_intro/
-qed-.
-
-fact cpes_cpr_lpr_aux: ∀h,g,G0,L0,T0.
-                       (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
-                       (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) →
-                       ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
-                       ∀T2. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T2⦄ → ⦃G, L1⦄ ⊢ T2 ¡[h, g] →
-                       ∀l1,l2. ⦃G, L1⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2 →
-                       ∀U1. ⦃G, L1⦄ ⊢ T1 ➡ U1 → ∀U2. ⦃G, L1⦄ ⊢ T2 ➡ U2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
-                       ⦃G, L2⦄ ⊢ U1 •*⬌*[h, g, l1, l2] U2.
-#h #g #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #T2 #HT02 #HT2 #l1 #l2 * #T0 #HT10 #HT20 #U1 #HTU1 #U2 #HTU2 #L2 #HL12
-elim (cpds_cpr_lpr_aux … IH2 IH1 … HT10 … HTU1 … HL12) -HT10 -HTU1 // #X1 #HUX1 #H1
-elim (cpds_cpr_lpr_aux … IH2 IH1 … HT20 … HTU2 … HL12) -HT20 -HTU2 // #X2 #HUX2 #H2
-elim (cprs_conf … H1 … H2) -T0
-/3 width=5 by cpds_div, cpds_cprs_trans/
-qed-.
-
-fact lstas_cpds_aux: ∀h,g,G0,L0,T0.
-                     (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lstas h g G1 L1 T1) →
-                     (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
-                     (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
-                     (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) →
-                     ∀G,L,T. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T⦄ → ⦃G, L⦄ ⊢ T ¡[h, g] →
-                     ∀l,l1. l1 ≤ l → ⦃G, L⦄ ⊢ T ▪[h, g] l → ∀T1. ⦃G, L⦄ ⊢ T •*[h, l1] T1 →
-                     ∀T2,l2. ⦃G, L⦄ ⊢ T •*➡*[h, g, l2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l2-l1, l1-l2] T2.
-#h #g #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G #L #T #H0 #HT #l #l1 #Hl1 #HTl #T1 #HT1 #T2 #l2 * #X #l0 #Hl20 #H #HTX #HXT2
-lapply (da_mono … H … HTl) -H #H destruct
-lapply (lstas_da_conf … HT1 … HTl) #HTl1
-lapply (lstas_da_conf … HTX … HTl) #HXl
-lapply (da_cprs_lpr_aux … IH3 IH2 … HXl … HXT2 L ?)
-[1,2,3: /3 width=8 by fpbg_fpbs_trans, lstas_fpbs/ ] #HTl2
-elim (le_or_ge l1 l2) #Hl12 >(eq_minus_O … Hl12)
-[ /5 width=3 by cpds_refl, lstas_conf_le, monotonic_le_minus_l, ex4_2_intro, ex2_intro/
-| lapply (lstas_conf_le … HTX … HT1) // #HXT1 -HT1
-  elim (lstas_cprs_lpr_aux … IH3 IH2 IH1 … HXl … HXT1 … HXT2 L) -IH3 -IH2 -IH1 -HXl -HXT1 -HXT2
-  /3 width=8 by cpcs_cpes, fpbg_fpbs_trans, lstas_fpbs, monotonic_le_minus_l/
-]
-qed-.
-
-fact cpes_le_aux: ∀h,g,G0,L0,T0.
-                  (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lstas h g G1 L1 T1) →
-                  (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
-                  (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
-                  (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) →
-                  ∀G,L,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, g] →
-                  ∀T2. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T2⦄ → ⦃G, L⦄ ⊢ T2 ¡[h, g] →
-                  ∀l11. ⦃G, L⦄ ⊢ T1 ▪[h, g] l11 → ∀l12. ⦃G, L⦄ ⊢ T2 ▪[h, g] l12 →
-                  ∀l21,l22,l. l21 + l ≤ l11 → l22 + l ≤ l12 →
-                  ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l21, l22] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l21+l, l22+l] T2.
-#h #g #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G #L #T1 #H01 #HT1 #T2 #H02 #HT2 #l11 #Hl11 #Hl12 #Hl12 #l21 #l22 #l #H1 #H2 * #T0 #HT10 #HT20 
-elim (da_inv_sta … Hl11) #X1 #HTX1
-elim (lstas_total … HTX1 (l21+l)) -X1 #X1 #HTX1
-elim (da_inv_sta … Hl12) #X2 #HTX2
-elim (lstas_total … HTX2 (l22+l)) -X2 #X2 #HTX2
-lapply (lstas_cpds_aux … IH4 IH3 IH2 IH1 … Hl11 … HTX1 … HT10) -HT10
-[1,2,3: // | >eq_minus_O [2: // ] <minus_plus_m_m_commutative #HX1 ]
-lapply (lstas_cpds_aux … IH4 IH3 IH2 IH1 … Hl12 … HTX2 … HT20) -HT20
-[1,2,3: // | >eq_minus_O [2: // ] <minus_plus_m_m_commutative #HX2 ]
-lapply (lstas_cpes_trans … Hl11 … HTX1 … HX1) [ // ] -Hl11 -HTX1 -HX1 -H1 #H1
-lapply (lstas_cpes_trans … Hl12 … HTX2 … HX2) [ // ] -Hl12 -HTX2 -HX2 -H2 #H2
-lapply (cpes_canc_dx … H1 … H2) // (**) (* full auto raises NTypeChecker failure *)
-qed-.
-
-(* Advanced properties ******************************************************)
-
-lemma snv_cast_cpes: ∀h,g,G,L,U,T. ⦃G, L⦄ ⊢ U ¡[h, g] →  ⦃G, L⦄ ⊢ T ¡[h, g] →
-                     ⦃G, L⦄ ⊢ U •*⬌*[h, g, 0, 1] T → ⦃G, L⦄ ⊢ ⓝU.T ¡[h, g].
-#h #g #G #L #U #T #HU #HT * /3 width=3 by snv_cast, cpds_fwd_cprs/
-qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma
index d558b90c0..dac9cd153 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma
@@ -14,7 +14,7 @@
 
 include "basic_2/static/lsubd_da.ma".
 include "basic_2/dynamic/snv_aaa.ma".
-include "basic_2/dynamic/snv_cpes.ma".
+include "basic_2/dynamic/snv_scpes.ma".
 
 (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
 
@@ -66,11 +66,11 @@ fact da_cpr_lpr_aux: ∀h,g,G0,L0,T0.
   | #b #V2 #W #W2 #U #U2 #HV12 #HW2 #HU2 #H1 #H2 destruct
     elim (snv_inv_bind … HT1) -HT1 #HW #HU
     lapply (da_inv_bind … Hl) -Hl #Hl
-    elim (cpds_inv_abst1 … HTU1) -HTU1 #W3 #U3 #HW3 #_ #H destruct -U3 -l1
+    elim (scpds_inv_abst1 … HTU1) -HTU1 #W3 #U3 #HW3 #_ #H destruct -U3 -l1
     elim (snv_fwd_da … HV1) #l1 #Hl1
     elim (snv_fwd_da … HW) #l0 #Hl0
-    lapply (cpds_div … W … 0 … HVW1) /2 width=2 by cprs_cpds/ -W3 #H
-    elim (da_cpes_aux … IH3 IH2 IH1 … Hl0 … Hl1 … H) -IH3 -IH2 -H /2 width=1 by fqup_fpbg/ #_ #H1
+    lapply (scpds_div … W … 0 … HVW1) /2 width=2 by cprs_scpds/ -W3 #H
+    elim (da_scpes_aux … IH3 IH2 IH1 … Hl0 … Hl1 … H) -IH3 -IH2 -H /2 width=1 by fqup_fpbg/ #_ #H1
     <minus_n_O #H destruct >(plus_minus_m_m l1 1) in Hl1; // -H1 #Hl1
     lapply (IH1 … HV1 … Hl1 … HV12 … HL12) -HV1 -Hl1 -HV12 [ /2 by fqup_fpbg/ ]
     lapply (IH1 … Hl0 … HW2 … HL12) -Hl0 /2 width=1 by fqup_fpbg/ -HW
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma
index d8fb8d161..b0f1f88f4 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/multiple/fqus_alt.ma".
-include "basic_2/computation/cpds_lift.ma".
+include "basic_2/computation/scpds_lift.ma".
 include "basic_2/dynamic/snv.ma".
 
 (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
@@ -40,12 +40,12 @@ lemma snv_lift: ∀h,g,G,K,T. ⦃G, K⦄ ⊢ T ¡[h, g] → ∀L,s,d,e. ⇩[s, d
   elim (lift_inv_flat1 … H) -H #W #U #HVW #HTU #H destruct
   elim (lift_total W0 d e) #W1 #HW01
   elim (lift_total U0 (d+1) e) #U1 #HU01
-  @(snv_appl … a … W1 … U1 l) [1,2,3: /2 width=10 by cpds_lift/ ] -IHV -IHT
-  @(cpds_lift … HTU0 … HLK … HTU) /2 width=1 by lift_bind/ (**) (* full auto raises typechecker failure *)
+  @(snv_appl … a … W1 … U1 l) [1,2,3: /2 width=10 by scpds_lift/ ] -IHV -IHT
+  @(scpds_lift … HTU0 … HLK … HTU) /2 width=1 by lift_bind/ (**) (* full auto raises typechecker failure *)
 | #G #K #V #T #U0 #_ #_ #HVU0 #HTU0 #IHV #IHT #L #s #d #e #HLK #X #H
   elim (lift_inv_flat1 … H) -H #W #U #HVW #HTU #H destruct
   elim (lift_total U0 d e)
-  /3 width=12 by snv_cast, cprs_lift, cpds_lift/
+  /3 width=12 by snv_cast, cprs_lift, scpds_lift/
 ]
 qed.
 
@@ -66,15 +66,15 @@ lemma snv_inv_lift: ∀h,g,G,L,U. ⦃G, L⦄ ⊢ U ¡[h, g] → ∀K,s,d,e. ⇩[
   /4 width=5 by snv_bind, drop_skip/
 | #a #G #L #W #W1 #U #U1 #l #_ #_ #HW1 #HU1 #IHW #IHU #K #s #d #e #HLK #X #H
   elim (lift_inv_flat2 … H) -H #V #T #HVW #HTU #H destruct
-  elim (cpds_inv_lift1 … HW1 … HLK … HVW) -HW1 #W0 #HW01 #HVW0  
-  elim (cpds_inv_lift1 … HU1 … HLK … HTU) -HU1 #X #H #HTU0
+  elim (scpds_inv_lift1 … HW1 … HLK … HVW) -HW1 #W0 #HW01 #HVW0  
+  elim (scpds_inv_lift1 … HU1 … HLK … HTU) -HU1 #X #H #HTU0
   elim (lift_inv_bind2 … H) -H #Y #U0 #HY #HU01 #H destruct
   lapply (lift_inj … HY … HW01) -HY #H destruct
   /3 width=6 by snv_appl/
 | #G #L #W #U #U1 #_ #_ #HWU1 #HU1 #IHW #IHU #K #s #d #e #HLK #X #H
   elim (lift_inv_flat2 … H) -H #V #T #HVW #HTU #H destruct
   elim (cprs_inv_lift1 … HWU1 … HLK … HVW) -HWU1 #U0 #HU01 #HVU0
-  elim (cpds_inv_lift1 … HU1 … HLK … HTU) -HU1 #X #HX #HTU0 
+  elim (scpds_inv_lift1 … HU1 … HLK … HTU) -HU1 #X #HX #HTU0 
   lapply (lift_inj … HX … HU01) -HX #H destruct
   /3 width=5 by snv_cast/
 ]
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma
index 3c93fd3fc..9eefdba8e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma
@@ -14,7 +14,7 @@
 
 include "basic_2/dynamic/snv_lift.ma".
 include "basic_2/dynamic/snv_aaa.ma".
-include "basic_2/dynamic/snv_cpes.ma".
+include "basic_2/dynamic/snv_scpes.ma".
 include "basic_2/dynamic/lsubsv_snv.ma".
 
 (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
@@ -56,50 +56,50 @@ fact snv_cpr_lpr_aux: ∀h,g,G0,L0,T0.
   [ #V2 #T2 #HV12 #HT12 #H destruct -IH4
     lapply (IH1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2
     lapply (IH1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ #HT2
-    elim (cpds_cpr_lpr_aux … IH2 IH3 … HVW1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ -HVW1 -HV12 #XV #HVW2 #HXV
-    elim (cpds_cpr_lpr_aux … IH2 IH3 … HTU1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ -HTU1 -HT12 #X #HTU2 #H
+    elim (scpds_cpr_lpr_aux … IH2 IH3 … HVW1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ -HVW1 -HV12 #XV #HVW2 #HXV
+    elim (scpds_cpr_lpr_aux … IH2 IH3 … HTU1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ -HTU1 -HT12 #X #HTU2 #H
     elim (cprs_inv_abst1 … H) -H #XW #U2 #HXW #_ #H destruct -IH1 -IH3 -IH2 -L1
     elim (cprs_conf … HXV … HXW) -W1 #W2 #HXV #HXW
-    lapply (cpds_cprs_trans … HVW2 … HXV) -XV
-    lapply (cpds_cprs_trans … (ⓛ{a}W2.U2) … HTU2 ?)
+    lapply (scpds_cprs_trans … HVW2 … HXV) -XV
+    lapply (scpds_cprs_trans … (ⓛ{a}W2.U2) … HTU2 ?)
     /2 width=7 by snv_appl, cprs_bind/
   | #b #V2 #W10 #W20 #T10 #T20 #HV12 #HW120 #HT120 #H1 #H2 destruct
     elim (snv_inv_bind … HT1) -HT1 #HW10 #HT10
-    elim (cpds_inv_abst1 … HTU1) -HTU1 #W30 #T30 #HW130 #_ #H destruct -T30 -l0
+    elim (scpds_inv_abst1 … HTU1) -HTU1 #W30 #T30 #HW130 #_ #H destruct -T30 -l0
     elim (snv_fwd_da … HV1) #l #HV1l
     elim (snv_fwd_da … HW10) #l0 #HW10l
-    lapply (cpds_div … W10 … 0 … HVW1) /2 width=2 by cprs_cpds/ -W30 #HVW10
-    elim (da_cpes_aux … IH4 IH1 IH2 … HW10l … HV1l … HVW10) /2 width=1 by fqup_fpbg/
+    lapply (scpds_div … W10 … 0 … HVW1) /2 width=2 by cprs_scpds/ -W30 #HVW10
+    elim (da_scpes_aux … IH4 IH1 IH2 … HW10l … HV1l … HVW10) /2 width=1 by fqup_fpbg/
     #_ #Hl <minus_n_O #H destruct >(plus_minus_m_m l 1) in HV1l; // -Hl #HV1l
-    lapply (cpes_cpr_lpr_aux … IH2 IH3 … HVW10 … HW120 … HV12 … HL12) /2 width=1 by fqup_fpbg/ -HVW10 #HVW20
+    lapply (scpes_cpr_lpr_aux … IH2 IH3 … HVW10 … HW120 … HV12 … HL12) /2 width=1 by fqup_fpbg/ -HVW10 #HVW20
     lapply (IH2 … HV1l … HV12 … HL12) /2 width=1 by fqup_fpbg/ -HV1l #HV2l
     lapply (IH2 … HW10l … HW120 … HL12) /2 width=1 by fqup_fpbg/ -HW10l #HW20l
     lapply (IH1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2
     lapply (IH1 … HW120 … HL12) /2 width=1 by fqup_fpbg/ -HW10 #HW20
     lapply (IH1 … HT10 … HT120 … (L2.ⓛW20) ?) /2 width=1 by fqup_fpbg, lpr_pair/ -HT10 #HT20
-    @snv_bind /2 width=1 by snv_cast_cpes/
+    @snv_bind /2 width=1 by snv_cast_scpes/
     @(lsubsv_snv_trans … HT20) -HT20
     @(lsubsv_beta … (l-1)) //
-    @hsnv_cast [1,2: // ] #l0 #Hl0
-    lapply (cpes_le_aux … IH4 IH1 IH2 IH3 … HW20l … HV2l … l0 … HVW20) -IH4 -IH3 -IH2 -IH1 -HW20l -HV2l -HVW20
+    @shnv_cast [1,2: // ] #l0 #Hl0
+    lapply (scpes_le_aux … IH4 IH1 IH2 IH3 … HW20l … HV2l … l0 … HVW20) -IH4 -IH3 -IH2 -IH1 -HW20l -HV2l -HVW20
     /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_fpbs, le_S_S/
   | #b #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HV02 #HW02 #HT02 #H1 #H2 destruct -IH4
     elim (snv_inv_bind … HT1) -HT1 #HW0 #HT0
-    elim (cpds_inv_abbr_abst … HTU1) -HTU1 #X #HTU0 #HX #H destruct
+    elim (scpds_inv_abbr_abst … HTU1) -HTU1 #X #HTU0 #HX #H destruct
     elim (lift_inv_bind1 … HX) -HX #W3 #U3 #HW13 #_ #H destruct
-    elim (cpds_cpr_lpr_aux … IH2 IH3 … HVW1 … HV10 … HL12) /2 width=1 by fqup_fpbg/ -HVW1 #XV #HXV0 #HXVW1
-    elim (cpds_cpr_lpr_aux … IH2 IH3 … HTU0 … HT02 (L2.ⓓW2)) /2 width=1 by fqup_fpbg, lpr_pair/ -HTU0 #X #HXT2 #H
+    elim (scpds_cpr_lpr_aux … IH2 IH3 … HVW1 … HV10 … HL12) /2 width=1 by fqup_fpbg/ -HVW1 #XV #HXV0 #HXVW1
+    elim (scpds_cpr_lpr_aux … IH2 IH3 … HTU0 … HT02 (L2.ⓓW2)) /2 width=1 by fqup_fpbg, lpr_pair/ -HTU0 #X #HXT2 #H
     elim (cprs_inv_abst1 … H) -H #W #U2 #HW3 #_ #H destruct -U3
     lapply (IH1 … HW02 … HL12) /2 width=1 by fqup_fpbg/ #HW2
     lapply (IH1 … HV10 … HL12) /2 width=1 by fqup_fpbg/ #HV0
     lapply (IH1 … HT02 (L2.ⓓW2) ?) /2 width=1 by fqup_fpbg, lpr_pair/ -L1 #HT2
     lapply (snv_lift … HV0 (L2.ⓓW2) (Ⓕ) … HV02) /2 width=1 by drop_drop/ -HV0 #HV2
     elim (lift_total XV 0 1) #XW #HXVW
-    lapply (cpds_lift … HXV0 (L2.ⓓW2) (Ⓕ) … HV02 … HXVW) /2 width=1 by drop_drop/ -V0 #HXWV2
+    lapply (scpds_lift … HXV0 (L2.ⓓW2) (Ⓕ) … HV02 … HXVW) /2 width=1 by drop_drop/ -V0 #HXWV2
     lapply (cprs_lift … HXVW1 (L2.ⓓW2) (Ⓕ) … HW13 … HXVW) /2 width=1 by drop_drop/ -W1 -XV #HXW3
     elim (cprs_conf … HXW3 … HW3) -W3 #W3 #HXW3 #HW3
-    lapply (cpds_cprs_trans … HXWV2 … HXW3) -XW
-    lapply (cpds_cprs_trans … (ⓛ{a}W3.U2) … HXT2 ?) /2 width=1 by cprs_bind/ -W
+    lapply (scpds_cprs_trans … HXWV2 … HXW3) -XW
+    lapply (scpds_cprs_trans … (ⓛ{a}W3.U2) … HXT2 ?) /2 width=1 by cprs_bind/ -W
     /3 width=6 by snv_appl, snv_bind/
   ]
 | #W1 #T1 #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4
@@ -107,11 +107,11 @@ fact snv_cpr_lpr_aux: ∀h,g,G0,L0,T0.
   elim (cpr_inv_cast1 … H2) -H2
   [ * #W2 #T2 #HW12 #HT12 #H destruct
     elim (snv_fwd_da … HW1) #l #HW1l
-    lapply (cpds_div … W1 … 0 … HTU1) /2 width=2 by cprs_cpds/ -U1 -l #HWT1
-    lapply (cpes_cpr_lpr_aux … IH2 IH3 … HWT1 … HW12 … HT12 … HL12) /2 width=1 by fqup_fpbg/
+    lapply (scpds_div … W1 … 0 … HTU1) /2 width=2 by cprs_scpds/ -U1 -l #HWT1
+    lapply (scpes_cpr_lpr_aux … IH2 IH3 … HWT1 … HW12 … HT12 … HL12) /2 width=1 by fqup_fpbg/
     lapply (IH1 … HW12 … HL12) /2 width=1 by fqup_fpbg/
     lapply (IH1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ -L1
-    /2 width=1 by snv_cast_cpes/
+    /2 width=1 by snv_cast_scpes/
   | #H -IH3 -IH2 -HW1 -U1
     lapply (IH1 … H … HL12) /2 width=1 by fqup_fpbg/
   ]
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lstas.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lstas.ma
index 4213293b8..45c861402 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lstas.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lstas.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/dynamic/snv_lift.ma".
-include "basic_2/dynamic/snv_cpes.ma".
+include "basic_2/dynamic/snv_scpes.ma".
 
 (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
 
@@ -49,8 +49,8 @@ fact snv_lstas_aux: ∀h,g,G0,L0,T0.
   lapply (da_inv_flat … Hl1) -Hl1 #Hl1
   elim (lstas_inv_appl1 … H2) -H2 #T0 #HT10 #H destruct
   lapply (IH1 … HT1 … Hl1 … HT10) /2 width=1 by fqup_fpbg/ #HT0
-  lapply (lstas_cpds_aux … IH1 IH4 IH3 IH2 … Hl1 … HT10 … HTU1) -IH4 -IH3 -IH2 -IH1 /2 width=1 by fqup_fpbg/ -T1 -l1 #H
-  elim (cpes_inv_abst2 … H) -H /3 width=6 by snv_appl, cpds_cprs_trans/
+  lapply (lstas_scpds_aux … IH1 IH4 IH3 IH2 … Hl1 … HT10 … HTU1) -IH4 -IH3 -IH2 -IH1 /2 width=1 by fqup_fpbg/ -T1 -l1 #H
+  elim (scpes_inv_abst2 … H) -H /3 width=6 by snv_appl, scpds_cprs_trans/
 | #U1 #T1 #HG0 #HL0 #HT0 #H1 #l1 #l2 @(nat_ind_plus … l2) -l2 [ #_ | #l2 #_ #Hl21 ] #Hl1 #X #H2 destruct -IH4 -IH3 -IH2
   [ lapply (lstas_inv_O … H2) -H2 #H destruct // ]
   elim (snv_inv_cast … H1) -H1 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lstas_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lstas_lpr.ma
index a974f248f..388cf2ba4 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lstas_lpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lstas_lpr.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/dynamic/snv_aaa.ma".
-include "basic_2/dynamic/snv_cpes.ma".
+include "basic_2/dynamic/snv_scpes.ma".
 include "basic_2/dynamic/lsubsv_lstas.ma".
 
 (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
@@ -86,13 +86,13 @@ fact lstas_cpr_lpr_aux: ∀h,g,G0,L0,T0.
     elim (snv_inv_bind … HT1) -HT1 #HW2 #HT2
     lapply (da_inv_bind … Hl1) -Hl1 #Hl1
     elim (lstas_inv_bind1 … HT1U) -HT1U #U #HT2U #H destruct
-    elim (cpds_inv_abst1 … HTU1) -HTU1 #W0 #U0 #HW20 #_ #H destruct -U0 -l0
+    elim (scpds_inv_abst1 … HTU1) -HTU1 #W0 #U0 #HW20 #_ #H destruct -U0 -l0
     elim (snv_fwd_da … HW2) #l0 #HW2l
-    lapply (cpds_div … W2 … 0 … HVW1) /2 width=3 by cprs_cpds/ -W0 #H21
+    lapply (scpds_div … W2 … 0 … HVW1) /2 width=3 by cprs_scpds/ -W0 #H21
     elim (snv_fwd_da … HV1) #l #HV1l
-    elim (da_cpes_aux … IH4 IH3 IH2 … HW2l … HV1l … H21) /2 width=1 by fqup_fpbg/ #_ #H
+    elim (da_scpes_aux … IH4 IH3 IH2 … HW2l … HV1l … H21) /2 width=1 by fqup_fpbg/ #_ #H
     <minus_n_O #H0 destruct >(plus_minus_m_m l 1) in HV1l; // -H #HV1l
-    lapply (cpes_cpr_lpr_aux … IH2 IH1 … H21 … HW23 … HV12 … HL12) -H21 /2 width=1 by fqup_fpbg/ #H32
+    lapply (scpes_cpr_lpr_aux … IH2 IH1 … H21 … HW23 … HV12 … HL12) -H21 /2 width=1 by fqup_fpbg/ #H32
     lapply (IH3 … HW23 … HL12) /2 width=1 by fqup_fpbg/ #HW3
     lapply (IH3 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2
     lapply (IH2 … HW2l … HW23 … HL12) /2 width=1 by fqup_fpbg/ -HW2 -HW2l #HW3l
@@ -106,8 +106,8 @@ fact lstas_cpr_lpr_aux: ∀h,g,G0,L0,T0.
       /4 width=3 by cpcs_flat, cpcs_bind2, lpr_cpr_conf/
     | -U3
       @(lsubsv_beta … (l-1)) /3 width=7 by fqup_fpbg/
-      @hsnv_cast [1,2: // ] #l0 #Hl0
-      lapply (cpes_le_aux … IH4 IH3 IH2 IH1 … HW3l … HV2l … l0 … H32) -IH4 -IH3 -IH2 -IH1 -HW3l -HV2l -H32
+      @shnv_cast [1,2: // ] #l0 #Hl0
+      lapply (scpes_le_aux … IH4 IH3 IH2 IH1 … HW3l … HV2l … l0 … H32) -IH4 -IH3 -IH2 -IH1 -HW3l -HV2l -H32
       /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_fpbs, le_S_S/
     | -IH1 -IH3 -IH4 /3 width=9 by fqup_fpbg, lpr_pair/
     ]
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_preserve.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_preserve.ma
index 1ee74e64a..5f76fea80 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_preserve.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_preserve.ma
@@ -53,3 +53,9 @@ theorem lstas_cpr_lpr: ∀h,g,G,L,T. IH_lstas_cpr_lpr h g G L T.
 qed-.
 
 (* Advanced preservation properties *****************************************)
+
+lemma snv_cprs_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+                    ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, g].
+#h #g #G #L1 #T1 #HT1 #T2 #H
+@(cprs_ind … H) -T2 /3 width=5 by snv_cpr_lpr/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_scpes.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_scpes.ma
new file mode 100644
index 000000000..5ee696600
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_scpes.ma
@@ -0,0 +1,199 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/fpbs_lift.ma".
+include "basic_2/computation/fpbg_fleq.ma".
+include "basic_2/equivalence/scpes_cpcs.ma".
+include "basic_2/equivalence/scpes_scpes.ma".
+include "basic_2/dynamic/snv.ma".
+
+(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
+
+(* Inductive premises for the preservation results **************************)
+
+definition IH_snv_cpr_lpr: ∀h:sh. sd h → relation3 genv lenv term ≝
+                           λh,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+                           ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, g].
+
+definition IH_da_cpr_lpr: ∀h:sh. sd h → relation3 genv lenv term ≝
+                          λh,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+                          ∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l →
+                          ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
+                          ⦃G, L2⦄ ⊢ T2 ▪[h, g] l.
+
+definition IH_lstas_cpr_lpr: ∀h:sh. sd h → relation3 genv lenv term ≝
+                             λh,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+                             ∀l1,l2. l2 ≤ l1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 →
+                             ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, l2] U1 →
+                             ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
+                             ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, l2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2.
+
+definition IH_snv_lstas: ∀h:sh. sd h → relation3 genv lenv term ≝
+                         λh,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] →
+                         ∀l1,l2. l2 ≤ l1 → ⦃G, L⦄ ⊢ T ▪[h, g] l1 →
+                         ∀U. ⦃G, L⦄ ⊢ T •*[h, l2] U → ⦃G, L⦄ ⊢ U ¡[h, g].
+
+(* Properties for the preservation results **********************************)
+
+fact snv_cprs_lpr_aux: ∀h,g,G0,L0,T0.
+                       (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+                       ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+                       ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, g].
+#h #g #G0 #L0 #T0 #IH #G #L1 #T1 #HLT0 #HT1 #T2 #H
+@(cprs_ind … H) -T2 /4 width=6 by fpbg_fpbs_trans, cprs_fpbs/
+qed-.
+
+fact da_cprs_lpr_aux: ∀h,g,G0,L0,T0.
+                      (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+                      (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
+                      ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+                      ∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l →
+                      ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ▪[h, g] l.
+#h #g #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #HLT0 #HT1 #l #Hl #T2 #H
+@(cprs_ind … H) -T2 /4 width=10 by snv_cprs_lpr_aux, fpbg_fpbs_trans, cprs_fpbs/
+qed-.
+
+fact da_scpds_lpr_aux: ∀h,g,G0,L0,T0.
+                       (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lstas h g G1 L1 T1) →
+                       (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+                       (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
+                       ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+                       ∀l1. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 →
+                       ∀T2,l2. ⦃G, L1⦄ ⊢ T1 •*➡*[h, g, l2] T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
+                       l2 ≤ l1 ∧ ⦃G, L2⦄ ⊢ T2 ▪[h, g] l1-l2.
+#h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L1 #T1 #HLT0 #HT1 #l1 #Hl1 #T2 #l2 * #T #l0 #Hl20 #H #HT1 #HT2 #L2 #HL12
+lapply (da_mono … H … Hl1) -H #H destruct
+lapply (lstas_da_conf … HT1 … Hl1) #Hl12
+lapply (da_cprs_lpr_aux … IH2 IH1 … Hl12 … HT2 … HL12) -IH2 -IH1 -HT2 -HL12
+/3 width=8 by fpbg_fpbs_trans, lstas_fpbs, conj/
+qed-.
+
+fact da_scpes_aux: ∀h,g,G0,L0,T0.
+                   (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lstas h g G1 L1 T1) →
+                   (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+                   (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
+                   ∀G,L,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, g] →
+                   ∀T2. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T2⦄ → ⦃G, L⦄ ⊢ T2 ¡[h, g] →
+                   ∀l11. ⦃G, L⦄ ⊢ T1 ▪[h, g] l11 → ∀l12. ⦃G, L⦄ ⊢ T2 ▪[h, g] l12 →
+                   ∀l21,l22. ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l21, l22] T2 →
+                   ∧∧ l21 ≤ l11 & l22 ≤ l12 & l11 - l21 = l12 - l22.
+#h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L #T1 #HLT01 #HT1 #T2 #HLT02 #HT2 #l11 #Hl11 #l12 #Hl12 #l21 #l22 * #T #HT1 #HT2
+elim (da_scpds_lpr_aux … IH3 IH2 IH1 … Hl11 … HT1 … L) -Hl11 -HT1 //
+elim (da_scpds_lpr_aux … IH3 IH2 IH1 … Hl12 … HT2 … L) -Hl12 -HT2 //
+/3 width=7 by da_mono, and3_intro/
+qed-.
+
+fact lstas_cprs_lpr_aux: ∀h,g,G0,L0,T0.
+                         (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+                         (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
+                         (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) →
+                         ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+                         ∀l1,l2. l2 ≤ l1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 →
+                         ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, l2] U1 →
+                         ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
+                         ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, l2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2.
+#h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #l1 #l2 #Hl21 #Hl1 #U1 #HTU1 #T2 #H
+@(cprs_ind … H) -T2 [ /2 width=10 by/ ]
+#T #T2 #HT1T #HTT2 #IHT1 #L2 #HL12
+elim (IHT1 L1) // -IHT1 #U #HTU #HU1
+elim (IH1 … Hl21 … HTU … HTT2 … HL12) -IH1 -HTU -HTT2
+[2: /3 width=12 by da_cprs_lpr_aux/
+|3: /3 width=10 by snv_cprs_lpr_aux/
+|4: /3 width=5 by fpbg_fpbs_trans, cprs_fpbs/
+] -G0 -L0 -T0 -T1 -T -l1
+/4 width=5 by lpr_cpcs_conf, cpcs_trans, ex2_intro/
+qed-.
+
+fact scpds_cpr_lpr_aux: ∀h,g,G0,L0,T0.
+                        (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
+                        (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) →
+                        ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+                        ∀U1,l. ⦃G, L1⦄ ⊢ T1 •*➡*[h, g, l] U1 →
+                        ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
+                        ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*➡*[h, g, l] U2 & ⦃G, L2⦄ ⊢ U1 ➡* U2.
+#h #g #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #U1 #l2 * #W1 #l1 #Hl21 #HTl1 #HTW1 #HWU1 #T2 #HT12 #L2 #HL12
+elim (IH1 … H01 … HTW1 … HT12 … HL12) -IH1 // #W2 #HTW2 #HW12
+lapply (IH2 … H01 … HTl1 … HT12 … HL12) -L0 -T0 // -T1
+lapply (lpr_cprs_conf … HL12 … HWU1) -L1 #HWU1
+lapply (cpcs_canc_sn … HW12 HWU1) -W1 #H
+elim (cpcs_inv_cprs … H) -H /3 width=6 by ex4_2_intro, ex2_intro/
+qed-.
+
+fact scpes_cpr_lpr_aux: ∀h,g,G0,L0,T0.
+                        (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
+                        (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) →
+                        ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+                        ∀T2. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T2⦄ → ⦃G, L1⦄ ⊢ T2 ¡[h, g] →
+                        ∀l1,l2. ⦃G, L1⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2 →
+                        ∀U1. ⦃G, L1⦄ ⊢ T1 ➡ U1 → ∀U2. ⦃G, L1⦄ ⊢ T2 ➡ U2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
+                        ⦃G, L2⦄ ⊢ U1 •*⬌*[h, g, l1, l2] U2.
+#h #g #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #T2 #HT02 #HT2 #l1 #l2 * #T0 #HT10 #HT20 #U1 #HTU1 #U2 #HTU2 #L2 #HL12
+elim (scpds_cpr_lpr_aux … IH2 IH1 … HT10 … HTU1 … HL12) -HT10 -HTU1 // #X1 #HUX1 #H1
+elim (scpds_cpr_lpr_aux … IH2 IH1 … HT20 … HTU2 … HL12) -HT20 -HTU2 // #X2 #HUX2 #H2
+elim (cprs_conf … H1 … H2) -T0
+/3 width=5 by scpds_div, scpds_cprs_trans/
+qed-.
+
+fact lstas_scpds_aux: ∀h,g,G0,L0,T0.
+                      (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lstas h g G1 L1 T1) →
+                      (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+                      (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
+                      (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) →
+                      ∀G,L,T. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T⦄ → ⦃G, L⦄ ⊢ T ¡[h, g] →
+                      ∀l,l1. l1 ≤ l → ⦃G, L⦄ ⊢ T ▪[h, g] l → ∀T1. ⦃G, L⦄ ⊢ T •*[h, l1] T1 →
+                      ∀T2,l2. ⦃G, L⦄ ⊢ T •*➡*[h, g, l2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l2-l1, l1-l2] T2.
+#h #g #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G #L #T #H0 #HT #l #l1 #Hl1 #HTl #T1 #HT1 #T2 #l2 * #X #l0 #Hl20 #H #HTX #HXT2
+lapply (da_mono … H … HTl) -H #H destruct
+lapply (lstas_da_conf … HT1 … HTl) #HTl1
+lapply (lstas_da_conf … HTX … HTl) #HXl
+lapply (da_cprs_lpr_aux … IH3 IH2 … HXl … HXT2 L ?)
+[1,2,3: /3 width=8 by fpbg_fpbs_trans, lstas_fpbs/ ] #HTl2
+elim (le_or_ge l1 l2) #Hl12 >(eq_minus_O … Hl12)
+[ /5 width=3 by scpds_refl, lstas_conf_le, monotonic_le_minus_l, ex4_2_intro, ex2_intro/
+| lapply (lstas_conf_le … HTX … HT1) // #HXT1 -HT1
+  elim (lstas_cprs_lpr_aux … IH3 IH2 IH1 … HXl … HXT1 … HXT2 L) -IH3 -IH2 -IH1 -HXl -HXT1 -HXT2
+  /3 width=8 by cpcs_scpes, fpbg_fpbs_trans, lstas_fpbs, monotonic_le_minus_l/
+]
+qed-.
+
+fact scpes_le_aux: ∀h,g,G0,L0,T0.
+                   (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lstas h g G1 L1 T1) →
+                   (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+                   (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
+                   (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) →
+                   ∀G,L,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, g] →
+                   ∀T2. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T2⦄ → ⦃G, L⦄ ⊢ T2 ¡[h, g] →
+                   ∀l11. ⦃G, L⦄ ⊢ T1 ▪[h, g] l11 → ∀l12. ⦃G, L⦄ ⊢ T2 ▪[h, g] l12 →
+                   ∀l21,l22,l. l21 + l ≤ l11 → l22 + l ≤ l12 →
+                   ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l21, l22] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l21+l, l22+l] T2.
+#h #g #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G #L #T1 #H01 #HT1 #T2 #H02 #HT2 #l11 #Hl11 #Hl12 #Hl12 #l21 #l22 #l #H1 #H2 * #T0 #HT10 #HT20 
+elim (da_inv_sta … Hl11) #X1 #HTX1
+elim (lstas_total … HTX1 (l21+l)) -X1 #X1 #HTX1
+elim (da_inv_sta … Hl12) #X2 #HTX2
+elim (lstas_total … HTX2 (l22+l)) -X2 #X2 #HTX2
+lapply (lstas_scpds_aux … IH4 IH3 IH2 IH1 … Hl11 … HTX1 … HT10) -HT10
+[1,2,3: // | >eq_minus_O [2: // ] <minus_plus_m_m_commutative #HX1 ]
+lapply (lstas_scpds_aux … IH4 IH3 IH2 IH1 … Hl12 … HTX2 … HT20) -HT20
+[1,2,3: // | >eq_minus_O [2: // ] <minus_plus_m_m_commutative #HX2 ]
+lapply (lstas_scpes_trans … Hl11 … HTX1 … HX1) [ // ] -Hl11 -HTX1 -HX1 -H1 #H1
+lapply (lstas_scpes_trans … Hl12 … HTX2 … HX2) [ // ] -Hl12 -HTX2 -HX2 -H2 #H2
+lapply (scpes_canc_dx … H1 … H2) // (**) (* full auto raises NTypeChecker failure *)
+qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma snv_cast_scpes: ∀h,g,G,L,U,T. ⦃G, L⦄ ⊢ U ¡[h, g] →  ⦃G, L⦄ ⊢ T ¡[h, g] →
+                      ⦃G, L⦄ ⊢ U •*⬌*[h, g, 0, 1] T → ⦃G, L⦄ ⊢ ⓝU.T ¡[h, g].
+#h #g #G #L #U #T #HU #HT * /3 width=3 by snv_cast, scpds_fwd_cprs/
+qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpes.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpes.ma
deleted file mode 100644
index 41ac80b94..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpes.ma
+++ /dev/null
@@ -1,41 +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/notation/relations/dpconvstar_8.ma".
-include "basic_2/computation/cpds.ma".
-
-(* DECOMPOSED EXTENDED PARALLEL EQUIVALENCE FOR TERMS ***********************)
-
-definition cpes: ∀h. sd h → nat → nat → relation4 genv lenv term term ≝
-                 λh,g,l1,l2,G,L,T1,T2.
-                 ∃∃T. ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l1] T & ⦃G, L⦄ ⊢ T2 •*➡*[h, g, l2] T.
-
-interpretation "decomposed extended parallel equivalence (term)"
-   'DPConvStar h g l1 l2 G L T1 T2 = (cpes h g l1 l2 G L T1 T2).
-
-(* Basic properties *********************************************************)
-
-lemma cpds_div: ∀h,g,G,L,T1,T2,T,l1,l2.
-                ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l1] T → ⦃G, L⦄ ⊢ T2 •*➡*[h, g, l2] T →
-                ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2.
-/2 width=3 by ex2_intro/ qed.
-
-lemma cpes_refl_O_O: ∀h,g,G,L,T,l. ⦃G, L⦄ ⊢ T ▪[h, g] l →
-                     ⦃G, L⦄ ⊢ T •*⬌*[h, g, 0, 0] T.
-/3 width=3 by cpds_refl, cpds_div/ qed.
-
-lemma cpes_sym: ∀h,g,G,L,T1,T2,l1,l2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2 →
-                ⦃G, L⦄ ⊢ T2 •*⬌*[h, g, l2, l1] T1.
-#h #g #G #L #T1 #T2 #L1 #l2 * /2 width=3 by cpds_div/
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpes_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpes_aaa.ma
deleted file mode 100644
index 6d1ad9fc3..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpes_aaa.ma
+++ /dev/null
@@ -1,29 +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/cpds_aaa.ma".
-include "basic_2/equivalence/cpes.ma".
-
-(* DECOMPOSED EXTENDED PARALLEL EQUIVALENCE FOR TERMS ***********************)
-
-(* Main inversion lemmas about atomic arity assignment on terms *************)
-
-theorem cpes_aaa_mono: ∀h,g,G,L,T1,T2,l1,l2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2 →
-                       ∀A1. ⦃G, L⦄ ⊢ T1 ⁝ A1 → ∀A2. ⦃G, L⦄ ⊢ T2 ⁝ A2 →
-                       A1 = A2.
-#h #g #G #L #T1 #T2 #l1 #l2 * #T #HT1 #HT2 #A1 #HA1 #A2 #HA2
-lapply (cpds_aaa_conf … HA1 … HT1) -T1 #HA1
-lapply (cpds_aaa_conf … HA2 … HT2) -T2 #HA2
-lapply (aaa_mono … HA1 … HA2) -L -T //
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpes_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpes_cpcs.ma
deleted file mode 100644
index 569f46b64..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpes_cpcs.ma
+++ /dev/null
@@ -1,39 +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/cpds_cpds.ma".
-include "basic_2/equivalence/cpcs_cpcs.ma".
-include "basic_2/equivalence/cpes.ma".
-
-(* DECOMPOSED EXTENDED PARALLEL EQUIVALENCE FOR TERMS ***********************)
-
-(* Inversion lemmas on parallel equivalence for terms ***********************)
-
-lemma cpes_inv_lstas_eq: ∀h,g,G,L,T1,T2,l1,l2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2 →
-                         ∀U1. ⦃G, L⦄ ⊢ T1 •*[h, l1] U1 →
-                         ∀U2. ⦃G, L⦄ ⊢ T2 •*[h, l2] U2 → ⦃G, L⦄ ⊢ U1 ⬌* U2.
-#h #g #G #L #T1 #T2 #l1 #l2 * #T #HT1 #HT2 #U1 #HTU1 #U2 #HTU2
-/3 width=8 by cpds_inv_lstas_eq, cprs_div/
-qed-.
-
-(* Properties on parallel equivalence for terms ***********************)
-
-lemma cpcs_cpes: ∀h,g,G,L,T1,l11. ⦃G, L⦄ ⊢ T1 ▪[h, g] l11 →
-                 ∀U1,l12. l12 ≤ l11 → ⦃G, L⦄ ⊢ T1 •*[h, l12] U1 →
-                 ∀T2,l21. ⦃G, L⦄ ⊢ T2 ▪[h, g] l21 →
-                 ∀U2,l22. l22 ≤ l21 → ⦃G, L⦄ ⊢ T2 •*[h, l22] U2 →
-                 ⦃G, L⦄ ⊢ U1 ⬌* U2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l12, l22] T2.
-#h #g #G #L #T1 #l11 #HT1 #U1 #l12 #Hl121 #HTU1 #T2 #l21 #HT2 #U2 #l22 #Hl221 #HTU2 #HU12
-elim (cpcs_inv_cprs … HU12) -HU12 /3 width=6 by cpds_div, ex4_2_intro/
-qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpes_cpes.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpes_cpes.ma
deleted file mode 100644
index 3843dcc43..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpes_cpes.ma
+++ /dev/null
@@ -1,62 +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/cpds_cpds.ma".
-include "basic_2/equivalence/cpes.ma".
-
-(* DECOMPOSED EXTENDED PARALLEL EQUIVALENCE FOR TERMS ***********************)
-
-(* Advanced inversion lemmas ************************************************)
-
-lemma cpes_inv_abst2: ∀h,g,a,G,L,T1,T2,W2,l1,l2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] ⓛ{a}W2.T2 →
-                      ∃∃W,T. ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l1] ⓛ{a}W.T & ⦃G, L⦄ ⊢ W2 ➡* W & 
-                             ⦃G, L.ⓛW2⦄ ⊢ T2 •*➡*[h, g, l2] T.
-#h #g #a #G #L #T1 #T2 #W2 #l1 #l2 * #T0 #HT10 #H
-elim (cpds_inv_abst1 … H) -H #W #T #HW2 #HT2 #H destruct /2 width=5 by ex3_2_intro/
-qed-.
-
-(* Advanced properties ******************************************************)
-
-lemma cpes_refl: ∀h,g,G,L,T,l1,l2. l2 ≤ l1 → ⦃G, L⦄ ⊢ T ▪[h, g] l1 →
-                 ⦃G, L⦄ ⊢ T •*⬌*[h, g, l2, l2] T.
-#h #g #G #L #T #l1 #l2 #Hl21 #Hl1
-elim (da_inv_sta … Hl1) #U #HTU
-elim (lstas_total … HTU l2) -U /3 width=3 by cpds_div, lstas_cpds/
-qed.
-
-lemma lstas_cpes_trans: ∀h,g,G,L,T1,l0,l1. ⦃G, L⦄ ⊢ T1 ▪[h, g] l0 → l1 ≤ l0 →
-                        ∀T. ⦃G, L⦄ ⊢ T1 •*[h, l1] T →
-                        ∀T2,l,l2. ⦃G, L⦄ ⊢ T •*⬌*[h,g,l,l2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h,g,l1+l,l2] T2.
-#h #g #G #L #T1 #l0 #l1 #Hl0 #Hl10 #T #HT1 #T2 #l #l2 *
-/3 width=3 by cpds_div, lstas_cpds_trans/ qed-.
-
-(* Main properties **********************************************************)
-
-theorem cpes_trans: ∀h,g,G,L,T1,T,l1,l. ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l] T →
-                    ∀T2,l2. ⦃G, L⦄ ⊢ T •*⬌*[h, g, l, l2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2.
-#h #g #G #L #T1 #T #l1 #l * #X1 #HT1X1 #HTX1 #T2 #l2 * #X2 #HTX2 #HT2X2
-elim (cpds_conf_eq … HTX1 … HTX2) -T -l /3 width=5 by cpds_cprs_trans, cpds_div/
-qed-.
-
-theorem cpes_canc_sn: ∀h,g,G,L,T,T1,l,l1. ⦃G, L⦄ ⊢ T •*⬌*[h, g, l, l1] T1 →
-                      ∀T2,l2. ⦃G, L⦄ ⊢ T •*⬌*[h, g, l, l2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2.
-#h #g #G #L #T #T1 #l #l1 #HT1
-@cpes_trans /2 width=1 by cpes_sym/ (**) (* full auto raises NTypeChecker failure *)
-qed-.
-
-theorem cpes_canc_dx: ∀h,g,G,L,T1,T,l1,l. ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l] T →
-                      ∀T2,l2. ⦃G, L⦄ ⊢ T2 •*⬌*[h, g, l2, l] T → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2.
-#h #g #G #L #T1 #T #l1 #l #HT1 #T2 #l2 #HT2
-@(cpes_trans … HT1) -T1 -l1 /2 width=1 by cpes_sym/ (**) (* full auto raises NTypeChecker failure *)
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/scpes.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/scpes.ma
new file mode 100644
index 000000000..4e838fee0
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/scpes.ma
@@ -0,0 +1,41 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/notation/relations/dpconvstar_8.ma".
+include "basic_2/computation/scpds.ma".
+
+(* STRATIFIED DECOMPOSED PARALLEL EQUIVALENCE FOR TERMS *********************)
+
+definition scpes: ∀h. sd h → nat → nat → relation4 genv lenv term term ≝
+                  λh,g,l1,l2,G,L,T1,T2.
+                  ∃∃T. ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l1] T & ⦃G, L⦄ ⊢ T2 •*➡*[h, g, l2] T.
+
+interpretation "stratified decomposed parallel equivalence (term)"
+   'DPConvStar h g l1 l2 G L T1 T2 = (scpes h g l1 l2 G L T1 T2).
+
+(* Basic properties *********************************************************)
+
+lemma scpds_div: ∀h,g,G,L,T1,T2,T,l1,l2.
+                 ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l1] T → ⦃G, L⦄ ⊢ T2 •*➡*[h, g, l2] T →
+                 ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2.
+/2 width=3 by ex2_intro/ qed.
+
+lemma scpes_refl_O_O: ∀h,g,G,L,T,l. ⦃G, L⦄ ⊢ T ▪[h, g] l →
+                      ⦃G, L⦄ ⊢ T •*⬌*[h, g, 0, 0] T.
+/3 width=3 by scpds_refl, scpds_div/ qed.
+
+lemma scpes_sym: ∀h,g,G,L,T1,T2,l1,l2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2 →
+                 ⦃G, L⦄ ⊢ T2 •*⬌*[h, g, l2, l1] T1.
+#h #g #G #L #T1 #T2 #L1 #l2 * /2 width=3 by scpds_div/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/scpes_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/scpes_aaa.ma
new file mode 100644
index 000000000..39bc00547
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/scpes_aaa.ma
@@ -0,0 +1,29 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/scpds_aaa.ma".
+include "basic_2/equivalence/scpes.ma".
+
+(* DECOMPOSED EXTENDED PARALLEL EQUIVALENCE FOR TERMS ***********************)
+
+(* Main inversion lemmas about atomic arity assignment on terms *************)
+
+theorem scpes_aaa_mono: ∀h,g,G,L,T1,T2,l1,l2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2 →
+                        ∀A1. ⦃G, L⦄ ⊢ T1 ⁝ A1 → ∀A2. ⦃G, L⦄ ⊢ T2 ⁝ A2 →
+                        A1 = A2.
+#h #g #G #L #T1 #T2 #l1 #l2 * #T #HT1 #HT2 #A1 #HA1 #A2 #HA2
+lapply (scpds_aaa_conf … HA1 … HT1) -T1 #HA1
+lapply (scpds_aaa_conf … HA2 … HT2) -T2 #HA2
+lapply (aaa_mono … HA1 … HA2) -L -T //
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/scpes_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/scpes_cpcs.ma
new file mode 100644
index 000000000..a746490a3
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/scpes_cpcs.ma
@@ -0,0 +1,39 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/scpds_scpds.ma".
+include "basic_2/equivalence/cpcs_cpcs.ma".
+include "basic_2/equivalence/scpes.ma".
+
+(* STRATIFIED DECOMPOSED PARALLEL EQUIVALENCE FOR TERMS *********************)
+
+(* Inversion lemmas on parallel equivalence for terms ***********************)
+
+lemma scpes_inv_lstas_eq: ∀h,g,G,L,T1,T2,l1,l2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2 →
+                         ∀U1. ⦃G, L⦄ ⊢ T1 •*[h, l1] U1 →
+                         ∀U2. ⦃G, L⦄ ⊢ T2 •*[h, l2] U2 → ⦃G, L⦄ ⊢ U1 ⬌* U2.
+#h #g #G #L #T1 #T2 #l1 #l2 * #T #HT1 #HT2 #U1 #HTU1 #U2 #HTU2
+/3 width=8 by scpds_inv_lstas_eq, cprs_div/
+qed-.
+
+(* Properties on parallel equivalence for terms ***********************)
+
+lemma cpcs_scpes: ∀h,g,G,L,T1,l11. ⦃G, L⦄ ⊢ T1 ▪[h, g] l11 →
+                  ∀U1,l12. l12 ≤ l11 → ⦃G, L⦄ ⊢ T1 •*[h, l12] U1 →
+                  ∀T2,l21. ⦃G, L⦄ ⊢ T2 ▪[h, g] l21 →
+                  ∀U2,l22. l22 ≤ l21 → ⦃G, L⦄ ⊢ T2 •*[h, l22] U2 →
+                  ⦃G, L⦄ ⊢ U1 ⬌* U2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l12, l22] T2.
+#h #g #G #L #T1 #l11 #HT1 #U1 #l12 #Hl121 #HTU1 #T2 #l21 #HT2 #U2 #l22 #Hl221 #HTU2 #HU12
+elim (cpcs_inv_cprs … HU12) -HU12 /3 width=6 by scpds_div, ex4_2_intro/
+qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/scpes_scpes.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/scpes_scpes.ma
new file mode 100644
index 000000000..2f8bcd962
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/scpes_scpes.ma
@@ -0,0 +1,62 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/scpds_scpds.ma".
+include "basic_2/equivalence/scpes.ma".
+
+(* STRATIFIED DECOMPOSED PARALLEL EQUIVALENCE FOR TERMS *********************)
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma scpes_inv_abst2: ∀h,g,a,G,L,T1,T2,W2,l1,l2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] ⓛ{a}W2.T2 →
+                       ∃∃W,T. ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l1] ⓛ{a}W.T & ⦃G, L⦄ ⊢ W2 ➡* W & 
+                              ⦃G, L.ⓛW2⦄ ⊢ T2 •*➡*[h, g, l2] T.
+#h #g #a #G #L #T1 #T2 #W2 #l1 #l2 * #T0 #HT10 #H
+elim (scpds_inv_abst1 … H) -H #W #T #HW2 #HT2 #H destruct /2 width=5 by ex3_2_intro/
+qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma scpes_refl: ∀h,g,G,L,T,l1,l2. l2 ≤ l1 → ⦃G, L⦄ ⊢ T ▪[h, g] l1 →
+                  ⦃G, L⦄ ⊢ T •*⬌*[h, g, l2, l2] T.
+#h #g #G #L #T #l1 #l2 #Hl21 #Hl1
+elim (da_inv_sta … Hl1) #U #HTU
+elim (lstas_total … HTU l2) -U /3 width=3 by scpds_div, lstas_scpds/
+qed.
+
+lemma lstas_scpes_trans: ∀h,g,G,L,T1,l0,l1. ⦃G, L⦄ ⊢ T1 ▪[h, g] l0 → l1 ≤ l0 →
+                         ∀T. ⦃G, L⦄ ⊢ T1 •*[h, l1] T →
+                         ∀T2,l,l2. ⦃G, L⦄ ⊢ T •*⬌*[h,g,l,l2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h,g,l1+l,l2] T2.
+#h #g #G #L #T1 #l0 #l1 #Hl0 #Hl10 #T #HT1 #T2 #l #l2 *
+/3 width=3 by scpds_div, lstas_scpds_trans/ qed-.
+
+(* Main properties **********************************************************)
+
+theorem scpes_trans: ∀h,g,G,L,T1,T,l1,l. ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l] T →
+                     ∀T2,l2. ⦃G, L⦄ ⊢ T •*⬌*[h, g, l, l2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2.
+#h #g #G #L #T1 #T #l1 #l * #X1 #HT1X1 #HTX1 #T2 #l2 * #X2 #HTX2 #HT2X2
+elim (scpds_conf_eq … HTX1 … HTX2) -T -l /3 width=5 by scpds_cprs_trans, scpds_div/
+qed-.
+
+theorem scpes_canc_sn: ∀h,g,G,L,T,T1,l,l1. ⦃G, L⦄ ⊢ T •*⬌*[h, g, l, l1] T1 →
+                       ∀T2,l2. ⦃G, L⦄ ⊢ T •*⬌*[h, g, l, l2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2.
+#h #g #G #L #T #T1 #l #l1 #HT1
+@scpes_trans /2 width=1 by scpes_sym/ (**) (* full auto raises NTypeChecker failure *)
+qed-.
+
+theorem scpes_canc_dx: ∀h,g,G,L,T1,T,l1,l. ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l] T →
+                       ∀T2,l2. ⦃G, L⦄ ⊢ T2 •*⬌*[h, g, l2, l] T → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2.
+#h #g #G #L #T1 #T #l1 #l #HT1 #T2 #l2 #HT2
+@(scpes_trans … HT1) -T1 -l1 /2 width=1 by scpes_sym/ (**) (* full auto raises NTypeChecker failure *)
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/snv_preserve.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/snv_preserve.etc
index 5185215c6..578937f4c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/snv_preserve.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/snv_preserve.etc
@@ -1,9 +1,3 @@
-lemma snv_cprs_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
-                    ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, g].
-#h #g #G #L1 #T1 #HT1 #T2 #H
-@(cprs_ind … H) -T2 /3 width=5 by snv_cpr_lpr/
-qed-.
-
 lemma da_cprs_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
                    ∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l →
                    ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ▪[h, g] l.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/term_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/term_vector.ma
index b9cc288a6..9575612e0 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/term_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/term_vector.ma
@@ -13,22 +13,22 @@
 (**************************************************************************)
 
 include "ground_2/lib/list.ma".
-include "basic_2/notation/functions/snappls_2.ma".
+include "basic_2/notation/functions/snapplvector_2.ma".
 include "basic_2/grammar/term_simple.ma".
 
 (* TERMS ********************************************************************)
 
-let rec appls Vs T on Vs ≝
+let rec applv Vs T on Vs ≝
   match Vs with
   [ nil        ⇒ T
-  | cons hd tl ⇒ ⓐhd. (appls tl T)
+  | cons hd tl ⇒ ⓐhd. (applv tl T)
   ].
 
 interpretation "application to vector (term)"
-   'SnApplStar Vs T = (appls Vs T).
+   'SnApplVector Vs T = (applv Vs T).
 
 (* properties concerning simple terms ***************************************)
 
-lemma appls_simple: ∀T,Vs.  𝐒⦃T⦄ → 𝐒⦃ⒶVs.T⦄.
+lemma applv_simple: ∀T,Vs.  𝐒⦃T⦄ → 𝐒⦃ⒶVs.T⦄.
 #T * //
 qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/tstc_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/tstc_vector.ma
index 997a5c179..df30d65b8 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/tstc_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/tstc_vector.ma
@@ -20,7 +20,7 @@ include "basic_2/grammar/tstc.ma".
 (* Advanced inversion lemmas ************************************************)
 
 (* Basic_1: was only: iso_flats_lref_bind_false iso_flats_flat_bind_false *)
-lemma tstc_inv_bind_appls_simple: ∀a,I,Vs,V2,T1,T2. ⒶVs.T1 ≂ ⓑ{a,I} V2. T2 →
+lemma tstc_inv_bind_applv_simple: ∀a,I,Vs,V2,T1,T2. ⒶVs.T1 ≂ ⓑ{a,I} V2. T2 →
                                   𝐒⦃T1⦄ → ⊥.
 #a #I #Vs #V2 #T1 #T2 #H
 elim (tstc_inv_pair2 … H) -H #V0 #T0
diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_vector.ma
index 3cb26d890..d6878c0a1 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_vector.ma
@@ -30,7 +30,7 @@ interpretation "generic relocation (vector)"
 (* Basic inversion lemmas ***************************************************)
 
 (* Basic_1: was: lifts1_flat (left to right) *)
-lemma lifts_inv_appls1: ∀V1s,U1,T2,des. ⇧*[des] Ⓐ V1s. U1 ≡ T2 →
+lemma lifts_inv_applv1: ∀V1s,U1,T2,des. ⇧*[des] Ⓐ V1s. U1 ≡ T2 →
                         ∃∃V2s,U2. ⇧*[des] V1s ≡ V2s & ⇧*[des] U1 ≡ U2 &
                                   T2 = Ⓐ V2s. U2.
 #V1s elim V1s -V1s normalize
@@ -46,7 +46,7 @@ qed-.
 (* Basic properties *********************************************************)
 
 (* Basic_1: was: lifts1_flat (right to left) *)
-lemma lifts_appls: ∀V1s,V2s,des. ⇧*[des] V1s ≡ V2s →
+lemma lifts_applv: ∀V1s,V2s,des. ⇧*[des] V1s ≡ V2s →
                    ∀T1,T2. ⇧*[des] T1 ≡ T2 →
                    ⇧*[des] Ⓐ V1s. T1 ≡ Ⓐ V2s. T2.
 #V1s #V2s #des #H elim H -V1s -V2s /3 width=1 by lifts_flat/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snappls_2.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snappls_2.ma
deleted file mode 100644
index c8beab968..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snappls_2.ma
+++ /dev/null
@@ -1,19 +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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( Ⓐ term 55 T1 . break term 55 T )"
- non associative with precedence 55
- for @{ 'SnApplStar $T1 $T }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snapplvector_2.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snapplvector_2.ma
new file mode 100644
index 000000000..e59520265
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snapplvector_2.ma
@@ -0,0 +1,19 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( Ⓐ term 55 T1 . break term 55 T )"
+ non associative with precedence 55
+ for @{ 'SnApplVector $T1 $T }.
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 147978606..55e58114b 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
@@ -47,12 +47,12 @@ table {
         ]
 *)
         [ { "local env. ref. for stratified native validity" * } {
-             [ "lsubsv ( ? ⊢ ? ⫃¡[?,?] ? )" "lsubsv_lsuba" + "lsubsv_lsubd" + "lsubsv_lstas" + "lsubsv_cpds" + "lsubsv_cpcs" + "lsubsv_snv" * ]
+             [ "lsubsv ( ? ⊢ ? ⫃¡[?,?] ? )" "lsubsv_lsuba" + "lsubsv_lsubd" + "lsubsv_lstas" + "lsubsv_scpds" + "lsubsv_cpcs" + "lsubsv_snv" * ]
           }
         ]
         [ { "stratified native validity" * } {
-             [ "hsnv ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] )" "hsnv_aaa" * ]
-             [ "snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] )" "snv_lift" + "snv_aaa" + "snv_da_lpr" + "snv_lstas" + "snv_lstas_lpr" + "snv_lpr" + "snv_cpes" + "snv_preserve" * ]
+             [ "shnv ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] )" "shnv_aaa" * ]
+             [ "snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] )" "snv_lift" + "snv_aaa" + "snv_da_lpr" + "snv_lstas" + "snv_lstas_lpr" + "snv_lpr" + "snv_scpes" + "snv_preserve" * ]
           }
         ]
      }
@@ -60,7 +60,7 @@ table {
    class "blue"
    [ { "equivalence" * } {
         [ { "decomposed extended equivalence" * } {
-             [ "cpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? )" "cpes_aaa" + "cpes_cpcs" + "cpes_cpes" * ]
+             [ "scpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? )" "scpes_aaa" + "scpes_cpcs" + "scpes_scpes" * ]
           }
         ]
         [ { "context-sensitive equivalence" * } {
@@ -106,7 +106,7 @@ table {
           }
         ]
         [ { "decomposed extended computation" * } {
-             [ "cpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?,?] ? )" "cpds_lift" + "cpds_aaa" + "cpds_cpds" * ]
+             [ "scpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?,?] ? )" "scpds_lift" + "scpds_aaa" + "scpds_scpds" * ]
           }
         ]
         [ { "context-sensitive extended computation" * } {
@@ -309,7 +309,7 @@ table {
         [ { "internal syntax" * } {
              [ "genv" * ]
              [ "lenv" "lenv_weight ( ♯{?} )" "lenv_length ( |?| )" "lenv_append ( ? @@ ? )" * ]
-             [ "term" "term_weight ( ♯{?} )" "term_simple ( 𝐒⦃?⦄ )" "term_vector" * ]
+             [ "term" "term_weight ( ♯{?} )" "term_simple ( 𝐒⦃?⦄ )" "term_vector ( Ⓐ?.? )" * ]
              [ "item" * ]
           }
         ]