From 18bc3082b332504f60345245e716b62ae628e3a7 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 15 Feb 2013 14:17:58 +0000
Subject: [PATCH] we reformulate the extended computation to simplify the proof
 of its normalization property

---
 matita/matita/contribs/lambdadelta/Makefile   | 20 +++--
 .../lambdadelta/basic_2/computation/dxprs.ma  | 46 ++++++++++
 .../basic_2/computation/dxprs_aaa.ma          | 25 ++++++
 .../basic_2/computation/dxprs_dxprs.ma        | 33 ++++++++
 .../basic_2/computation/dxprs_lift.ma         | 52 ++++++++++++
 .../basic_2/computation/dxprs_lsubss.ma       | 26 ++++++
 .../lambdadelta/basic_2/dynamic/snv.ma        | 22 +++--
 .../lambdadelta/basic_2/dynamic/snv_aaa.ma    |  8 +-
 .../lambdadelta/basic_2/dynamic/snv_lift.ma   |  6 +-
 .../dynamic/{snv_ltpr.ma => snv_ltpr_1.ma}    | 48 +----------
 .../lambdadelta/basic_2/dynamic/snv_ltpr_2.ma | 67 +++++++++++++++
 .../lambdadelta/basic_2/etc/sstas/sstas.etc   |  4 -
 .../{reducibility/xpr.ma => etc/xpr/xpr.etc}  |  4 +
 .../xpr_aaa.ma => etc/xpr/xpr_aaa.etc}        |  0
 .../xpr_lift.ma => etc/xpr/xpr_lift.etc}      |  0
 .../xpr_lsubss.ma => etc/xpr/xpr_lsubss.etc}  |  0
 .../{computation/xprs.ma => etc/xpr/xprs.etc} |  8 ++
 .../xprs_aaa.ma => etc/xpr/xprs_aaa.etc}      |  0
 .../xprs_cprs.ma => etc/xpr/xprs_cprs.etc}    |  0
 .../xprs_lift.ma => etc/xpr/xprs_lift.etc}    |  0
 .../xpr/xprs_lsubss.etc}                      |  0
 .../xprs_xprs.ma => etc/xpr/xprs_xprs.etc}    |  0
 .../contribs/lambdadelta/basic_2/notation.ma  | 16 ++--
 .../lambdadelta/basic_2/static/ssta_aaa.ma    |  1 -
 .../lambdadelta/basic_2/unwind/sstas.ma       | 84 +++++++++++++++++++
 .../lambdadelta/basic_2/unwind/sstas_aaa.ma   | 25 ++++++
 .../lambdadelta/basic_2/unwind/sstas_lift.ma  | 53 ++++++++++++
 .../basic_2/unwind/sstas_lsubss.ma            | 30 +++++++
 .../basic_2/unwind/sstas_ltpss_dx.ma          | 55 ++++++++++++
 .../basic_2/unwind/sstas_ltpss_sn.ma          | 53 ++++++++++++
 .../lambdadelta/basic_2/unwind/sstas_sstas.ma | 52 ++++++++++++
 31 files changed, 659 insertions(+), 79 deletions(-)
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/dxprs.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_aaa.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_dxprs.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_lift.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_lsubss.ma
 rename matita/matita/contribs/lambdadelta/basic_2/dynamic/{snv_ltpr.ma => snv_ltpr_1.ma} (74%)
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr_2.ma
 rename matita/matita/contribs/lambdadelta/basic_2/{reducibility/xpr.ma => etc/xpr/xpr.etc} (88%)
 rename matita/matita/contribs/lambdadelta/basic_2/{reducibility/xpr_aaa.ma => etc/xpr/xpr_aaa.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{reducibility/xpr_lift.ma => etc/xpr/xpr_lift.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{reducibility/xpr_lsubss.ma => etc/xpr/xpr_lsubss.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{computation/xprs.ma => etc/xpr/xprs.etc} (88%)
 rename matita/matita/contribs/lambdadelta/basic_2/{computation/xprs_aaa.ma => etc/xpr/xprs_aaa.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{computation/xprs_cprs.ma => etc/xpr/xprs_cprs.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{computation/xprs_lift.ma => etc/xpr/xprs_lift.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{computation/xprs_lsubss.ma => etc/xpr/xprs_lsubss.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{computation/xprs_xprs.ma => etc/xpr/xprs_xprs.etc} (100%)
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/unwind/sstas.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_aaa.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_lift.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_lsubss.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_ltpss_dx.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_ltpss_sn.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_sstas.ma

diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile
index 5b8fd2863..69fca343b 100644
--- a/matita/matita/contribs/lambdadelta/Makefile
+++ b/matita/matita/contribs/lambdadelta/Makefile
@@ -74,39 +74,41 @@ define STATS_TEMPLATE
 
 $$(STT_$(1)):
 	@printf '\x1B[1;40;37m'
-	@printf '%-15s %-43s' 'Statistics for:' $(1)
+	@printf '%-15s %-44s' 'Statistics for:' $(1)
 	@printf '\x1B[0m\n'
 	@printf '\x1B[1;40;35m'
 	@printf '%-8s %6i' Chars $$(S1)
-	@printf '   %-8s %3i' Pages $$(S2)
+	@printf '   %-8s %4i' Pages $$(S2)
 	@printf '   %-26s' ''
 	@printf '\x1B[0m\n'
 	@printf '\x1B[1;40;36m'
 	@printf '%-8s %6i' Files $$(S4)
-	@printf '   %-8s %3i' Sources $$(word 1, $$(S5))	
+	@printf '   %-8s %4i' Sources $$(word 1, $$(S5))	
 	@printf '   %-7s %4i' Objects $$(word 2, $$(S5))
 	@printf '   %-11s' ''
 	@printf '\x1B[0m\n'	
 	@printf '\x1B[1;40;32m'
 	@printf '%-8s %6i' Theorems $$(P1)
-	@printf '   %-8s %3i' Lemmas $$(P2)
+	@printf '   %-8s %4i' Lemmas $$(P2)
 	@printf '   %-7s %4i' Facts $$(P3)
 	@printf '   %-6s %4i' Proofs $$(P4)
 	@printf '\x1B[0m\n'	
 	@printf '\x1B[1;40;33m'
 	@printf '%-8s %6i' Declared $$(C1)
-	@printf '   %-8s %3i' Defined $$(C2)	
+	@printf '   %-8s %4i' Defined $$(C2)	
 	@printf '   %-26s' ''
 	@printf '\x1B[0m\n'
 	@printf '\x1B[1;40;31m'
 	@printf '%-8s %6i' Axioms $$(M1)
-	@printf '   %-8s %3i' Comments $$(M2)
+	@printf '   %-8s %4i' Comments $$(M2)
 	@printf '   %-7s %4i' Marks $$(M3)
 	@printf '   %-11s' ''
 	@printf '\x1B[0m\n'
 endef
 
-$(foreach PKG, $(PACKAGES), $(eval $(call STATS_TEMPLATE,$(PKG))))
+ifeq ($(MAKECMDGOALS), stats)
+   $(foreach PKG, $(PACKAGES), $(eval $(call STATS_TEMPLATE,$(PKG))))
+endif
 
 stats: $(STTS)
 
@@ -154,6 +156,8 @@ define SUMMARY_TEMPLATE
 	@printf 'class "number" { 2 } { 4 } { 6 }\n\n' >> $$@
 endef
 
-$(foreach PKG, $(PACKAGES), $(eval $(call SUMMARY_TEMPLATE,$(PKG))))
+ifeq ($(MAKECMDGOALS), tbls)
+   $(foreach PKG, $(PACKAGES), $(eval $(call SUMMARY_TEMPLATE,$(PKG))))
+endif
 
 tbls: $(TBLS)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs.ma
new file mode 100644
index 000000000..1db0aec2b
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs.ma
@@ -0,0 +1,46 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/unwind/sstas.ma".
+include "basic_2/computation/cprs.ma".
+
+(* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************)
+
+definition dxprs: ∀h. sd h → lenv → relation term ≝ λh,g,L,T1,T2.
+                  ∃∃T. ⦃h, L⦄ ⊢ T1 •*[g] T & L ⊢ T ➡* T2.
+
+interpretation "decomposed extended parallel computation (term)"
+   'DecomposedXPRedStar h g L T1 T2 = (dxprs h g L T1 T2).
+
+(* Basic properties *********************************************************)
+
+lemma dxprs_refl: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → ⦃h, L⦄ ⊢ T •*➡*[g] T.
+/3 width=3/ qed.
+
+lemma sstas_dxprs: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 •*[g] T2 → ⦃h, L⦄ ⊢ T1 •*➡*[g] T2.
+/2 width=3/ qed.
+
+lemma cprs_dxprs: ∀h,g,L,T1,T2,U,l. ⦃h, L⦄ ⊢ T1 •[g, l] U → L ⊢ T1 ➡* T2 →
+                  ⦃h, L⦄ ⊢ T1 •*➡*[g] T2.
+/3 width=3/ qed.
+
+lemma dxprs_strap1: ∀h,g,L,T1,T,T2.
+                    ⦃h, L⦄ ⊢ T1 •*➡*[g] T → L ⊢ T ➡ T2 → ⦃h, L⦄ ⊢ T1 •*➡*[g] T2.
+#h #g #L #T1 #T #T2 * /3 width=5/
+qed.
+
+lemma dxprs_strap2: ∀h,g,L,T1,T,T2,l.
+                    ⦃h, L⦄ ⊢ T1 •[g, l+1] T → ⦃h, L⦄ ⊢ T •*➡*[g] T2 → ⦃h, L⦄ ⊢ T1 •*➡*[g] T2.
+#h #g #L #T1 #T #T2 #l #HT1 * /3 width=4/
+qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_aaa.ma
new file mode 100644
index 000000000..57c72a7b0
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_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/unwind/sstas_aaa.ma".
+include "basic_2/computation/cprs_aaa.ma".
+include "basic_2/computation/dxprs.ma".
+
+(* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************)
+
+(* Properties on atomic arity assignment for terms **************************)
+
+lemma dxprs_aaa: ∀h,g,L,T,A. L ⊢ T ⁝ A → ∀U. ⦃h, L⦄ ⊢ T •*➡*[g] U → L ⊢ U ⁝ A.
+#h #g #L #T #A #HT #U * /3 width=5/
+qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_dxprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_dxprs.ma
new file mode 100644
index 000000000..772cbd94a
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_dxprs.ma
@@ -0,0 +1,33 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/unwind/sstas_sstas.ma".
+include "basic_2/computation/cprs_cprs.ma".
+include "basic_2/computation/dxprs.ma".
+
+(* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************)
+
+(* Advanced properties ******************************************************)
+
+lemma dxprs_cprs_trans: ∀h,g,L,T1,T,T2.
+                   ⦃h, L⦄ ⊢ T1 •*➡*[g] T → L ⊢ T ➡* T2 → ⦃h, L⦄ ⊢ T1 •*➡*[g] T2.
+#h #g #L #T1 #T #T2 * #T0 #HT10 #HT0 #HT2
+lapply (cprs_trans … HT0 … HT2) -T /2 width=3/
+qed-.
+
+lemma sstas_dxprs_trans: ∀h,g,L,T1,T,T2.
+                         ⦃h, L⦄ ⊢ T1 •*[g] T → ⦃h, L⦄ ⊢ T •*➡*[g] T2 → ⦃h, L⦄ ⊢ T1 •*➡*[g] T2.
+#h #g #L #T1 #T #T2 #HT1 * #T0 #HT0 #HT02
+lapply (sstas_trans … HT1 … HT0) -T /2 width=3/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_lift.ma
new file mode 100644
index 000000000..431a9f511
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_lift.ma
@@ -0,0 +1,52 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/unwind/sstas_lift.ma".
+include "basic_2/computation/cprs_lift.ma".
+include "basic_2/computation/dxprs.ma".
+
+(* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************)
+
+(* Advanced inversion lemmas *************************************************)
+
+lemma dxprs_inv_abst1: ∀h,g,a,L,V1,T1,U2. ⦃h, L⦄ ⊢ ⓛ{a}V1. T1 •*➡*[g] U2 →
+                       ∃∃V2,T2. L ⊢ V1 ➡* V2 & ⦃h, L.ⓛV1⦄ ⊢ T1 •*➡*[g] T2 &
+                                U2 = ⓛ{a}V2. T2.
+#h #g #a #L #V1 #T1 #U2 * #X #H1 #H2
+elim (sstas_inv_bind1 … H1) -H1 #U #HTU1 #H destruct
+elim (cprs_inv_abst1 Abst V1 … H2) -H2 #V2 #T2 #HV12 #HUT2 #H destruct /3 width=5/
+qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma ssta_cprs_dxprs: ∀h,g,L,T1,T,T2,l. ⦃h, L⦄ ⊢ T1 •[g, l+1] T → 
+                       L ⊢ T ➡* T2 → ⦃h, L⦄ ⊢ T1 •*➡*[g] T2.
+/3 width=3/ qed.
+
+(* Relocation properties ****************************************************)
+
+lemma dxprs_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K → ∀T1,U1. ⇧[d, e] T1 ≡ U1 →
+                  ∀h,g,T2. ⦃h, K⦄ ⊢ T1 •*➡*[g] T2 → ∀U2. ⇧[d, e] T2 ≡ U2 →
+                  ⦃h, L⦄ ⊢ U1 •*➡*[g] U2.
+#L #K #d #e #HLK #T1 #U1 #HTU1 #h #g #T2 * #T
+elim (lift_total T d e) /3 width=11/
+qed.
+
+lemma dxprs_inv_lift1: ∀L,K,d,e. ⇩[d, e] L ≡ K →
+                       ∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀h,g,U2. ⦃h, L⦄ ⊢ U1 •*➡*[g] U2 →
+                       ∃∃T2. ⇧[d, e] T2 ≡ U2 & ⦃h, K⦄ ⊢ T1 •*➡*[g] T2.
+#L #K #d #e #HLK #T1 #U1 #HTU1 #h #g #U2 * #U #HU1 #HU2
+elim (sstas_inv_lift1 … HU1 … HLK … HTU1) -U1 #T #HT1 #HTU
+elim (cprs_inv_lift1 … HLK … HTU … HU2) -U -L /3 width=5/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_lsubss.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_lsubss.ma
new file mode 100644
index 000000000..a9a5cd84e
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_lsubss.ma
@@ -0,0 +1,26 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/unwind/sstas_lsubss.ma".
+include "basic_2/computation/dxprs.ma".
+
+(* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************)
+
+(* Properties on lenv ref for stratified type assignment ********************)
+
+lemma lsubss_dxprs_trans: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 →
+                          ∀T1,T2. ⦃h, L2⦄ ⊢ T1 •*➡*[g] T2 → ⦃h, L1⦄ ⊢ T1 •*➡*[g] T2.
+#h #g #L1 #L2 #HL12 #T1 #T2 *
+lapply (lsubss_fwd_lsubs2 … HL12) /4 width=5/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma
index 2be571525..e39a5764a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma
@@ -12,8 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/computation/cprs.ma".
-include "basic_2/computation/xprs.ma".
+include "basic_2/computation/dxprs.ma".
 include "basic_2/equivalence/cpcs.ma".
 
 (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
@@ -24,7 +23,7 @@ inductive snv (h:sh) (g:sd h): lenv → predicate term ≝
 | snv_bind: ∀a,I,L,V,T. snv h g L V → snv h g (L.ⓑ{I}V) T → snv h g L (ⓑ{a,I}V.T)
 | snv_appl: ∀a,L,V,W,W0,T,U,l. snv h g L V → snv h g L T →
             ⦃h, L⦄ ⊢ V •[g, l + 1] W → L ⊢ W ➡* W0 →
-            ⦃h, L⦄ ⊢ T •➡*[g] ⓛ{a}W0.U → snv h g L (ⓐV.T)
+            ⦃h, L⦄ ⊢ T •*➡*[g] ⓛ{a}W0.U → snv h g L (ⓐV.T)
 | snv_cast: ∀L,W,T,U,l. snv h g L W → snv h g L T →
             ⦃h, L⦄ ⊢ T •[g, l + 1] U → L ⊢ U ⬌* W → snv h g L (ⓝW.T)
 .
@@ -49,6 +48,19 @@ lemma snv_inv_lref: ∀h,g,L,i. ⦃h, L⦄ ⊩ #i :[g] →
                     ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V & ⦃h, K⦄ ⊩ V :[g].
 /2 width=3/ qed-.
 
+fact snv_inv_gref_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀p. X = §p → ⊥.
+#h #g #L #X * -L -X
+[ #L #k #p #H destruct
+| #I #L #K #V #i #_ #_ #p #H destruct
+| #a #I #L #V #T #_ #_ #p #H destruct
+| #a #L #V #W #W0 #T #U #l #_ #_ #_ #_ #_ #p #H destruct
+| #L #W #T #U #l #_ #_ #_ #_ #p #H destruct
+]
+qed.
+
+lemma snv_inv_gref: ∀h,g,L,p. ⦃h, L⦄ ⊩ §p :[g] → ⊥.
+/2 width=7/ qed-.
+
 fact snv_inv_bind_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀a,I,V,T. X = ⓑ{a,I}V.T →
                        ⦃h, L⦄ ⊩ V :[g] ∧ ⦃h, L.ⓑ{I}V⦄ ⊩ T :[g].
 #h #g #L #X * -L -X
@@ -67,7 +79,7 @@ lemma snv_inv_bind: ∀h,g,a,I,L,V,T. ⦃h, L⦄ ⊩ ⓑ{a,I}V.T :[g] →
 fact snv_inv_appl_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀V,T. X = ⓐV.T →
                        ∃∃a,W,W0,U,l. ⦃h, L⦄ ⊩ V :[g] & ⦃h, L⦄ ⊩ T :[g] &
                                    ⦃h, L⦄ ⊢ V •[g, l + 1] W & L ⊢ W ➡* W0 &
-                                   ⦃h, L⦄ ⊢ T •➡*[g] ⓛ{a}W0.U.
+                                   ⦃h, L⦄ ⊢ T •*➡*[g] ⓛ{a}W0.U.
 #h #g #L #X * -L -X
 [ #L #k #V #T #H destruct
 | #I #L #K #V0 #i #_ #_ #V #T #H destruct
@@ -80,7 +92,7 @@ qed.
 lemma snv_inv_appl: ∀h,g,L,V,T. ⦃h, L⦄ ⊩ ⓐV.T :[g] →
                     ∃∃a,W,W0,U,l. ⦃h, L⦄ ⊩ V :[g] & ⦃h, L⦄ ⊩ T :[g] &
                                 ⦃h, L⦄ ⊢ V •[g, l + 1] W & L ⊢ W ➡* W0 &
-                                ⦃h, L⦄ ⊢ T •➡*[g] ⓛ{a}W0.U.
+                                ⦃h, L⦄ ⊢ T •*➡*[g] ⓛ{a}W0.U.
 /2 width=3/ qed-.
 
 fact snv_inv_cast_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀W,T. X = ⓝW.T →
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 3d4761da8..3ebe6e485 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma
@@ -13,8 +13,8 @@
 (**************************************************************************)
 
 include "basic_2/computation/csn_aaa.ma".
-include "basic_2/computation/xprs_aaa.ma".
-include "basic_2/computation/xprs_cprs.ma".
+include "basic_2/computation/dxprs_lift.ma".
+include "basic_2/computation/dxprs_aaa.ma".
 include "basic_2/equivalence/cpcs_aaa.ma".
 include "basic_2/dynamic/snv.ma".
 
@@ -28,8 +28,8 @@ lemma snv_aaa: ∀h,g,L,T. ⦃h, L⦄ ⊩ T :[g] → ∃A. L ⊢ T ⁝ A.
 | #I #L #K #V #i #HLK #_ * /3 width=6/
 | #a * #L #V #T #_ #_ * #B #HV * #A #HA /3 width=2/
 | #a #L #V #W #W0 #T #U #l #_ #_ #HVW #HW0 #HTU * #B #HV * #X #HT
-  lapply (xprs_aaa h g … HV W0 ?) [ /3 width=3/ ] -W #HW0
-  lapply (xprs_aaa … HT … HTU) -HTU #H
+  lapply (dxprs_aaa h g … HV W0 ?) [ -HTU /2 width=4/ ] -W #HW0 (**) (* auto fail without -HTU *)
+  lapply (dxprs_aaa … HT … HTU) -HTU #H
   elim (aaa_inv_abst … H) -H #B0 #A #H1 #HU #H2 destruct
   lapply (aaa_mono … H1 … HW0) -W0 #H destruct /3 width=4/
 | #L #W #T #U #l #_ #_ #HTU #HUW * #B #HW * #A #HT
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 6d79ef571..ec9be23a4 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/computation/xprs_lift.ma".
+include "basic_2/computation/dxprs_lift.ma".
 include "basic_2/equivalence/cpcs_cpcs.ma".
 include "basic_2/dynamic/snv.ma".
 
@@ -42,7 +42,7 @@ lemma snv_lift: ∀h,g,K,T. ⦃h, K⦄ ⊩ T :[g] → ∀L,d,e. ⇩[d, e] L ≡
   elim (lift_total T1 (d+1) e) #U1 #HTU1
   @(snv_appl … a … W0 … W1 … U1 l)
   [ /2 width=4/ | /2 width=4/ | /2 width=9/ | /2 width=9/ ]
-  @(xprs_lift … HLK … HTU … HT1) /2 width=1/
+  @(dxprs_lift … HLK … HTU … HT1) /2 width=1/
 | #K #V0 #T #V #l #_ #_ #HTV #HV0 #IHV0 #IHT #L #d #e #HLK #X #H
   elim (lift_inv_flat1 … H) -H #W0 #U #HVW0 #HTU #H destruct
   elim (lift_total V d e) #W #HVW
@@ -68,7 +68,7 @@ lemma snv_inv_lift: ∀h,g,L,U. ⦃h, L⦄ ⊩ U :[g] → ∀K,d,e. ⇩[d, e] L
   elim (lift_inv_flat2 … H) -H #V #T #HVW #HTU #H destruct
   elim (ssta_inv_lift1 … HW0 … HLK … HVW) -HW0 #V0 #HV0 #HVW0
   elim (cprs_inv_lift1 … HLK … HVW0 … HW01) -W0 #V1 #HVW1 #HV01
-  elim (xprs_inv_lift1 … HLK … HTU … HU1) -HU1 #X #H #HTU
+  elim (dxprs_inv_lift1 … HLK … HTU … HU1) -HU1 #X #H #HTU
   elim (lift_inv_bind2 … H) -H #Y #T1 #HY #HTU1 #H destruct
   lapply (lift_inj … HY … HVW1) -HY #H destruct /3 width=8/
 | #L #W0 #U #W #l #_ #_ #HUW #HW0 #IHW0 #IHU #K #d #e #HLK #X #H
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr_1.ma
similarity index 74%
rename from matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma
rename to matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr_1.ma
index cb7e54413..4beecd835 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr_1.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/static/ssta_ltpss_dx.ma".
-include "basic_2/computation/xprs_lift.ma".
+include "basic_2/computation/dxprs_lift.ma".
 include "basic_2/equivalence/lsubse_ssta.ma".
 include "basic_2/equivalence/fpcs_cpcs.ma".
 include "basic_2/equivalence/lfpcs_fpcs.ma".
@@ -97,7 +97,7 @@ fact ssta_ltpr_tpr_aux: ∀h,g,n. (
   | #b #V2 #W #T2 #T20 #HV12 #HT20 #H1 #H2 destruct
     elim (snv_inv_bind … HT1) -HT1 #HW #HT2
     elim (ssta_inv_bind1 … HTU1) -HTU1 #U2 #HTU2 #H destruct
-    elim (xprs_fwd_abst1 … HTU10) -HTU10 #W0 #U0 #HW0 #H destruct
+    elim (dxprs_inv_abst1 … HTU10) -HTU10 #W0 #U0 #HW0 #_ #H destruct
     lapply (cprs_div … HW10 … HW0) -W0 #HW1
     elim (ssta_fwd_correct … HVW1) <minus_plus_m_m #X1 #HWX1
     elim (snv_ssta … HW) #V #l1 #HWV
@@ -134,47 +134,3 @@ fact ssta_ltpr_tpr_aux: ∀h,g,n. (
   ]
 ]
 qed-.
-(*  
-fact snv_ltpr_tpr_aux: ∀h,g,L,T. (
-                          ∀L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 →
-                          ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → ⦃h, L1⦄ ⊩ T1 :[g] →
-                          h ⊢ ⦃L, T⦄ •⭃*[g] ⦃L1 ,T1⦄ →
-                          ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & ⦃L1, U1⦄ ⬌* ⦃L2, U2⦄
-                       ) → (
-                          ∀L1,T1. ⦃h, L1⦄ ⊩ T1 :[g] →
-                          ∀L2. L1 ➡ L2 → ∀T2. ⦃h, L2⦄ ⊢ T1 •➡*[g] T2 →
-                          h ⊢ ⦃L, T⦄ •⭃*[g] ⦃L1 ,T1⦄ → ⦃h, L2⦄ ⊩ T2 :[g]
-                       ) →
-                       ∀L1,T1. ⦃h, L1⦄ ⊩ T1 :[g] →
-                       ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 →
-                       L = L1 → T = T1 → ⦃h, L2⦄ ⊩ T2 :[g].
-#h #g #L #T #IH2 #IH1 #L1 #T1 * -L1 -T1
-[ #L1 #k #L2 #_ #X #H #H1 #H2 destruct -IH2 -IH1 -L1
-  >(tpr_inv_atom1 … H) -X //
-| #I #L1 #K1 #V1 #i #HLK1 #HV1 #L2 #HL12 #X #H #H1 #H2 destruct -IH2
-  >(tpr_inv_atom1 … H) -X
-  elim (ltpr_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2
-  elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct
-  lapply (IH1 … HV1 … HK12 V2 ? ?) -IH1 -HV1 -HK12 /4 width=1/ -HV12 /3 width=4/ -HLK1 /3 width=5/
-| #a #I #L1 #V1 #T1 #HV1 #HT1 #L2 #HL12 #X #H #H1 #H2 destruct -IH2
-  elim (tpr_inv_bind1 … H) -H *
-  [ #V2 #T0 #T2 #HV12 #HT10 #HT02 #H destruct
-    lapply (tps_lsubs_trans … HT02 (L2.ⓑ{I}V2) ?) -HT02 /2 width=1/ #HT02
-    lapply (cpr_intro (L2.ⓑ{I}V2) … T2 0 1 HT10 ?) -HT10 /2 width=1/ -HT02 #HT12
-    lapply (IH1 … HV1 … HL12 V2 ? ?) -HV1 /4 width=1/ #HV2
-    lapply (IH1 … HT1 (L2.ⓑ{I}V2) … T2 ? ?) -IH1 -HT1 /3 width=1/
-  | #T2 #HT12 #HXT2 #H1 #H2 destruct
-    lapply (IH1 … HT1 (L2.ⓓV1) ? T2 ? ?) -IH1 -HT1 /4 width=1/ -HT12 -HL12 #HT2
-    lapply (snv_inv_lift … HT2 L2 … HXT2) -T2 // /2 width=1/
-  ]
-| #a #L1 #V1 #W1 #W10 #T1 #U1 #l #HV1 #HT1 #HVW1 #HW10 #HTU1 #L2 #HL12 #X #H #H1 #H2 destruct
-  elim (tpr_inv_appl1 … H) -H *
-  [ #V2 #T2 #HV12 #HT12 #H destruct
-    lapply (IH1 … HV1 … HL12 V2 ? ?) /4 width=1/ #HV2
-    lapply (IH1 … HT1 … HL12 T2 ? ?) /4 width=1/ #HT2
-    lapply (IH1 … HT1 … HTU1 ?) -IH1 -HT1 // /2 width=1/ #H
-    elim (snv_inv_bind … H) -H #HW10 #HU1
-    elim (IH2 … HVW1 … HL12 … HV12 HV1 ?) -IH2 -HVW1 -HL12 -HV12 -HV1 /2 width=1/ #W2 #HVW2 #HW12
-    lapply (fpcs_canc_sn L1 L1 … W10 … HW12) -HW12 /3 width=1/ -W1 #HW102
-    @(snv_appl … HV2 HT2 HVW2)
-*)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr_2.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr_2.ma
new file mode 100644
index 000000000..3a722d9dd
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr_2.ma
@@ -0,0 +1,67 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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_ltpr_1.ma".
+include "basic_2/dynamic/snv_lift.ma".
+
+(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
+
+(* Properties on context-free parallel reduction for local environments *****)
+
+fact snv_ltpr_tpr_aux: ∀h,g,n. (
+                          ∀L1,T1. ♯{L1, T1} < n →
+                          ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 →
+                          ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → ⦃h, L1⦄ ⊩ T1 :[g] →
+                          ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & ⦃L1, U1⦄ ⬌* ⦃L2, U2⦄
+                       ) → (
+                          ∀L1,T1. ♯{L1, T1} < n → ⦃h, L1⦄ ⊩ T1 :[g] →
+                          ∀L2. L1 ➡ L2 → ∀T2. ⦃h, L2⦄ ⊢ T1 •*➡*[g] T2 → ⦃h, L2⦄ ⊩ T2 :[g]
+                       ) →
+                       ∀L1,T1. ♯{L1, T1} = n → ⦃h, L1⦄ ⊩ T1 :[g] →
+                       ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → ⦃h, L2⦄ ⊩ T2 :[g].
+#h #g #n #IH2 #IH1 #L1 * * [||||*]
+[ #k #Hn #H1 #L2 #_ #X #H2 destruct -IH2 -IH1 -L1
+  >(tpr_inv_atom1 … H2) -X //
+| #i #Hn #H1 #L2 #HL12 #X #H2 destruct -IH2
+  elim (snv_inv_lref … H1) -H1 #I #K1 #V1 #HLK1 #HV1
+  >(tpr_inv_atom1 … H2) -X
+  elim (ltpr_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2
+  elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct
+  lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) -HLK1 #HLK1
+  lapply (IH1 … HV1 … HK12 V2 ?) -IH1 -HV1 -HK12 // -L1 -K1 /4 width=1/ -HV12 /2 width=5/
+| #p #Hn #H1 #L2 #HL12 #X #H2 destruct -IH2
+  elim (snv_inv_gref … H1)
+| #a #I #V1 #T1 #Hn #H1 #L2 #HL12 #X #H2 destruct -IH2
+  elim (snv_inv_bind … H1) -H1 #HV1 #HT1
+  elim (tpr_inv_bind1 … H2) -H2 *
+  [ #V2 #T0 #T2 #HV12 #HT10 #HT02 #H destruct
+    lapply (tps_lsubs_trans … HT02 (L2.ⓑ{I}V2) ?) -HT02 /2 width=1/ #HT02
+    lapply (cpr_intro (L2.ⓑ{I}V2) … T2 0 1 HT10 ?) -HT10 /2 width=1/ -HT02 #HT12
+    lapply (IH1 … HV1 … HL12 V2 ?) -HV1 // /4 width=1/ #HV2
+    lapply (IH1 … HT1 (L2.ⓑ{I}V2) … T2 ?) -IH1 -HT1 /3 width=1/
+  | #T2 #HT12 #HXT2 #H1 #H2 destruct
+    lapply (IH1 … HT1 (L2.ⓓV1) … T2 ?) -IH1 -HT1 // /4 width=1/ -HT12 -HL12 #HT2
+    lapply (snv_inv_lift … HT2 L2 … HXT2) -T2 // /2 width=1/
+  ]
+| #V1 #T1 #Hn #H1 #L2 #HL12 #X #H2 destruct
+  elim (snv_inv_appl … H1) -H1 #a #W10 #W1 #U1 #l #HV1 #HT1 #HVW1 #HW10 #HTU1
+  elim (tpr_inv_appl1 … H2) -H2 *
+  [ #V2 #T2 #HV12 #HT12 #H destruct
+    lapply (IH1 … HV1 … HL12 V2 ?) // /4 width=1/ #HV2
+    lapply (IH1 … HT1 … HL12 T2 ?) // /4 width=1/ #HT2
+    lapply (IH1 … HT1 … HTU1) -IH1 // #H
+    elim (snv_inv_bind … H) -H #HW1 #HU1
+    elim (IH2 … HVW1 … HL12 … HV12 HV1) -IH2 -HVW1 -HV12 -HV1 // #W2 #HVW2 #HW12
+    lapply (fpcs_canc_sn L1 L1 … W10 W1 … HW12) -HW12 /3 width=1/ -W10 #HW12
+    @(snv_appl … HV2 HT2 HVW2)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/sstas/sstas.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/sstas/sstas.etc
index 5954145d9..37d8cdb68 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/sstas/sstas.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/sstas/sstas.etc
@@ -12,10 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 •* break [ g ] break term 46 T2 )"
-   non associative with precedence 45
-   for @{ 'StaticTypeStar $h $g $L $T1 $T2 }.
-
 include "basic_2/static/ssta.ma".
 
 (* ITERATED STRATIFIED STATIC TYPE ASSIGNMENTON TERMS ***********************)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/xpr.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xpr.etc
similarity index 88%
rename from matita/matita/contribs/lambdadelta/basic_2/reducibility/xpr.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xpr.etc
index 7375349ef..1e17654ca 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/xpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xpr.etc
@@ -12,6 +12,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
+notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 • ➡ break [ term 46 g ] break term 46 T2 )"
+   non associative with precedence 45
+   for @{ 'XPRed $h $g $L $T1 $T2 }.
+
 include "basic_2/static/ssta.ma".
 include "basic_2/reducibility/cpr.ma".
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/xpr_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xpr_aaa.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/reducibility/xpr_aaa.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xpr_aaa.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/xpr_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xpr_lift.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/reducibility/xpr_lift.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xpr_lift.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/xpr_lsubss.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xpr_lsubss.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/reducibility/xpr_lsubss.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xpr_lsubss.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/xprs.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xprs.etc
similarity index 88%
rename from matita/matita/contribs/lambdadelta/basic_2/computation/xprs.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xprs.etc
index 854c5da27..bffc4e735 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/xprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xprs.etc
@@ -12,6 +12,14 @@
 (*                                                                        *)
 (**************************************************************************)
 
+notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 • ➡ * break [ term 46 g ] break term 46 T2 )"
+   non associative with precedence 45
+   for @{ 'XPRedStar $h $g $L $T1 $T2 }.
+
+notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ • ⬊ * break [ term 46 g ] break term 46 T2 )"
+   non associative with precedence 45
+   for @{ 'XSN $h $g $L $T }.
+
 include "basic_2/static/lsubss.ma".
 include "basic_2/reducibility/xpr.ma".
 (*
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/xprs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xprs_aaa.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/computation/xprs_aaa.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xprs_aaa.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/xprs_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xprs_cprs.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/computation/xprs_cprs.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xprs_cprs.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/xprs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xprs_lift.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/computation/xprs_lift.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xprs_lift.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/xprs_lsubss.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xprs_lsubss.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/computation/xprs_lsubss.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xprs_lsubss.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/xprs_xprs.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xprs_xprs.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/computation/xprs_xprs.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xprs_xprs.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation.ma b/matita/matita/contribs/lambdadelta/basic_2/notation.ma
index e378dc719..71e9fae60 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation.ma
@@ -264,6 +264,10 @@ notation "hvbox( h ⊢ break term 46 L1 • ⊑ [ term 46 g ] break term 46 L2 )
 
 (* Unwind *******************************************************************)
 
+notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 •* break [ term 46 g ] break term 46 T2 )"
+   non associative with precedence 45
+   for @{ 'StaticTypeStar $h $g $L $T1 $T2 }.
+
 notation "hvbox( L1 ⊢ ⧫ * break term 46 T ≡ break term 46 L2 )"
    non associative with precedence 45
    for @{ 'Unwind $L1 $T $L2 }.
@@ -336,10 +340,6 @@ notation "hvbox( ⦃ term 46 L1 ⦄ ➡ ➡ break ⦃ term 46 L2 ⦄ )"
    non associative with precedence 45
    for @{ 'FocalizedPRedAlt $L1 $L2 }.
 
-notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 • ➡ break [ term 46 g ] break term 46 T2 )"
-   non associative with precedence 45
-   for @{ 'XPRed $h $g $L $T1 $T2 }.
-
 (* Computation **************************************************************)
 
 notation "hvbox( T1 ➡ * break term 46 T2 )"
@@ -394,13 +394,13 @@ notation "hvbox( T1 ⊑ break [ term 46 R ] break term 46 T2 )"
    non associative with precedence 45
    for @{ 'CrSubEq $T1 $R $T2 }.
 
-notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 • ➡ * break [ term 46 g ] break term 46 T2 )"
+notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 • * ➡ * break [ term 46 g ] break term 46 T2 )"
    non associative with precedence 45
-   for @{ 'XPRedStar $h $g $L $T1 $T2 }.
+   for @{ 'DecomposedXPRedStar $h $g $L $T1 $T2 }.
 
-notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ • ⬊ * break [ term 46 g ] break term 46 T2 )"
+notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ • * ⬊ * break [ term 46 g ] break term 46 T2 )"
    non associative with precedence 45
-   for @{ 'XSN $h $g $L $T }.
+   for @{ 'DecomposedXSN $h $g $L $T }.
 
 (* Conversion ***************************************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_aaa.ma
index d14083a45..01841483c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_aaa.ma
@@ -38,4 +38,3 @@ lemma ssta_aaa: ∀h,g,L,T,A. L ⊢ T ⁝ A → ∀U,l. ⦃h, L⦄ ⊢ T •[g,
   lapply (ssta_inv_cast1 … H) -H /2 width=2/
 ]
 qed.
-
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas.ma b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas.ma
new file mode 100644
index 000000000..3928e49cc
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas.ma
@@ -0,0 +1,84 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/ssta.ma".
+
+(* ITERATED STRATIFIED STATIC TYPE ASSIGNMENT FOR TERMS *********************)
+
+inductive sstas (h:sh) (g:sd h) (L:lenv): relation term ≝
+| sstas_refl: ∀T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → sstas h g L T T
+| sstas_step: ∀T,U1,U2,l. ⦃h, L⦄ ⊢ T •[g, l+1] U1 → sstas h g L U1 U2 →
+              sstas h g L T U2.
+
+interpretation "iterated stratified static type assignment (term)"
+   'StaticTypeStar h g L T U = (sstas h g L T U).
+
+(* Basic eliminators ********************************************************)
+
+fact sstas_ind_alt_aux: ∀h,g,L,U2. ∀R:predicate term.
+                        (∀T,l. ⦃h, L⦄ ⊢ U2 •[g , l] T → R U2) →
+                        (∀T,U1,l. ⦃h, L⦄ ⊢ T •[g, l + 1] U1 →
+                                  ⦃h, L⦄ ⊢ U1 •* [g] U2 → R U1 → R T
+                        ) →
+                        ∀T,U. ⦃h, L⦄ ⊢ T •*[g] U → U = U2 → R T.
+#h #g #L #U2 #R #H1 #H2 #T #U #H elim H -H -T -U /2 width=3/ /3 width=5/
+qed-.
+
+lemma sstas_ind_alt: ∀h,g,L,U2. ∀R:predicate term.
+                     (∀T,l. ⦃h, L⦄ ⊢ U2 •[g , l] T → R U2) →
+                     (∀T,U1,l. ⦃h, L⦄ ⊢ T •[g, l + 1] U1 →
+                               ⦃h, L⦄ ⊢ U1 •* [g] U2 → R U1 → R T
+                     ) →
+                     ∀T. ⦃h, L⦄ ⊢ T •*[g] U2 → R T.
+/3 width=9 by sstas_ind_alt_aux/ qed-.
+                         
+(* Basic inversion lemmas ***************************************************)
+
+fact sstas_inv_bind1_aux: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U →
+                          ∀a,J,X,Y. T = ⓑ{a,J}Y.X →
+                          ∃∃Z. ⦃h, L.ⓑ{J}Y⦄ ⊢ X •*[g] Z & U = ⓑ{a,J}Y.Z.
+#h #g #L #T #U #H @(sstas_ind_alt … H) -T
+[ #U0 #l #HU0 #a #J #X #Y #H destruct
+  elim (ssta_inv_bind1 … HU0) -HU0 #X0 #HX0 #H destruct /3 width=3/
+| #T0 #U0 #l #HTU0 #_ #IHU0 #a #J #X #Y #H destruct
+  elim (ssta_inv_bind1 … HTU0) -HTU0 #X0 #HX0 #H destruct
+  elim (IHU0 a J X0 Y …) -IHU0 // #X1 #HX01 #H destruct /3 width=4/
+]
+qed-.
+
+lemma sstas_inv_bind1: ∀h,g,a,J,L,Y,X,U. ⦃h, L⦄ ⊢ ⓑ{a,J}Y.X •*[g] U →
+                       ∃∃Z. ⦃h, L.ⓑ{J}Y⦄ ⊢ X •*[g] Z & U = ⓑ{a,J}Y.Z.
+/2 width=3 by sstas_inv_bind1_aux/ qed-.
+
+fact sstas_inv_appl1_aux: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U → ∀X,Y. T = ⓐY.X →
+                          ∃∃Z. ⦃h, L⦄ ⊢ X •*[g] Z & U = ⓐY.Z.
+#h #g #L #T #U #H @(sstas_ind_alt … H) -T
+[ #U0 #l #HU0 #X #Y #H destruct
+  elim (ssta_inv_appl1 … HU0) -HU0 #X0 #HX0 #H destruct /3 width=3/
+| #T0 #U0 #l #HTU0 #_ #IHU0 #X #Y #H destruct
+  elim (ssta_inv_appl1 … HTU0) -HTU0 #X0 #HX0 #H destruct
+  elim (IHU0 X0 Y ?) -IHU0 // #X1 #HX01 #H destruct /3 width=4/
+]
+qed-.
+
+lemma sstas_inv_appl1: ∀h,g,L,Y,X,U. ⦃h, L⦄ ⊢ ⓐY.X •*[g] U →
+                       ∃∃Z. ⦃h, L⦄ ⊢ X •*[g] Z & U = ⓐY.Z.
+/2 width=3 by sstas_inv_appl1_aux/ qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma sstas_fwd_correct: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U →
+                         ∃∃l,W. ⦃h, L⦄ ⊢ U •[g, l] W.
+#h #g #L #T #U #H @(sstas_ind_alt … H) -T // /2 width=3/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_aaa.ma
new file mode 100644
index 000000000..fbf485841
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_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/static/ssta_aaa.ma".
+include "basic_2/unwind/sstas.ma".
+
+(* ITERATED STRATIFIED STATIC TYPE ASSIGNMENT FOR TERMS *********************)
+
+(* Properties on atomic arity assignment for terms **************************)
+
+lemma sstas_aaa: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U →
+                 ∀A. L ⊢ T ⁝ A → L ⊢ U ⁝ A.
+#h #g #L #T #U #H @(sstas_ind_alt … H) -T // /3 width=6/
+qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_lift.ma
new file mode 100644
index 000000000..7273963a3
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_lift.ma
@@ -0,0 +1,53 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/ssta_lift.ma".
+include "basic_2/unwind/sstas.ma".
+
+(* ITERATED STRATIFIED STATIC TYPE ASSIGNMENT FOR TERMS *********************)
+
+(* Advanced properties ******************************************************)
+
+lemma ssta_sstas: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l+1] U → ⦃h, L⦄ ⊢ T •*[g] U.
+#h #g #L #T #U #l #HTU
+elim (ssta_fwd_correct … HTU) /3 width=4/
+qed. 
+
+(* Properties on relocation *************************************************)
+
+lemma sstas_lift: ∀h,g,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 •*[g] U1 →
+                  ∀L2,d,e. ⇩[d, e] L2 ≡ L1 → ∀T2. ⇧[d, e] T1 ≡ T2 →
+                  ∀U2. ⇧[d, e] U1 ≡ U2 → ⦃h, L2⦄ ⊢ T2 •*[g] U2.
+#h #g #L1 #T1 #U1 #H @(sstas_ind_alt … H) -T1
+[ #T1 #l #HUT1 #L2 #d #e #HL21 #X #HX #U2 #HU12
+  >(lift_mono … HX … HU12) -X
+  elim (lift_total T1 d e) /3 width=11/
+| #T0 #U0 #l0 #HTU0 #_ #IHU01 #L2 #d #e #HL21 #T2 #HT02 #U2 #HU12
+  elim (lift_total U0 d e) /3 width=10/
+]
+qed.
+
+(* Inversion lemmas on relocation *******************************************)
+
+lemma sstas_inv_lift1: ∀h,g,L2,T2,U2. ⦃h, L2⦄ ⊢ T2 •*[g] U2 →
+                       ∀L1,d,e. ⇩[d, e] L2 ≡ L1 → ∀T1. ⇧[d, e] T1 ≡ T2 →
+                       ∃∃U1. ⦃h, L1⦄ ⊢ T1 •*[g] U1 & ⇧[d, e] U1 ≡ U2.
+#h #g #L2 #T2 #U2 #H @(sstas_ind_alt … H) -T2
+[ #T2 #l #HUT2 #L1 #d #e #HL21 #U1 #HU12
+  elim (ssta_inv_lift1 … HUT2 … HL21 … HU12) -HUT2 -HL21 /3 width=3/
+| #T0 #U0 #l0 #HTU0 #_ #IHU01 #L1 #d #e #HL21 #U1 #HU12
+  elim (ssta_inv_lift1 … HTU0 … HL21 … HU12) -HTU0 -HU12 #U #HU1 #HU0
+  elim (IHU01 … HL21 … HU0) -IHU01 -HL21 -U0 /3 width=4/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_lsubss.ma b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_lsubss.ma
new file mode 100644
index 000000000..ba2910da8
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_lsubss.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/static/lsubss_ssta.ma".
+include "basic_2/unwind/sstas.ma".
+
+(* ITERATED STRATIFIED STATIC TYPE ASSIGNMENT FOR TERMS *********************)
+
+(* Properties on lenv ref for stratified type assignment ********************)
+
+lemma lsubss_sstas_trans: ∀h,g,L2,T,U. ⦃h, L2⦄ ⊢ T •*[g] U →
+                          ∀L1. h ⊢ L1 •⊑[g] L2 → ⦃h, L1⦄ ⊢ T •*[g] U.
+#h #g #L2 #T #U #H @(sstas_ind_alt … H) -T /3 width=4/ /3 width=5/
+qed.
+
+lemma lsubss_sstas_conf: ∀h,g,L1,T,U. ⦃h, L1⦄ ⊢ T •*[g] U →
+                         ∀L2. h ⊢ L1 •⊑[g] L2 → ⦃h, L2⦄ ⊢ T •*[g] U.
+#h #g #L2 #T #U #H @(sstas_ind_alt … H) -T /3 width=4/ /3 width=5/
+qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_ltpss_dx.ma b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_ltpss_dx.ma
new file mode 100644
index 000000000..84f2d805b
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_ltpss_dx.ma
@@ -0,0 +1,55 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/ssta_ltpss_dx.ma".
+include "basic_2/unwind/sstas.ma".
+
+(* ITERATED STRATIFIED STATIC TYPE ASSIGNMENT FOR TERMS *********************)
+
+(* Properties about dx parallel unfold **************************************)
+
+lemma sstas_ltpss_dx_tpss_conf: ∀h,g,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 •*[g] U1 →
+                                ∀L2,d,e. L1 ▶* [d, e] L2 →
+                                ∀T2. L2 ⊢ T1 ▶* [d, e] T2 →
+                                ∃∃U2. ⦃h, L2⦄ ⊢ T2 •*[g] U2 &
+                                      L2 ⊢ U1 ▶* [d, e] U2.
+#h #g #L1 #T1 #U1 #H @(sstas_ind_alt … H) -T1
+[ #T1 #l #HUT1 #L2 #d #e #HL12 #U2 #HU12
+  elim (ssta_ltpss_dx_tpss_conf … HUT1 … HL12 … HU12) -HUT1 -HL12 /3 width=3/
+| #T0 #U0 #l0 #HTU0 #_ #IHU01 #L2 #d #e #HL12 #T #HT0
+  elim (ssta_ltpss_dx_tpss_conf … HTU0 … HL12 … HT0) -HTU0 -HT0 #U #HTU #HU0
+  elim (IHU01 … HL12 … HU0) -IHU01 -HL12 -U0 /3 width=4/
+]
+qed.
+
+lemma sstas_ltpss_dx_tps_conf: ∀h,g,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 •*[g] U1 →
+                               ∀L2,d,e. L1 ▶* [d, e] L2 →
+                               ∀T2. L2 ⊢ T1 ▶ [d, e] T2 →
+                               ∃∃U2. ⦃h, L2⦄ ⊢ T2 •*[g] U2 & L2 ⊢ U1 ▶* [d, e] U2.
+/3 width=5/ qed.
+
+lemma sstas_ltpss_dx_conf: ∀h,g,L1,T,U1. ⦃h, L1⦄ ⊢ T •*[g] U1 →
+                           ∀L2,d,e. L1 ▶* [d, e] L2 →
+                           ∃∃U2. ⦃h, L2⦄ ⊢ T •*[g] U2 & L2 ⊢ U1 ▶* [d, e] U2.
+/2 width=5/ qed.
+
+lemma sstas_tpss_conf: ∀h,g,L,T1,U1. ⦃h, L⦄ ⊢ T1 •*[g] U1 →
+                       ∀T2,d,e. L ⊢ T1 ▶* [d, e] T2 →
+                       ∃∃U2. ⦃h, L⦄ ⊢ T2 •*[g] U2 & L ⊢ U1 ▶* [d, e] U2.
+/2 width=5/ qed.
+
+lemma sstas_tps_conf: ∀h,g,L,T1,U1. ⦃h, L⦄ ⊢ T1 •*[g] U1 →
+                      ∀T2,d,e. L ⊢ T1 ▶ [d, e] T2 →
+                      ∃∃U2. ⦃h, L⦄ ⊢ T2 •*[g] U2 & L ⊢ U1 ▶* [d, e] U2.
+/2 width=5/ qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_ltpss_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_ltpss_sn.ma
new file mode 100644
index 000000000..0a00fd9d8
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_ltpss_sn.ma
@@ -0,0 +1,53 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/ltpss_sn_alt.ma".
+include "basic_2/unwind/sstas_ltpss_dx.ma".
+
+(* ITERATED STRATIFIED STATIC TYPE ASSIGNMENT FOR TERMS ************************)
+
+(* Properties about sn parallel unfold *****************************************)
+
+lemma sstas_ltpss_sn_conf: ∀h,g,L1,L2,d,e. L1 ⊢ ▶* [d, e] L2 →
+                           ∀T,U1. ⦃h, L1⦄ ⊢ T •*[g] U1 →
+                           ∃∃U2. L1 ⊢ U1 ▶* [d, e] U2 & ⦃h, L2⦄ ⊢ T •*[g] U2.
+#h #g #L1 #L2 #d #e #H
+lapply (ltpss_sn_ltpssa … H) -H #H @(ltpssa_ind … H) -L2 /2 width=3/
+#L #L2 #HL1 #HL2 #IHL1 #T #U1 #H1
+lapply (ltpssa_ltpss_sn … HL1) -HL1 #HL1
+lapply (ltpss_sn_dx_trans_eq … HL1 … HL2) -HL1 #HL12
+elim (IHL1 … H1) -IHL1 -H1 #U #HU1 #HTU
+elim (sstas_ltpss_dx_conf … HTU … HL2) -HTU -HL2 #U2 #H2 #HU2  
+lapply (ltpss_sn_tpss_trans_eq … HU2 … HL12) -HU2 -HL12 #HU2
+lapply (tpss_trans_eq … HU1 HU2) -U /2 width=3/
+qed.
+
+lemma sstas_ltpss_sn_tpss_conf: ∀h,g,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 •*[g] U1 →
+                                ∀L2,d,e. L1 ⊢ ▶* [d, e] L2 →
+                                ∀T2. L2 ⊢ T1 ▶* [d, e] T2 →
+                                ∃∃U2. ⦃h, L2⦄ ⊢ T2 •*[g] U2 &
+                                      L1 ⊢ U1 ▶* [d, e] U2.
+#h #g #L1 #T1 #U1 #HTU1 #L2 #d #e #HL12 #T2 #HT12
+elim (sstas_ltpss_sn_conf … HL12 … HTU1) -HTU1 #U #HU1 #HT1U
+elim (sstas_tpss_conf … HT1U … HT12) -T1 #U2 #HTU2 #HU2
+lapply (ltpss_sn_tpss_trans_eq … HU2 … HL12) -HU2 -HL12 #HU2
+lapply (tpss_trans_eq … HU1 HU2) -U /2 width=3/
+qed.
+
+lemma sstas_ltpss_sn_tps_conf: ∀h,g,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 •*[g] U1 →
+                               ∀L2,d,e. L1 ⊢ ▶* [d, e] L2 →
+                               ∀T2. L2 ⊢ T1 ▶ [d, e] T2 →
+                               ∃∃U2. ⦃h, L2⦄ ⊢ T2 •*[g] U2 &
+                                     L1 ⊢ U1 ▶* [d, e] U2.
+/3 width=3/ qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_sstas.ma b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_sstas.ma
new file mode 100644
index 000000000..e7e99c001
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_sstas.ma
@@ -0,0 +1,52 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/ssta_ssta.ma".
+include "basic_2/unwind/sstas.ma".
+
+(* ITERATED STRATIFIED STATIC TYPE ASSIGNMENT FOR TERMS *********************)
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma sstas_inv_O: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U →
+                   ∀T0. ⦃h, L⦄ ⊢ T •[g , 0] T0 → U = T.
+#h #g #L #T #U #H @(sstas_ind_alt … H) -T //
+#T0 #U0 #l0 #HTU0 #_ #_ #T1 #HT01
+elim (ssta_mono … HTU0 … HT01) <plus_n_Sm #H destruct
+qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma sstas_strip: ∀h,g,L,T,U1. ⦃h, L⦄ ⊢ T •*[g] U1 →
+                   ∀U2,l. ⦃h, L⦄ ⊢ T •[g, l] U2 →
+                   ⦃h, L⦄ ⊢ U1 •[g, l] U2 ∨ ⦃h, L⦄ ⊢ U2 •*[g] U1.
+#h #g #L #T #U1 #H1 @(sstas_ind_alt … H1) -T /2 width=1/
+#T #U #l0 #HTU #HU1 #_ #U2 #l #H2
+elim (ssta_mono … H2 … HTU) -H2 -HTU #H1 #H2 destruct /2 width=1/
+qed-.
+
+(* Main properties **********************************************************)
+
+theorem sstas_trans: ∀h,g,L,T1,U. ⦃h, L⦄ ⊢ T1 •*[g] U →
+                     ∀T2. ⦃h, L⦄ ⊢ U •*[g] T2 → ⦃h, L⦄ ⊢ T1 •*[g] T2.
+#h #g #L #T1 #U #H1 @(sstas_ind_alt … H1) -T1 // /3 width=4/
+qed-.
+
+theorem sstas_conf: ∀h,g,L,T,U1. ⦃h, L⦄ ⊢ T •*[g] U1 →
+                    ∀U2. ⦃h, L⦄ ⊢ T •*[g] U2 →
+                   ⦃h, L⦄ ⊢ U1 •*[g] U2 ∨ ⦃h, L⦄ ⊢ U2 •*[g] U1.
+#h #g #L #T #U1 #H1 @(sstas_ind_alt … H1) -T /2 width=1/
+#T #U #l #HTU #HU1 #IHU1 #U2 #H2
+elim (sstas_strip … H2 … HTU) -T /2 width=1/ -IHU1 /3 width=4/
+qed-.
-- 
2.39.2