From b074ebf6441993694c6e39e4eaeeb58a3186f479 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 13 Jul 2012 16:28:23 +0000
Subject: [PATCH] - dynamic type assignment dismissed for now - stratified
 static type assignment and unwind defined

---
 .../lambda_delta/apps_2/functional/subst.ma   |   2 +-
 .../contribs/lambda_delta/basic_2/basic_1.txt |   7 -
 .../basic_2/computation/cprs_lift.ma          |   6 +
 .../basic_2/equivalence/cpcs_cpcs.ma          |  15 +
 .../basic_2/equivalence/cpcs_cprs.ma          |  21 ++
 .../basic_2/{hod/ntas.ma => etc/hod/ntas.etc} |   4 +
 .../ntas_lift.ma => etc/hod/ntas_lift.etc}    |   0
 .../{dynamic/lsubn.ma => etc/nta/lsubn.etc}   |   8 +
 .../lsubn_cpcs.ma => etc/nta/lsubn_cpcs.etc}  |   0
 .../nta/lsubn_ldrop.etc}                      |   0
 .../lsubn_nta.ma => etc/nta/lsubn_nta.etc}    |   0
 .../{dynamic/nta.ma => etc/nta/nta.etc}       |   0
 .../nta_aaa.ma => etc/nta/nta_aaa.etc}        |   0
 .../nta_alt.ma => etc/nta/nta_alt.etc}        |   0
 .../nta_lift.ma => etc/nta/nta_lift.etc}      |   0
 .../nta_ltpr.ma => etc/nta/nta_ltpr.etc}      |   0
 .../nta_ltpss.ma => etc/nta/nta_ltpss.etc}    |   0
 .../nta_nta.ma => etc/nta/nta_nta.etc}        |   0
 .../nta_sta.ma => etc/nta/nta_sta.etc}        |   0
 .../nta_thin.ma => etc/nta/nta_thin.etc}      |   0
 .../lambda_delta/basic_2/etc/snta/lsubsn.etc  | 110 +++++++
 .../basic_2/etc/snta/lsubsn_cpcs.etc          |  32 ++
 .../basic_2/etc/snta/lsubsn_ldrop.etc         |  65 ++++
 .../basic_2/etc/snta/lsubsn_snta.etc          |  49 +++
 .../lambda_delta/basic_2/etc/snta/snta.etc    |  48 +++
 .../basic_2/etc/snta/snta_lift.etc            | 238 +++++++++++++++
 .../basic_2/etc/snta/snta_ltpr.etc            | 278 ++++++++++++++++++
 .../basic_2/etc/snta/snta_ltpss.etc           | 123 ++++++++
 .../basic_2/etc/snta/snta_snta.etc            |  65 ++++
 .../basic_2/etc/snta/snta_thin.etc            | 116 ++++++++
 .../{static/sta.ma => etc/sta/sta.etc}        |   0
 .../sta_lift.ma => etc/sta/sta_lift.etc}      |   0
 .../sta_ltpss.ma => etc/sta/sta_ltpss.etc}    |   0
 .../sta_sta.ma => etc/sta/sta_sta.etc}        |   0
 .../basic_2/grammar/term_simple.ma            |   5 +
 .../contribs/lambda_delta/basic_2/names.txt   |  11 +-
 .../contribs/lambda_delta/basic_2/notation.ma |  36 ++-
 .../basic_2/reducibility/cpr_lift.ma          |   2 +-
 .../lambda_delta/basic_2/static/sd.ma         | 105 +++++++
 .../lambda_delta/basic_2/static/sh.ma         |  15 +-
 .../lambda_delta/basic_2/static/ssta.ma       | 134 +++++++++
 .../lambda_delta/basic_2/static/ssta_lift.ma  | 124 ++++++++
 .../lambda_delta/basic_2/static/ssta_ltpss.ma | 125 ++++++++
 .../lambda_delta/basic_2/static/ssta_ssta.ma  |  50 ++++
 .../lambda_delta/basic_2/unfold/delift.ma     |   7 +
 .../basic_2/unfold/thin_delift.ma             |   2 +-
 .../lambda_delta/basic_2/unfold/tpss.ma       |   4 +-
 .../lambda_delta/basic_2/unwind/sstas.ma      | 106 +++++++
 .../lambda_delta/basic_2/unwind/sstas_lift.ma |  57 ++++
 .../basic_2/unwind/sstas_ltpss.ma             |  55 ++++
 .../basic_2/unwind/sstas_sstas.ma             |  74 +++++
 .../contribs/lambda_delta/ground_2/arith.ma   |  27 +-
 52 files changed, 2093 insertions(+), 33 deletions(-)
 rename matita/matita/contribs/lambda_delta/basic_2/{hod/ntas.ma => etc/hod/ntas.etc} (93%)
 rename matita/matita/contribs/lambda_delta/basic_2/{hod/ntas_lift.ma => etc/hod/ntas_lift.etc} (100%)
 rename matita/matita/contribs/lambda_delta/basic_2/{dynamic/lsubn.ma => etc/nta/lsubn.etc} (94%)
 rename matita/matita/contribs/lambda_delta/basic_2/{dynamic/lsubn_cpcs.ma => etc/nta/lsubn_cpcs.etc} (100%)
 rename matita/matita/contribs/lambda_delta/basic_2/{dynamic/lsubn_ldrop.ma => etc/nta/lsubn_ldrop.etc} (100%)
 rename matita/matita/contribs/lambda_delta/basic_2/{dynamic/lsubn_nta.ma => etc/nta/lsubn_nta.etc} (100%)
 rename matita/matita/contribs/lambda_delta/basic_2/{dynamic/nta.ma => etc/nta/nta.etc} (100%)
 rename matita/matita/contribs/lambda_delta/basic_2/{dynamic/nta_aaa.ma => etc/nta/nta_aaa.etc} (100%)
 rename matita/matita/contribs/lambda_delta/basic_2/{dynamic/nta_alt.ma => etc/nta/nta_alt.etc} (100%)
 rename matita/matita/contribs/lambda_delta/basic_2/{dynamic/nta_lift.ma => etc/nta/nta_lift.etc} (100%)
 rename matita/matita/contribs/lambda_delta/basic_2/{dynamic/nta_ltpr.ma => etc/nta/nta_ltpr.etc} (100%)
 rename matita/matita/contribs/lambda_delta/basic_2/{dynamic/nta_ltpss.ma => etc/nta/nta_ltpss.etc} (100%)
 rename matita/matita/contribs/lambda_delta/basic_2/{dynamic/nta_nta.ma => etc/nta/nta_nta.etc} (100%)
 rename matita/matita/contribs/lambda_delta/basic_2/{dynamic/nta_sta.ma => etc/nta/nta_sta.etc} (100%)
 rename matita/matita/contribs/lambda_delta/basic_2/{dynamic/nta_thin.ma => etc/nta/nta_thin.etc} (100%)
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/etc/snta/lsubsn.etc
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/etc/snta/lsubsn_cpcs.etc
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/etc/snta/lsubsn_ldrop.etc
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/etc/snta/lsubsn_snta.etc
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta.etc
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta_lift.etc
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta_ltpr.etc
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta_ltpss.etc
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta_snta.etc
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta_thin.etc
 rename matita/matita/contribs/lambda_delta/basic_2/{static/sta.ma => etc/sta/sta.etc} (100%)
 rename matita/matita/contribs/lambda_delta/basic_2/{static/sta_lift.ma => etc/sta/sta_lift.etc} (100%)
 rename matita/matita/contribs/lambda_delta/basic_2/{static/sta_ltpss.ma => etc/sta/sta_ltpss.etc} (100%)
 rename matita/matita/contribs/lambda_delta/basic_2/{static/sta_sta.ma => etc/sta/sta_sta.etc} (100%)
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/static/sd.ma
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/static/ssta.ma
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/static/ssta_lift.ma
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/static/ssta_ltpss.ma
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/static/ssta_ssta.ma
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/unwind/sstas.ma
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/unwind/sstas_lift.ma
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/unwind/sstas_ltpss.ma
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/unwind/sstas_sstas.ma

diff --git a/matita/matita/contribs/lambda_delta/apps_2/functional/subst.ma b/matita/matita/contribs/lambda_delta/apps_2/functional/subst.ma
index 78f319a06..4c164f018 100644
--- a/matita/matita/contribs/lambda_delta/apps_2/functional/subst.ma
+++ b/matita/matita/contribs/lambda_delta/apps_2/functional/subst.ma
@@ -39,7 +39,7 @@ theorem fsubst_delift: ∀K,V,T,L,d.
 [ * #i #L #d #HLK normalize in ⊢ (? ? ? ? ? %); /2 width=3/
   elim (lt_or_eq_or_gt i d) #Hid
   [ -HLK >(tri_lt ?????? Hid) /3 width=3/
-  | destruct >tri_eq /4 width=4 by tpss_strap, tps_subst, le_n, ex2_1_intro/ (**) (* too slow without trace *)   
+  | destruct >tri_eq /4 width=4 by tpss_strap2, tps_subst, le_n, ex2_1_intro/ (**) (* too slow without trace *)   
   | -HLK >(tri_gt ?????? Hid) /3 width=3/
   ]
 | * /3 width=1/ /4 width=1/
diff --git a/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt b/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt
index c5fe6def0..70d162599 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt
+++ b/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt
@@ -184,13 +184,6 @@ pr3/pr1 pr3_pr1
 pr3/props pr3_eta
 sn3/props sns3_lifts
 sty1/cnt sty1_cnt
-sty1/props sty1_trans
-sty1/props sty1_bind
-sty1/props sty1_appl
-sty1/props sty1_lift
-sty1/props sty1_correct
-sty1/props sty1_abbr
-sty1/props sty1_cast2
 subst/fwd subst_sort
 subst/fwd subst_lref_lt
 subst/fwd subst_lref_eq
diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lift.ma
index 11ce81ff8..c3cabda9e 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lift.ma
@@ -47,6 +47,12 @@ lemma cprs_inv_abst1: ∀I,W,L,V1,T1,U2. L ⊢ ⓛV1. T1 ➡* U2 →
 elim (cpr_inv_abst1 … HU2 I W) -HU2 #V2 #T2 #HV2 #HT2 #H destruct  /3 width=5/
 qed-.
 
+lemma cprs_inv_abst: ∀L,V1,V2,T1,T2. L ⊢ ⓛV1. T1 ➡* ⓛV2. T2 → ∀I,W.
+                     L ⊢ V1 ➡* V2 ∧ L. ⓑ{I} W ⊢ T1 ➡* T2.
+#L #V1 #V2 #T1 #T2 #H #I #W
+elim (cprs_inv_abst1 I W … H) -H #V #T #HV1 #HT1 #H destruct /2 width=1/
+qed-.
+
 (* Relocation properties ****************************************************)
 
 (* Basic_1: was: pr3_lift *)
diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma
index fcad182e0..cb34d78c5 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma
@@ -90,6 +90,21 @@ qed-.
 
 (* Advanced properties ******************************************************)
 
+lemma cpr_cprs_conf: ∀L,T,T1,T2. L ⊢ T ➡* T1 → L ⊢ T ➡ T2 → L ⊢ T1 ⬌* T2.
+#L #T #T1 #T2 #HT1 #HT2
+elim (cprs_strip … HT1 … HT2) /2 width=3 by cpr_cprs_div/
+qed-.
+
+lemma cprs_cpr_conf: ∀L,T,T1,T2. L ⊢ T ➡* T1 → L ⊢ T ➡ T2 → L ⊢ T2 ⬌* T1.
+#L #T #T1 #T2 #HT1 #HT2
+elim (cprs_strip … HT1 … HT2) /2 width=3 by cprs_cpr_div/
+qed-.
+
+lemma cprs_conf: ∀L,T,T1,T2. L ⊢ T ➡* T1 → L ⊢ T ➡* T2 → L ⊢ T1 ⬌* T2.
+#L #T #T1 #T2 #HT1 #HT2
+elim (cprs_conf … HT1 … HT2) /2 width=3/
+qed-.
+
 (* Basic_1: was only: pc3_thin_dx *)
 lemma cpcs_flat: ∀L,V1,V2. L ⊢ V1 ⬌* V2 → ∀T1,T2. L ⊢ T1 ⬌* T2 →
                  ∀I. L ⊢ ⓕ{I}V1. T1 ⬌* ⓕ{I}V2. T2.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cprs.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cprs.ma
index 7394858ef..c2911e1c8 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cprs.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cprs.ma
@@ -39,21 +39,42 @@ lemma cpcs_cprs_strap1: ∀L,T1,T. L ⊢ T1 ⬌* T → ∀T2. L ⊢ T ➡* T2 
 #L #T1 #T #HT1 #T2 #H @(cprs_ind … H) -T2 /width=1/ /2 width=3/
 qed.
 
+lemma cpcs_cpr_strap1: ∀L,T1,T. L ⊢ T1 ⬌* T → ∀T2. L ⊢ T ➡ T2 → L ⊢ T1 ⬌* T2.
+/3 width=3/ qed-.
+
 lemma cpcs_cprs_strap2: ∀L,T1,T. L ⊢ T1 ➡* T → ∀T2. L ⊢ T ⬌* T2 → L ⊢ T1 ⬌* T2.
 #L #T1 #T #H #T2 #HT2 @(cprs_ind_dx … H) -T1 /width=1/ /2 width=3/
 qed.
 
+lemma cpcs_cpr_strap2: ∀L,T1,T. L ⊢ T1 ➡ T → ∀T2. L ⊢ T ⬌* T2 → L ⊢ T1 ⬌* T2.
+/3 width=3/ qed-.
+
 lemma cpcs_cprs_div: ∀L,T1,T. L ⊢ T1 ⬌* T → ∀T2. L ⊢ T2 ➡* T → L ⊢ T1 ⬌* T2.
 #L #T1 #T #HT1 #T2 #H @(cprs_ind_dx … H) -T2 /width=1/ /2 width=3/
 qed.
 
+lemma cpcs_cpr_div: ∀L,T1,T. L ⊢ T1 ⬌* T → ∀T2. L ⊢ T2 ➡ T → L ⊢ T1 ⬌* T2.
+/3 width=3/ qed-.
+
 (* Basic_1: was: pc3_pr3_conf *)
 lemma cpcs_cprs_conf: ∀L,T1,T. L ⊢ T ➡* T1 → ∀T2. L ⊢ T ⬌* T2 → L ⊢ T1 ⬌* T2.
 #L #T1 #T #H #T2 #HT2 @(cprs_ind … H) -T1 /width=1/ /2 width=3/
 qed.
 
+lemma cpcs_cpr_conf: ∀L,T1,T. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ⬌* T2 → L ⊢ T1 ⬌* T2.
+/3 width=3/ qed-.
+
 (* Basic_1: was: pc3_pr3_t *)
 (* Basic_1: note: pc3_pr3_t should be renamed *)
 lemma cprs_div: ∀L,T1,T. L ⊢ T1 ➡* T → ∀T2. L ⊢ T2 ➡* T → L ⊢ T1 ⬌* T2.
 #L #T1 #T #HT1 #T2 #H @(cprs_ind_dx … H) -T2 /2 width=1/ /2 width=3/
 qed.
+
+lemma cprs_cpr_div: ∀L,T1,T. L ⊢ T1 ➡* T → ∀T2. L ⊢ T2 ➡ T → L ⊢ T1 ⬌* T2.
+/3 width=5 by step, cprs_div/ qed-.
+
+lemma cpr_cprs_div: ∀L,T1,T. L ⊢ T1 ➡ T → ∀T2. L ⊢ T2 ➡* T → L ⊢ T1 ⬌* T2.
+/3 width=3 by step, cprs_div/ qed-.
+
+lemma cpr_div: ∀L,T1,T. L ⊢ T1 ➡ T → ∀T2. L ⊢ T2 ➡ T → L ⊢ T1 ⬌* T2.
+/3 width=5 by step, cprs_div/ qed-.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/hod/ntas.ma b/matita/matita/contribs/lambda_delta/basic_2/etc/hod/ntas.etc
similarity index 93%
rename from matita/matita/contribs/lambda_delta/basic_2/hod/ntas.ma
rename to matita/matita/contribs/lambda_delta/basic_2/etc/hod/ntas.etc
index c090997e6..8cfaa343b 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/hod/ntas.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/etc/hod/ntas.etc
@@ -12,6 +12,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
+notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 : : * break term 46 T2 )"
+   non associative with precedence 45
+   for @{ 'NativeTypeStarAlt $h $L $T1 $T2 }.
+
 include "basic_2/dynamic/nta.ma".
 
 (* HIGHER ORDER NATIVE TYPE ASSIGNMENT ON TERMS *****************************)
diff --git a/matita/matita/contribs/lambda_delta/basic_2/hod/ntas_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/etc/hod/ntas_lift.etc
similarity index 100%
rename from matita/matita/contribs/lambda_delta/basic_2/hod/ntas_lift.ma
rename to matita/matita/contribs/lambda_delta/basic_2/etc/hod/ntas_lift.etc
diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/lsubn.ma b/matita/matita/contribs/lambda_delta/basic_2/etc/nta/lsubn.etc
similarity index 94%
rename from matita/matita/contribs/lambda_delta/basic_2/dynamic/lsubn.ma
rename to matita/matita/contribs/lambda_delta/basic_2/etc/nta/lsubn.etc
index cedff815a..c4359c35f 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/lsubn.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/etc/nta/lsubn.etc
@@ -12,6 +12,14 @@
 (*                                                                        *)
 (**************************************************************************)
 
+notation "hvbox( h ⊢ break term 46 L1 : ⊑ break term 46 L2 )"
+   non associative with precedence 45
+   for @{ 'CrSubEqN $h $L1 $L2 }.
+
+notation "hvbox( h ⊢ break term 46 L1 : : ⊑ break term 46 L2 )"
+   non associative with precedence 45
+   for @{ 'CrSubEqNAlt $h $L1 $L2 }.
+
 include "basic_2/dynamic/nta.ma".
 
 (* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE TYPE ASSIGNMENT ******************)
diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/lsubn_cpcs.ma b/matita/matita/contribs/lambda_delta/basic_2/etc/nta/lsubn_cpcs.etc
similarity index 100%
rename from matita/matita/contribs/lambda_delta/basic_2/dynamic/lsubn_cpcs.ma
rename to matita/matita/contribs/lambda_delta/basic_2/etc/nta/lsubn_cpcs.etc
diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/lsubn_ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/etc/nta/lsubn_ldrop.etc
similarity index 100%
rename from matita/matita/contribs/lambda_delta/basic_2/dynamic/lsubn_ldrop.ma
rename to matita/matita/contribs/lambda_delta/basic_2/etc/nta/lsubn_ldrop.etc
diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/lsubn_nta.ma b/matita/matita/contribs/lambda_delta/basic_2/etc/nta/lsubn_nta.etc
similarity index 100%
rename from matita/matita/contribs/lambda_delta/basic_2/dynamic/lsubn_nta.ma
rename to matita/matita/contribs/lambda_delta/basic_2/etc/nta/lsubn_nta.etc
diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta.ma b/matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta.etc
similarity index 100%
rename from matita/matita/contribs/lambda_delta/basic_2/dynamic/nta.ma
rename to matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta.etc
diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_aaa.etc
similarity index 100%
rename from matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_aaa.ma
rename to matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_aaa.etc
diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_alt.ma b/matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_alt.etc
similarity index 100%
rename from matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_alt.ma
rename to matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_alt.etc
diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_lift.etc
similarity index 100%
rename from matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_lift.ma
rename to matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_lift.etc
diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_ltpr.ma b/matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_ltpr.etc
similarity index 100%
rename from matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_ltpr.ma
rename to matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_ltpr.etc
diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_ltpss.etc
similarity index 100%
rename from matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_ltpss.ma
rename to matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_ltpss.etc
diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_nta.ma b/matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_nta.etc
similarity index 100%
rename from matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_nta.ma
rename to matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_nta.etc
diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_sta.ma b/matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_sta.etc
similarity index 100%
rename from matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_sta.ma
rename to matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_sta.etc
diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_thin.ma b/matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_thin.etc
similarity index 100%
rename from matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_thin.ma
rename to matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_thin.etc
diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/snta/lsubsn.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/snta/lsubsn.etc
new file mode 100644
index 000000000..f6b54500e
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/etc/snta/lsubsn.etc
@@ -0,0 +1,110 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "hvbox( h ⊢ break term 46 L1 : ⊑ [ ] break term 46 L2 )"
+   non associative with precedence 45
+   for @{ 'StratifiedCrSubEqN $h $L1 $L2 }.
+
+include "basic_2/dynamic/snta.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE TYPE ASSIGNMENT *******)
+
+(* Note: may not be transitive *)
+inductive lsubsn (h:sh): relation lenv ≝
+| lsubsn_atom: lsubsn h (⋆) (⋆)
+| lsubsn_pair: ∀I,L1,L2,W. lsubsn h L1 L2 →
+               lsubsn h (L1. ⓑ{I} W) (L2. ⓑ{I} W)
+| lsubsn_abbr: ∀L1,L2,V,W,l. ⦃h, L1⦄ ⊢ V :[l+1] W → ⦃h, L2⦄ ⊢ V :[l+1] W →
+               lsubsn h L1 L2 → lsubsn h (L1. ⓓV) (L2. ⓛW)
+.
+
+interpretation
+  "local environment refinement (stratified native type assigment)"
+  'StratifiedCrSubEqN h L1 L2 = (lsubsn h L1 L2).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact lsubsn_inv_atom1_aux: ∀h,L1,L2. h ⊢ L1 :⊑[] L2 → L1 = ⋆ → L2 = ⋆.
+#h #L1 #L2 * -L1 -L2
+[ //
+| #I #L1 #L2 #V #_ #H destruct
+| #L1 #L2 #V #W #l #_ #_ #_ #H destruct
+]
+qed.
+
+lemma lsubsn_inv_atom1: ∀h,L2. h ⊢ ⋆ :⊑[] L2 → L2 = ⋆.
+/2 width=5/ qed-.
+
+fact lsubsn_inv_pair1_aux: ∀h,L1,L2. h ⊢ L1 :⊑[] L2 →
+                           ∀I,K1,V. L1 = K1. ⓑ{I} V →
+                           (∃∃K2. h ⊢ K1 :⊑[] K2 & L2 = K2. ⓑ{I} V) ∨
+                           ∃∃K2,W,l. ⦃h, K1⦄ ⊢ V :[l+1] W & ⦃h, K2⦄ ⊢ V :[l+1] W &
+                                     h ⊢ K1 :⊑[] K2 & L2 = K2. ⓛW & I = Abbr.
+#h #L1 #L2 * -L1 -L2
+[ #I #K1 #V #H destruct
+| #J #L1 #L2 #V #HL12 #I #K1 #W #H destruct /3 width=3/
+| #L1 #L2 #V #W #l #H1VW #H2VW #HL12 #I #K1 #V1 #H destruct /3 width=7/
+]
+qed.
+
+lemma lsubsn_inv_pair1: ∀h,I,K1,L2,V. h ⊢ K1. ⓑ{I} V :⊑[] L2 →
+                        (∃∃K2. h ⊢ K1 :⊑[] K2 & L2 = K2. ⓑ{I} V) ∨
+                        ∃∃K2,W,l. ⦃h, K1⦄ ⊢ V :[l+1] W & ⦃h, K2⦄ ⊢ V :[l+1] W &
+                                  h ⊢ K1 :⊑[] K2 & L2 = K2. ⓛW & I = Abbr.
+/2 width=3/ qed-.
+
+fact lsubsn_inv_atom2_aux: ∀h,L1,L2. h ⊢ L1 :⊑[] L2 → L2 = ⋆ → L1 = ⋆.
+#h #L1 #L2 * -L1 -L2
+[ //
+| #I #L1 #L2 #V #_ #H destruct
+| #L1 #L2 #V #W #l #_ #_ #_ #H destruct
+]
+qed.
+
+lemma lsubsn_inv_atom2: ∀h,L1. h ⊢ L1 :⊑[] ⋆ → L1 = ⋆.
+/2 width=5/ qed-.
+
+fact lsubsn_inv_pair2_aux: ∀h,L1,L2. h ⊢ L1 :⊑[] L2 →
+                           ∀I,K2,W. L2 = K2. ⓑ{I} W →
+                           (∃∃K1. h ⊢ K1 :⊑[] K2 & L1 = K1. ⓑ{I} W) ∨
+                           ∃∃K1,V,l. ⦃h, K1⦄ ⊢ V :[l+1] W & ⦃h, K2⦄ ⊢ V :[l+1] W &
+                                     h ⊢ K1 :⊑[] K2 & L1 = K1. ⓓV & I = Abst.
+#h #L1 #L2 * -L1 -L2
+[ #I #K2 #W #H destruct
+| #J #L1 #L2 #V #HL12 #I #K2 #W #H destruct /3 width=3/
+| #L1 #L2 #V #W #l #H1VW #H2VW #HL12 #I #K2 #W2 #H destruct /3 width=7/
+]
+qed.
+
+lemma lsubsn_inv_pair2: ∀h,I,L1,K2,W. h ⊢ L1 :⊑[] K2. ⓑ{I} W →
+                        (∃∃K1. h ⊢ K1 :⊑[] K2 & L1 = K1. ⓑ{I} W) ∨
+                        ∃∃K1,V,l. ⦃h, K1⦄ ⊢ V :[l+1] W & ⦃h, K2⦄ ⊢ V :[l+1] W &
+                                  h ⊢ K1 :⊑[] K2 & L1 = K1. ⓓV & I = Abst.
+/2 width=3/ qed-.
+
+(* Basic_forward lemmas *****************************************************)
+
+lemma lsubsn_fwd_lsubs1: ∀h,L1,L2. h ⊢ L1 :⊑[] L2 → L1 ≼[0, |L1|] L2.
+#h #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
+qed-.
+
+lemma lsubsn_fwd_lsubs2: ∀h,L1,L2. h ⊢ L1 :⊑[] L2 → L1 ≼[0, |L2|] L2.
+#h #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma lsubsn_refl: ∀h,L. h ⊢ L :⊑[] L.
+#h #L elim L -L // /2 width=1/
+qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/snta/lsubsn_cpcs.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/snta/lsubsn_cpcs.etc
new file mode 100644
index 000000000..38f7e17bd
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/etc/snta/lsubsn_cpcs.etc
@@ -0,0 +1,32 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/equivalence/cpcs_cpcs.ma".
+include "basic_2/dynamic/lsubsn.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE TYPE ASSIGNMENT *******)
+
+(* Properties on context-sensitive parallel equivalence for terms ***********)
+
+lemma cpr_lsubsn_trans: ∀h,L1,L2. h ⊢ L1 :⊑[] L2 →
+                        ∀T1,T2. L2 ⊢ T1 ➡ T2 → L1 ⊢ T1 ➡ T2.
+/3 width=5 by lsubsn_fwd_lsubs2, cpr_lsubs_trans/ qed-.
+
+lemma cprs_lsubsn_trans: ∀h,L1,L2. h ⊢ L1 :⊑[] L2 →
+                         ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2.
+/3 width=5 by lsubsn_fwd_lsubs2, cprs_lsubs_trans/ qed-.
+
+lemma cpcs_lsubsn_trans: ∀h,L1,L2. h ⊢ L1 :⊑[] L2 →
+                         ∀T1,T2. L2 ⊢ T1 ⬌* T2 → L1 ⊢ T1 ⬌* T2.
+/3 width=5 by lsubsn_fwd_lsubs2, cpcs_lsubs_trans/ qed-.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/snta/lsubsn_ldrop.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/snta/lsubsn_ldrop.etc
new file mode 100644
index 000000000..092883783
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/etc/snta/lsubsn_ldrop.etc
@@ -0,0 +1,65 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/lsubsn.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE TYPE ASSIGNMENT *******)
+
+(* Properties concerning basic local environment slicing ********************)
+
+(* Note: the constant 0 cannot be generalized *)
+lemma lsubsn_ldrop_O1_conf: ∀h,L1,L2. h ⊢ L1 :⊑[] L2 →
+                            ∀K1,e. ⇩[0, e] L1 ≡ K1 →
+                            ∃∃K2. h ⊢ K1 :⊑[] K2 & ⇩[0, e] L2 ≡ K2.
+#h #L1 #L2 #H elim H -L1 -L2
+[ /2 width=3/
+| #I #L1 #L2 #V #_ #IHL12 #K1 #e #H
+  elim (ldrop_inv_O1 … H) -H * #He #HLK1
+  [ destruct
+    elim (IHL12 L1 0 ?) -IHL12 // #X #HL12 #H
+    <(ldrop_inv_refl … H) in HL12; -H /3 width=3/
+  | elim (IHL12 … HLK1) -L1 /3 width=3/
+  ]
+| #L1 #L2 #V #W #l #H1VW #H2VW #_ #IHL12 #K1 #e #H
+  elim (ldrop_inv_O1 … H) -H * #He #HLK1
+  [ destruct
+    elim (IHL12 L1 0 ?) -IHL12 // #X #HL12 #H
+    <(ldrop_inv_refl … H) in HL12; -H /3 width=3/
+  | elim (IHL12 … HLK1) -L1 /3 width=3/
+  ]
+]
+qed.
+
+(* Note: the constant 0 cannot be generalized *)
+lemma lsubsn_ldrop_O1_trans: ∀h,L1,L2. h ⊢ L1 :⊑[] L2 →
+                             ∀K2,e. ⇩[0, e] L2 ≡ K2 →
+                             ∃∃K1. h ⊢ K1 :⊑[] K2 & ⇩[0, e] L1 ≡ K1.
+#h #L1 #L2 #H elim H -L1 -L2
+[ /2 width=3/
+| #I #L1 #L2 #V #_ #IHL12 #K2 #e #H
+  elim (ldrop_inv_O1 … H) -H * #He #HLK2
+  [ destruct
+    elim (IHL12 L2 0 ?) -IHL12 // #X #HL12 #H
+    <(ldrop_inv_refl … H) in HL12; -H /3 width=3/
+  | elim (IHL12 … HLK2) -L2 /3 width=3/
+  ]
+| #L1 #L2 #V #W #l #H1VW #H2VW #_ #IHL12 #K2 #e #H
+  elim (ldrop_inv_O1 … H) -H * #He #HLK2
+  [ destruct
+    elim (IHL12 L2 0 ?) -IHL12 // #X #HL12 #H
+    <(ldrop_inv_refl … H) in HL12; -H /3 width=3/
+  | elim (IHL12 … HLK2) -L2 /3 width=3/
+  ]
+]
+qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/snta/lsubsn_snta.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/snta/lsubsn_snta.etc
new file mode 100644
index 000000000..c6215302c
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/etc/snta/lsubsn_snta.etc
@@ -0,0 +1,49 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/snta_snta.ma".
+include "basic_2/dynamic/lsubsn_ldrop.ma".
+include "basic_2/dynamic/lsubsn_cpcs.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE TYPE ASSIGNMENT *******)
+
+(* Properties concerning stratified native type assignment ******************)
+
+(* Note: the corresponding confluence property does not hold *)
+lemma lsubsn_snta_trans: ∀h,L2,T,U,l. ⦃h, L2⦄ ⊢ T :[l] U →
+                         ∀L1. h ⊢ L1 :⊑[] L2 → ⦃h, L1⦄ ⊢ T :[l] U.
+#h #L2 #T #U #l #H elim H -L2 -T -U -l
+[ //
+| #L2 #K2 #V2 #W2 #U2 #i #l #HLK2 #_ #WU2 #IHVW2 #L1 #HL12
+  elim (lsubsn_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1
+  elim (lsubsn_inv_pair2 … H) -H * #K1
+  [ #HK12 #H destruct /3 width=6/
+  | #V1 #l0 #_ #_ #_ #_ #H destruct
+  ]
+| #L2 #K2 #W2 #V2 #U2 #i #l #HLK2 #HWV2 #HWU2 #IHWV2 #L1 #HL12
+  elim (lsubsn_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1
+  elim (lsubsn_inv_pair2 … H) -H * #K1 [ -HWV2 | -IHWV2 ]
+  [ #HK12 #H destruct /3 width=6/
+  | #V1 #l0 #H1 #H2 #_ #H #_ destruct
+    elim (snta_fwd_correct … H2) -H2 #V #H
+    elim (snta_mono … HWV2 … H) -HWV2 -H /2 width=6/
+  ]
+| /4 width=3/
+| /3 width=2/
+| /3 width=2/
+| /3 width=1/
+| #L2 #T #U1 #U2 #V2 #l #_ #HU12 #_ #IHTU1 #IHUV2 #L1 #HL12
+  lapply (cpcs_lsubsn_trans … HL12 … HU12) -HU12 /3 width=3/
+]
+qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta.etc
new file mode 100644
index 000000000..71ed42179
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta.etc
@@ -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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 : * break [ l ] break term 46 T2 )"
+   non associative with precedence 45
+   for @{ 'NativeTypeStar $h $l $L $T1 $T2 }.
+
+notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 : break [ l ] break term 46 T2 )"
+   non associative with precedence 45
+   for @{ 'StratifiedNativeType $h $l $L $T1 $T2 }.
+
+include "basic_2/static/sh.ma".
+include "basic_2/equivalence/cpcs.ma".
+
+(* STRATIFIED NATIVE TYPE ASSIGNMENT ON TERMS *******************************)
+
+inductive snta (h:sh): nat → lenv → relation term ≝
+| snta_sort: ∀L,k. snta h 0 L (⋆k) (⋆(next h k))
+| snta_ldef: ∀L,K,V,W,U,i,l. ⇩[0, i] L ≡ K. ⓓV → snta h l K V W →
+             ⇧[0, i + 1] W ≡ U → snta h l L (#i) U
+| snta_ldec: ∀L,K,W,V,U,i,l. ⇩[0, i] L ≡ K. ⓛW → snta h l K W V →
+             ⇧[0, i + 1] W ≡ U → snta h (l+1) L (#i) U
+| snta_bind: ∀I,L,V,W,T,U,l1,l2. snta h l1 L V W → snta h l2 (L. ⓑ{I} V) T U →
+             snta h l2 L (ⓑ{I}V.T) (ⓑ{I}V.U)
+| snta_appl: ∀L,V,W1,W2,T,U,l1,l2. snta h (l1+1) L V W2 →
+             snta h l2 L (ⓛW1.T) (ⓛW2.U) →
+             snta h l2 L (ⓐV.ⓛW1.T) (ⓐV.ⓛW2.U)
+| snta_pure: ∀L,V,T,U,W,l. snta h (l+1) L T U → snta h l L (ⓐV.U) W →
+             snta h (l+1) L (ⓐV.T) (ⓐV.U)
+| snta_cast: ∀L,T,U,W,l1,l2. snta h l2 L T U → snta h l1 L U W →
+             snta h l2 L (ⓝU.T) U
+| snta_conv: ∀L,T,U1,U2,V2,l. snta h l L T U1 → L ⊢ U1 ⬌* U2 →
+             snta h (l-1) L U2 V2 → snta h l L T U2
+.
+
+interpretation "stratified native type assignment (term)"
+   'StratifiedNativeType h l L T U = (snta h l L T U).
diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta_lift.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta_lift.etc
new file mode 100644
index 000000000..424bfe89f
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta_lift.etc
@@ -0,0 +1,238 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/equivalence/cpcs_cpcs.ma".
+include "basic_2/dynamic/snta.ma".
+
+(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************)
+
+(* Advanced inversion lemmas ************************************************)
+
+fact snta_inv_sort1_aux: ∀h,L,T,U,l. ⦃h, L⦄ ⊢ T :[l] U → ∀k0. T = ⋆k0 →
+                         l = 0 ∧ L ⊢ ⋆(next h k0) ⬌* U.
+#h #L #T #U #l #H elim H -L -T -U -l
+[ #L #k #k0 #H destruct /2 width=1/
+| #L #K #V #W #U #i #l #_ #_ #_ #_ #k0 #H destruct
+| #L #K #W #V #U #i #l #_ #_ #_ #_ #k0 #H destruct
+| #I #L #V #W #T #U #l1 #l2 #_ #_ #_ #_ #k0 #H destruct
+| #L #V #W1 #W2 #T #U #l1 #l2 #_ #_ #_ #_ #k0 #H destruct
+| #L #V #T #U #W #l #_ #_ #_ #_ #k0 #H destruct
+| #L #T #U #W #l1 #l2 #_ #_ #_ #_ #k0 #H destruct
+| #L #T #U1 #U2 #V2 #l #_ #HU12 #_ #IHTU1 #_ #k0 #H destruct
+  elim (IHTU1 ??) -IHTU1 [3: // |2: skip ] #H #Hk0
+  lapply (cpcs_trans … Hk0 … HU12) -U1 /2 width=1/
+]
+qed.
+
+lemma snta_inv_sort1: ∀h,L,U,k,l. ⦃h, L⦄ ⊢ ⋆k :[l] U →
+                      l = 0 ∧ L ⊢ ⋆(next h k) ⬌* U.
+/2 width=4/ qed-.
+
+fact snta_inv_lref1_aux: ∀h,L,T,U,l. ⦃h, L⦄ ⊢ T :[l] U → ∀j. T = #j →
+                         (∃∃K,V,W,U0. ⇩[0, j] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V :[l] W &
+                                      ⇧[0, j + 1] W ≡ U0 & L ⊢ U0 ⬌* U
+                         ) ∨
+                         (∃∃K,W,V,U0. ⇩[0, j] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W :[l-1] V &
+                                      ⇧[0, j + 1] W ≡ U0 & l > 0 & L ⊢ U0 ⬌* U
+                         ).
+#h #L #T #U #l #H elim H -L -T -U -l
+[ #L #k #j #H destruct
+| #L #K #V #W #U #i #l #HLK #HVW #HWU #_ #j #H destruct /3 width=8/
+| #L #K #W #V #U #i #l #HLK #HWV #HWU #_ #j #H destruct /3 width=8/
+| #I #L #V #W #T #U #l1 #l2 #_ #_ #_ #_ #j #H destruct
+| #L #V #W1 #W2 #T #U #l1 #l2 #_ #_ #_ #_ #j #H destruct
+| #L #V #T #U #W #l #_ #_ #_ #_ #j #H destruct
+| #L #T #U #W #l1 #l2 #_ #_ #_ #_ #j #H destruct
+| #L #T #U1 #U2 #V2 #l #_ #HU12 #_ #IHTU1 #_ #j #H destruct
+  elim (IHTU1 ??) -IHTU1 [4: // |2: skip ] * #K #V #W #U0 #HLK #HVW #HWU0 [2: #H ] #HU01
+  lapply (cpcs_trans … HU01 … HU12) -U1 /3 width=8/
+]
+qed.
+
+lemma snta_inv_lref1: ∀h,L,U,i,l. ⦃h, L⦄ ⊢ #i :[l] U →
+                     (∃∃K,V,W,U0. ⇩[0, i] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V :[l] W &
+                                  ⇧[0, i + 1] W ≡ U0 & L ⊢ U0 ⬌* U
+                     ) ∨
+                     (∃∃K,W,V,U0. ⇩[0, i] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W :[l-1] V &
+                                  ⇧[0, i + 1] W ≡ U0 & l > 0 & L ⊢ U0 ⬌* U
+                     ).
+/2 width=3/ qed-.
+
+fact snta_inv_bind1_aux: ∀h,L,T,U,l. ⦃h, L⦄ ⊢ T :[l] U → ∀J,X,Y. T = ⓑ{J}Y.X →
+                         ∃∃Z1,Z2,l0. ⦃h, L⦄ ⊢ Y :[l0] Z1 &
+                                  ⦃h, L.ⓑ{J}Y⦄ ⊢ X :[l] Z2 &
+                                  L ⊢ ⓑ{J}Y.Z2 ⬌* U.
+#h #L #T #U #l #H elim H -L -T -U -l
+[ #L #k #J #X #Y #H destruct
+| #L #K #V #W #U #i #l #_ #_ #_ #_ #J #X #Y #H destruct
+| #L #K #W #V #U #i #l #_ #_ #_ #_ #J #X #Y #H destruct
+| #I #L #V #W #T #U #l1 #l2 #HVW #HTU #_ #_ #J #X #Y #H destruct /2 width=3/
+| #L #V #W1 #W2 #T #U #l1 #l2 #_ #_ #_ #_ #J #X #Y #H destruct
+| #L #V #T #U #W #l #_ #_ #_ #_ #J #X #Y #H destruct
+| #L #T #U #W #l1 #l2 #_ #_ #_ #_ #J #X #Y #H destruct
+| #L #T #U1 #U2 #V2 #l #_ #HU12 #_ #IHTU1 #_ #J #X #Y #H destruct
+  elim (IHTU1 ????) -IHTU1 [5: // |2,3,4: skip ] #Z1 #Z2 #l0 #HZ1 #HZ2 #HU1
+  lapply (cpcs_trans … HU1 … HU12) -U1 /2 width=3/
+]
+qed.
+
+lemma snta_inv_bind1: ∀h,J,L,Y,X,U,l. ⦃h, L⦄ ⊢ ⓑ{J}Y.X :[l] U →
+                      ∃∃Z1,Z2,l0. ⦃h, L⦄ ⊢ Y :[l0] Z1 & ⦃h, L.ⓑ{J}Y⦄ ⊢ X :[l] Z2 &
+                                  L ⊢ ⓑ{J}Y.Z2 ⬌* U.
+/2 width=3/ qed-.
+
+fact snta_inv_cast1_aux: ∀h,L,T,U,l. ⦃h, L⦄ ⊢ T :[l] U → ∀X,Y. T = ⓝY.X →
+                      ⦃h, L⦄ ⊢ X :[l] Y ∧ L ⊢ Y ⬌* U.
+#h #L #T #U #l #H elim H -L -T -U -l
+[ #L #k #X #Y #H destruct
+| #L #K #V #W #U #i #l #_ #_ #_ #_ #X #Y #H destruct
+| #L #K #W #V #U #i #l #_ #_ #_ #_ #X #Y #H destruct
+| #I #L #V #W #T #U #l1 #l2 #_ #_ #_ #_ #X #Y #H destruct
+| #L #V #W1 #W2 #T #U #l1 #l2 #_ #_ #_ #_ #X #Y #H destruct
+| #L #V #T #U #W #l #_ #_ #_ #_ #X #Y #H destruct
+| #L #T #U #W #l1 #l2 #HTU #_ #_ #_ #X #Y #H destruct /2 width=1/
+| #L #T #U1 #U2 #V2 #l #_ #HU12 #_ #IHTU1 #_ #X #Y #H destruct
+  elim (IHTU1 ???) -IHTU1 [4: // |2,3: skip ] #HXY #HU1
+  lapply (cpcs_trans … HU1 … HU12) -U1 /2 width=1/
+]
+qed.
+
+lemma snta_inv_cast1: ∀h,L,X,Y,U,l. ⦃h, L⦄ ⊢ ⓝY.X :[l] U →
+                      ⦃h, L⦄ ⊢ X :[l] Y ∧ L ⊢ Y ⬌* U.
+/2 width=3/ qed-.
+
+(* Properties on relocation *************************************************)
+
+lemma snta_lift: ∀h,L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 :[l] U1 →
+                 ∀L2,d,e. ⇩[d, e] L2 ≡ L1 →
+                 ∀T2. ⇧[d, e] T1 ≡ T2 → ∀U2. ⇧[d, e] U1 ≡ U2 →
+                 ⦃h, L2⦄ ⊢ T2 :[l] U2.
+#h #L1 #T1 #U1 #l #H elim H -L1 -T1 -U1 -l
+[ #L1 #k #L2 #d #e #HL21 #X1 #H1 #X2 #H2
+  >(lift_inv_sort1 … H1) -X1
+  >(lift_inv_sort1 … H2) -X2 //
+| #L1 #K1 #V1 #W1 #W #i #l #HLK1 #_ #HW1 #IHVW1 #L2 #d #e #HL21 #X #H #U2 #HWU2
+  elim (lift_inv_lref1 … H) * #Hid #H destruct
+  [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // #W2 #HW12 #HWU2
+    elim (ldrop_trans_le … HL21 … HLK1 ?) -L1 /2 width=2/ #X #HLK2 #H
+    elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K2 #V2 #HK21 #HV12 #H destruct
+    /3 width=8/
+  | lapply (lift_trans_be … HW1 … HWU2 ? ?) -W // /2 width=1/ #HW1U2
+    lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/
+  ]
+| #L1 #K1 #W1 #V1 #W #i #l #HLK1 #_ #HW1 #IHWV1 #L2 #d #e #HL21 #X #H #U2 #HWU2
+  elim (lift_inv_lref1 … H) * #Hid #H destruct
+  [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // <minus_plus #W #HW1 #HWU2
+    elim (ldrop_trans_le … HL21 … HLK1 ?) -L1 /2 width=2/ #X #HLK2 #H
+    elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K2 #W2 #HK21 #HW12 #H destruct
+    lapply (lift_mono … HW1 … HW12) -HW1 #H destruct
+    elim (lift_total V1 (d-i-1) e) /3 width=8/
+  | lapply (lift_trans_be … HW1 … HWU2 ? ?) -W // /2 width=1/ #HW1U2
+    lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/
+  ]
+| #I #L1 #V1 #W1 #T1 #U1 #l1 #l2 #_ #_ #IHVW1 #IHTU1 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
+  elim (lift_inv_bind1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H destruct
+  elim (lift_inv_bind1 … H2) -H2 #X #U2 #H1 #HU12 #H2 destruct
+  lapply (lift_mono … H1 … HV12) -H1 #H destruct
+  elim (lift_total W1 d e) /4 width=6/
+| #L1 #V1 #W11 #W12 #T1 #U1 #l1 #l2 #_ #_ #IHVW1 #IHTU1 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
+  elim (lift_inv_flat1 … H1) -H1 #V2 #X #HV12 #H1 #H destruct
+  elim (lift_inv_bind1 … H1) -H1 #W21 #T2 #HW121 #HT12 #H destruct
+  elim (lift_inv_flat1 … H2) -H2 #Y2 #X #HY #H2 #H destruct
+  elim (lift_inv_bind1 … H2) -H2 #W22 #U2 #HW122 #HU12 #H destruct
+  lapply (lift_mono … HY … HV12) -HY #H destruct /4 width=6/
+| #L1 #V1 #T1 #U1 #W1 #l #_ #_ #IHTU1 #IHUW1 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
+  elim (lift_inv_flat1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H destruct
+  elim (lift_inv_flat1 … H2) -H2 #X #U2 #H1 #HU12 #H2 destruct
+  lapply (lift_mono … H1 … HV12) -H1 #H destruct
+  elim (lift_total W1 d e) #W2 #HW12 /4 width=6/
+| #L1 #T1 #U1 #W1 #l1 #l2 #_ #_ #IHTU1 #IHUW1 #L2 #d #e #HL21 #X #H #U2 #HU12
+  elim (lift_inv_flat1 … H) -H #X2 #T2 #HUX2 #HT12 #H destruct
+  lapply (lift_mono … HUX2 … HU12) -HUX2 #H destruct
+  elim (lift_total W1 d e) /3 width=6/
+| #L1 #T1 #U11 #U12 #V12 #l #_ #HU112 #_ #IHTU11 #IHUV12 #L2 #d #e #HL21 #U1 #HTU1 #U2 #HU12
+  elim (lift_total U11 d e) #U #HU11
+  elim (lift_total V12 d e) #V22 #HV122
+  lapply (cpcs_lift … HL21 … HU11 … HU12 HU112) -HU112 /3 width=6/
+]
+qed.
+
+(* Advanced forvard lemmas **************************************************)
+
+fact snta_fwd_pure1_aux: ∀h,L,T,U,l. ⦃h, L⦄ ⊢ T :[l] U → ∀X,Y. T = ⓐY.X →
+                         ∃∃V,W,l0. ⦃h, L⦄ ⊢ Y :[l0+1] W & ⦃h, L⦄ ⊢ X :[l] V &
+                                   L ⊢ ⓐY.V ⬌* U.
+#h #L #T #U #l #H elim H -L -T -U -l
+[ #L #k #X #Y #H destruct
+| #L #K #V #W #U #i #l #_ #_ #_ #_ #X #Y #H destruct
+| #L #K #W #V #U #i #l #_ #_ #_ #_ #X #Y #H destruct
+| #I #L #V #W #T #U #l1 #l2 #_ #_ #_ #_ #X #Y #H destruct
+| #L #V #W1 #W2 #T #U #l1 #l2 #HVW2 #HTU #_ #_ #X #Y #H destruct /2 width=3/
+| #L #V #T #U #W #l #HTU #_ #_ #IHU #X #Y #H destruct
+  elim (IHU U Y ?) -IHU // /3 width=3/
+| #L #T #U #W #l1 #l2 #_ #_ #_ #_ #X #Y #H destruct
+| #L #T #U1 #U2 #V2 #l #_ #HU12 #_ #IHTU1 #_ #X #Y #H destruct
+  elim (IHTU1 ???) -IHTU1 [4: // |2,3: skip ] #V #W #l0 #HYW #HXV #HU1
+  lapply (cpcs_trans … HU1 … HU12) -U1 /2 width=3/
+]
+qed.
+
+lemma snta_fwd_pure1: ∀h,L,X,Y,U,l. ⦃h, L⦄ ⊢ ⓐY.X :[l] U →
+                      ∃∃V,W,l0. ⦃h, L⦄ ⊢ Y :[l0+1] W & ⦃h, L⦄ ⊢ X :[l] V &
+                                L ⊢ ⓐY.V ⬌* U.
+/2 width=3/ qed-.
+
+lemma snta_fwd_correct: ∀h,L,T,U,l. ⦃h, L⦄ ⊢ T :[l] U →
+                        ∃T0. ⦃h, L⦄ ⊢ U :[l-1] T0.
+#h #L #T #U #l #H elim H -L -T -U -l
+[ /2 width=2/
+| #L #K #V #W #W0 #i #l #HLK #_ #HW0 * #V0 #HWV0
+  lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
+  elim (lift_total V0 0 (i+1)) /3 width=10/
+| #L #K #W #V #V0 #i #l #HLK #HWV #HWV0 #_
+  lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
+  elim (lift_total V 0 (i+1)) /3 width=10/
+| #I #L #V #W #T #U #l1 #l2 #HVW #_ #_ * /3 width=3/
+| #L #V #W1 #W2 #T #U #l1 #l2 #HVW2 #_ #_ * #X #H
+  elim (snta_inv_bind1 … H) -H /4 width=5/   
+| /3 width=2/
+| /2 width=2/
+| /2 width=2/
+]
+qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma snta_cast_short: ∀h,L,T,U,l. ⦃h, L⦄ ⊢ T :[l] U → ⦃h, L⦄ ⊢ ⓝU.T :[l] U.
+#h #L #T #U #l #HTU
+elim (snta_fwd_correct … HTU) /2 width=3/
+qed.
+
+lemma snta_typecheck: ∀h,L,T,U,l. ⦃h, L⦄ ⊢ T :[l] U →
+                      ∃T0. ⦃h, L⦄ ⊢ ⓝU.T :[l] T0.
+/3 width=2/ qed.
+
+lemma snta_cast_old: ∀h,L,W,T,U,l.
+                    ⦃h, L⦄ ⊢ T :[l] U → ⦃h, L⦄ ⊢ U :[l-1] W → ⦃h, L⦄ ⊢ ⓝU.T :[l] ⓝW.U.
+#h #L #W #T #U #l #HTU #HUW
+@(snta_conv … U) /2 width=2/ /3 width=1/ (**) (* /4 width=3/ is a bit slow *)
+qed.
+
+lemma snta_appl_old: ∀h,L,V,W,T,U,l1,l2.
+                     ⦃h, L⦄ ⊢ V :[l1+1] W → ⦃h, L⦄ ⊢ T :[l2+1] ⓛW.U →
+                     ⦃h, L⦄ ⊢ ⓐV.T :[l2+1] ⓐV.ⓛW.U.
+#h #L #V #W #T #U #l1 #l2 #HVW #HTU
+elim (snta_fwd_correct … HTU) #X #H
+elim (snta_inv_bind1 … H) -H /4 width=5/
+qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta_ltpr.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta_ltpr.etc
new file mode 100644
index 000000000..77b62e4f4
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta_ltpr.etc
@@ -0,0 +1,278 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/snta_ltpss.ma".
+include "basic_2/dynamic/snta_thin.ma".
+include "basic_2/dynamic/lsubsn_snta.ma".
+
+(* STRATIFIED NATIVE TYPE ASSIGNMENT ON TERMS *******************************)
+(*
+lemma snta_fwd_abst: ∀h,L,W1,W2,T,U,l2. ⦃h, L⦄ ⊢ ⓛW1.T :[l2] ⓛW2.U →
+                     ∃∃V1,V2,l1. ⦃h, L⦄ ⊢ W1 :[l1] V1 & ⦃h, L⦄ ⊢ W2 :[l1] V2 &
+                                 L ⊢ W1 ⬌* W2.
+#h #L #W1 #W2 #T #U #l2 #HTU
+elim (snta_fwd_correct … HTU) #X #H
+elim (snta_inv_bind1 … H) -H #W #T0 #l #HW2 #_ #_ -X
+elim (snta_inv_bind1 … HTU) -HTU #V1 #U0 #l0 #HWV1 #_ #H
+elim (cpcs_inv_abst … H Abst W1) -H
+#HW12 #_ -U0
+@(ex3_3_intro … HWV1 … HW12)
+[3: @(snta_conv … HTU0 HU0) 
+
+ /3 width=3/
+
+*)
+(*
+#h #L #V #T #U #l2 #HTU
+elim (snta_fwd_correct … HTU) #X #H
+elim (snta_inv_bind1 … H) -H #W #T0 #l1 #HVW #HUT0 #_ -X
+elim (snta_inv_bind1 … HTU) -HTU #W0 #U0 #l0 #_ #HTU0 #H -l0
+elim (cpcs_inv_abst … H Abst V) -H /3 width=3/
+qed-.
+*)
+(*
+lemma snta_fwd_appl1_sound_aux: ∀h,l0. (∀L1,L2,T1,T2,U,l.
+                                        l < l0 → ⦃h, L1⦄ ⊢ T1 :[l] U →
+                                        L1 ➡ L2 → L2 ⊢ T1 ➡* T2 → ⦃h, L2⦄ ⊢ T2 :[l] U
+                                       ) →
+                                ∀L,T,U,l2. ⦃h, L⦄ ⊢ T :[l2] U →
+                                ∀Z,Y,X1. T = ⓐZ.ⓛY.X1 → l0 = l2 →
+                                ∃l1. ⦃h, L⦄ ⊢ Z :[l1+1] Y.
+#h #l0 #IH #L #T #U #l2 #H elim H -L -T -U -l2
+[
+|
+|
+|
+| #L #V #W1 #W2 #T #U #l1 #l2 #HVW2 #HTU #_ #_ #Z #Y #X1 #H1 #H2 destruct -IH
+  elim (snta_fwd_abst … HTU) -X1 -U -l2 #Y0 #W0 #l0 #HY0 #H1 #HYW2
+  elim (snta_fwd_correct … HVW2) #W #H2
+  elim (snta_mono … H1 … H2) -H1 -H2 #H #_ destruct -W0 -W /4 width=6/
+| #L #V #T #U #W #l #HTU #HUW #Z #Y #X1 #X2 #H1 #H2 #H3 destruct
+  elim (snta_inv_abst_sn … HTU) -HTU #Y0 #l0 #HY0 #HX12
+|
+| #L #T #U1 #U2 #V2 #l #HTU1 #HU12 #HUV2 #Z #Y #X1 #X2 #H1 #H2 #H3 destruct
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+lemma snta_inv_appl_aux: ∀h,l0. (∀L1,L2,T1,T2,U,l.
+                                 l < l0 + 1 → ⦃h, L1⦄ ⊢ T1 :[l] U →
+                                 L1 ➡ L2 → L2 ⊢ T1 ➡* T2 → ⦃h, L2⦄ ⊢ T2 :[l] U
+                                ) →
+                         ∀L,T,U,l2. ⦃h, L⦄ ⊢ T :[l2] U →
+                         ∀Z,Y,X1,X2. T = ⓐZ.ⓛY.X1 → U = ⓐZ.ⓛY.X2 → l0 = l2 →
+                         ∃∃l1. ⦃h, L⦄ ⊢ Z :[l1+1] Y & ⦃h, L.ⓛY⦄ ⊢ X1 :[l2] X2.
+#h #l0 #IH #L #T #U #l2 * -L -T -U -l2
+[
+|
+|
+|
+| #L #V #W1 #W2 #T #U #l1 #l2 #HVW2 #HTU #Z #Y #X1 #X2 #H1 #H2 #H3 destruct -IH
+  elim (snta_inv_abst … HTU) -HTU /2 width=2/
+| #L #V #T #U #W #l #HTU #HUW #Z #Y #X1 #X2 #H1 #H2 #H3 destruct
+  elim (snta_inv_abst … HTU) -HTU #Y0 #l0 #HY0 #HX12
+|
+| #L #T #U1 #U2 #V2 #l #HTU1 #HU12 #HUV2 #Z #Y #X1 #X2 #H1 #H2 #H3 destruct
+  
+   /2 width=2/
+
+
+axiom pippo: ∀h,l0. (∀L1,L2,T1,T2,U,l.
+                l < l0 + 1 → ⦃h, L1⦄ ⊢ T1 :[l] U →
+                L1 ➡ L2 → L2 ⊢ T1 ➡* T2 → ⦃h, L2⦄ ⊢ T2 :[l] U
+             ) →
+             ∀L,T1,U1,l. ⦃h, L⦄ ⊢ T1 :[l] U1 →
+             ∀V2,W2,T2. L ⊢ T1 ➡* ⓐV2.ⓛW2.T2 → l0 = l →
+             ∃l0. ⦃h, L2⦄ ⊢ V2 :[l0+1] W2.
+(*
+#h #l #IH #L1 #T1 #U1 #l1 * -L1 -T1 -U1 -l1
+[
+|
+|
+|
+| #L1 #V1 #W1 #T1 #U1 #l1 #HVW1 #HTU1 #Y1 #X1 #H1 #L2 #Y2 #HL12 #HY12 #Z2 #X2 #HX12 #H2 destruct
+  elim (IH ??? Y2 … HVW1 HL12 ?) -HVW1 // [2: /3 width=1/ ] -HY12 #l21 #HY2W1 #H1l21 #H2l21
+  elim (IH … HTU1 HL12 HX12) -IH -HTU1 -HL12 -HX12 // #l22 #H #_ #H2l22
+  elim (snta_inv_bind1 … H) -H #Z #X #HZ2 #_ #H
+  elim (cpcs_inv_abst … H Abst W1) -H #H #_
+  lapply (transitive_le … (l21+l22) … H1l21 ?) -H1l21 // #Hl21
+  @(ex3_1_intro … Hl21) [2: /3 width=1/ ]
+  @(snta_conv … W1) /2 width=2/ (**) (* explicit constructors *)
+| #L1 #V1 #T1 #U1 #W1 #l1 #HTU1 #HUW1 #Y1 #X1 #H1 #L2 #Y2 #HL12 #HY12 #Z2 #X2 #HX12 #H2 destruct
+
+*)
+(* Properties on context-free parallel reduction for local environments *****)
+*)
+fact snta_ltpr_tpr_conf_aux: ∀h,l0. (∀L1,L2,T1,T2,U,l.
+                                l < l0 → ⦃h, L1⦄ ⊢ T1 :[l] U →
+                                L1 ➡ L2 → L2 ⊢ T1 ➡* T2 → ⦃h, L2⦄ ⊢ T2 :[l] U
+                             ) →
+                             ∀L1,T1,U,l. ⦃h, L1⦄ ⊢ T1 :[l] U → ∀L2. L1 ➡ L2 →
+                             ∀T2. T1 ➡ T2 → l0 = l → ⦃h, L2⦄ ⊢ T2 :[l] U.
+#h #l0 #IH #L1 #T1 #U #l #H elim H -L1 -T1 -U -l
+[ #L1 #k1 #L2 #_ #T2 #H #_ -l0
+  >(tpr_inv_atom1 … H) -H //
+| #L1 #K1 #V1 #W #U #i1 #l #HLK1 #_ #HWU #IHV1 #L2 #HL12 #T2 #H #Hl -IH
+  >(tpr_inv_atom1 … H) -T2
+  elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #HLK2 #H
+  elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct /3 width=6/
+| #L1 #K1 #W1 #V1 #U1 #i1 #l #HLK1 #HWV1 #HWU1 #IHWV1 #L2 #HL12 #T2 #H #Hl -IH
+(*  
+  >(tpr_inv_atom1 … H) -T2
+  elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #HLK2 #H
+  elim (ltpr_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct
+  lapply (ldrop_fwd_ldrop2 … HLK2) #HLK
+  elim (lift_total V1 0 (i+1)) #W #HW
+  lapply (snta_lift h … HLK … HWU1 … HW) /2 width=1/ -HLK -HW
+  elim (lift_total W2 0 (i+1)) #U2 #HWU2
+  lapply (tpr_lift … HW12 … HWU1 … HWU2) -HWU1 #HU12
+  @(snta_conv … U2) /2 width=1/ /3 width=6/ (**) (* explicit constructor, /3 width=6/ is too slow *)
+*)
+| #I #L1 #V1 #W1 #T1 #U1 #l1 #l2 #_ #_ #IHVW1 #IHTU1 #L2 #HL12 #X #H #Hl -IH
+(*  
+  elim (tpr_inv_bind1 … H) -H *
+  [ #V2 #T #T2 #HV12 #HT1 #HT2 #H destruct
+    lapply (IHVW1 … HL12 … HV12) #HV2W1
+    lapply (IHVW1 L2 … V1 ?) // -IHVW1 #HWV1
+    lapply (IHTU1 (L2.ⓑ{I}V2) … HT1) -HT1 /2 width=1/ #HTU1
+    lapply (IHTU1 (L2.ⓑ{I}V1) ? T1 ?) -IHTU1 // /2 width=1/ -HL12 #H
+    lapply (tps_lsubs_trans … HT2 (L2.ⓑ{I}V2) ?) -HT2 /2 width=1/ #HT2
+    lapply (snta_tps_conf … HTU1 … HT2) -T #HT2U1
+    elim (snta_fwd_correct … H) -H #U2 #HU12
+    @(snta_conv … (ⓑ{I}V2.U1)) /2 width=2/ /3 width=1/ (**) (* explicit constructor, /4 width=6/ is too slow *)
+  | #T #HT1 #HTX #H destruct
+    lapply (IHVW1 … HL12 V1 ?) -IHVW1 // #HVW1
+    lapply (IHTU1 (L2.ⓓV1) … HT1) -T1 /2 width=1/ -L1 #H
+    elim (snta_fwd_correct … H) #T1 #HUT1
+    elim (snta_ldrop_conf … H L2 0 1 ? ?) -H // /2 width=1/ #T0 #U0 #HTU0 #H #HU10
+    lapply (delift_inv_lift1_eq … H L2 … HTX) -H -HTX /2 width=1/ #H destruct
+    @(snta_conv … HTU0) /2 width=2/
+  ]
+*)
+| #L1 #V1 #W11 #W2 #T1 #U1 #l1 #l2 #_ #_ #IHVW1 #IHTU1 #L2 #HL12 #X #H #Hl -IH
+(*
+  elim (tpr_inv_appl1 … H) -H *
+  [ #V2 #Y #HV12 #HY #H destruct
+    elim (tpr_inv_abst1 … HY) -HY #W2 #T2 #HW12 #HT12 #H destruct
+    lapply (IHTU1 L2 ? (ⓛW1.T1) ?) // #H
+    elim (snta_fwd_correct … H) -H #X #H
+    elim (snta_inv_bind1 … H) -H #W #U #HW #HU #_
+    @(snta_conv … (ⓐV2.ⓛW1.U1)) /4 width=2/ (**) (* explicit constructor, /5 width=5/ is too slow *)
+  | #V2 #W2 #T0 #T2 #HV12 #HT02 #H1 #H2 destruct
+    lapply (IHVW1 … HL12 … HV12) #HVW2
+    lapply (IHVW1 … HL12 V1 ?) -IHVW1 // #HV1W2
+    lapply (IHTU1 … HL12 (ⓛW2.T2) ?) -IHTU1 -HL12 /2 width=1/ -HT02 #H1
+    elim (snta_fwd_correct … H1) #T #H2
+    elim (snta_inv_bind1 … H1) -H1 #W #U2 #HW2 #HTU2 #H
+    elim (cpcs_inv_abst … H Abst W2) -H #_ #HU21
+    elim (snta_inv_bind1 … H2) -H2 #W0 #U0 #_ #H #_ -T -W0
+    lapply (lsubsn_snta_trans … HTU2 (L2.ⓓV2) ?) -HTU2 /2 width=1/ #HTU2
+    @(snta_conv … (ⓓV2.U2)) /2 width=2/ /3 width=2/ (**) (* explicit constructor, /4 width=5/ is too slow *)
+  | #V0 #V2 #W0 #W2 #T0 #T2 #_ #_ #_ #_ #H destruct
+  ]
+*)
+| #L1 #V1 #T1 #U1 #W1 #l #_ #HUW1 #IHTU1 #_ #L2 #HL12 #X #H #Hl
+  elim (tpr_inv_appl1 … H) -H *
+  [ #V2 #T2 #HV12 #HT12 #H destruct
+    lapply (cpr_tpr … HV12 L2) #HV
+    elim (snta_fwd_correct h L2 (ⓐV1.T1) (ⓐV1.U1) (l+1) ?) [2: /3 width=6/ ] #U
+    @(snta_conv … (ⓐV2.U1)) /2 width=1/ -HV12 /4 width=8 by snta_pure, cprs_flat_dx/ (**) (* explicit constructor, /4 width=8/ is too slow without trace *)
+  | #V2 #W0 #T0 #T2 #HV12 #HT02 #H1 #H2 destruct
+    lapply (IHTU1 … HL12 (ⓛW0.T2) ? ?) -IHTU1 // /2 width=1/ -T0 #H1
+    lapply (IH … (ⓐV2.U1) … HUW1 HL12 ?) // /3 width=1/ #H2
+    lapply (snta_pure … H1 H2) -H2 #H
+    elim (snta_inv_bind1 … H1) -H1 #V0 #U2 #l1 #HWV0 #HTU2 #HU21
+    @(snta_conv … (ⓓV2.U2)) (**) (* explicit constructor *)
+    [2:
+(*
+        @snta_bind /3 width=2/ /3 width=6/ (**) (* /4 width=6/ is a bit slow *)
+*)
+    |3: @(cpcs_cpr_conf … (ⓐV1.ⓛW0.U2)) /2 width=1/
+    |4: /2 width=5/
+    | skip
+    ]
+(*
+    elim (snta_fwd_pure1 … H) -H #T1 #W2 #HVW2 #HUT1 #HTW1
+
+    elim (cpcs_inv_abst1 … HU21) #W3 #U3 #HU13 #H
+    elim (cprs_inv_abst … H Abst W0) -H #HW03 #_
+    elim (pippo … IH … HUW1 ? V2 W3 U3 HL12 ? ?) -IH -HUW1 -HL12 // /3 width=1/ -HU13 #l2 #HV2W3
+    lapply (snta_conv h L2 V2 W3 W0 V0 (l1+1) ? ? ?) /2 width=1/ -HV2W3 -HW03 -HWV0 #HV2W0    
+*)    
+(* SEGMENT 1.5
+    lapply (IH … HV1 … HL12 … HV12) -HV1 -HV12 /width=5/ #HB
+    lapply (IH … HB0  … HL12 W2 ?) -HB0 /width=5/ #HB0
+    lapply (IH … HA0 … (L2.ⓛW2) … HT02) -IH -HA0 -HT02 /width=5/ -T0 /2 width=1/ -L1 -V1 /4 width=7/
+    
+axiom pippo: ⦃h, L⦄ ⊢ ⓐV.X : Y →
+             ∃∃W,T. L ⊢ X ➡* ⓛW.T & ⦃h, L⦄ ⊢ ⓐV : W.
+
+*)
+(* SEGMENT 2
+| #L1 #T1 #U1 #W1 #_ #_ #IHTU1 #IHUW1 #L2 #d #e #HL12 #X #H
+  elim (tpss_inv_flat1 … H) -H #U2 #T2 #HU12 #HT12 #H destruct
+  lapply (cpr_tpss … HU12) /4 width=4/
+| #L1 #T1 #U11 #U12 #U #_ #HU112 #_ #IHTU11 #IHU12 #L2 #d #e #HL12 #T2 #HT12
+  @(snta_conv … U11) /2 width=5/ (**) (* explicot constructor, /3 width=7/ is too slow *)
+]
+qed.
+*)
+
+(* SEGMENT 3
+fact snta_ltpr_tpr_conf_aux: ∀h,L,T,L1,T1,U. ⦃h, L1⦄ ⊢ T1 : U → L = L1 → T = T1 →
+                            ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → ⦃h, L2⦄ ⊢ T2 : U.
+  
+  
+  | #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HW02 #HT02 #HV02 #H1 #H2 destruct
+    elim (snta_inv_abbr … HT1) -HT1 #B0 #HW0 #HT0
+    lapply (IH … HW0  … HL12 … HW02) -HW0 /width=5/ #HW2
+    lapply (IH … HV1 … HL12 … HV10) -HV1 -HV10 /width=5/ #HV0
+    lapply (IH … HT0 … (L2.ⓓW2) … HT02) -IH -HT0 -HT02 /width=5/ -V1 -T0 /2 width=1/ -L1 -W0 #HT2
+    @(snta_abbr … HW2) -HW2
+    @(snta_appl … HT2) -HT2 /3 width=7/ (**) (* explict constructors, /5 width=7/ is too slow *)
+  ]
+| #L1 #V1 #T1 #A #HV1 #HT1 #H1 #H2 #L2 #HL12 #X #H destruct
+  elim (tpr_inv_cast1 … H) -H
+  [ * #V2 #T2 #HV12 #HT12 #H destruct
+    lapply (IH … HV1 … HL12 … HV12) -HV1 -HV12 /width=5/ #HV2
+    lapply (IH … HT1 … HL12 … HT12) -IH -HT1 -HL12 -HT12 /width=5/ -L1 -V1 -T1 /2 width=1/
+  | -HV1 #HT1X
+     lapply (IH … HT1 … HL12 … HT1X) -IH -HT1 -HL12 -HT1X /width=5/
+  ]
+]
+qed.
+
+lemma snta_ltpr_tpr_conf: ∀h,L1,T1,U. ⦃h, L1⦄ ⊢ T1 : U → ∀L2. L1 ➡ L2 →
+                         ∀T2. T1 ➡ T2 → ⦃h, L2⦄ ⊢ T2 : U.
+
+/2 width=9/ qed.
+
+axiom snta_ltpr_conf: ∀L1,T,A. L1 ⊢ T : A → ∀L2. L1 ➡ L2 → L2 ⊢ T : A.
+/2 width=5/ qed.
+
+axiom snta_tpr_conf: ∀L,T1,A. L ⊢ T1 : A → ∀T2. T1 ➡ T2 → L ⊢ T2 : A.
+/2 width=5/ qed.
+*)
+*)*)
\ No newline at end of file
diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta_ltpss.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta_ltpss.etc
new file mode 100644
index 000000000..0e5f3930e
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta_ltpss.etc
@@ -0,0 +1,123 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/equivalence/cpcs_ltpss.ma".
+include "basic_2/dynamic/snta_snta.ma".
+
+(* STRATIFIED NATIVE TYPE ASSIGNMENT ON TERMS *******************************)
+
+(* Properties about parallel unfold *****************************************)
+
+lemma snta_ltpss_tpss_conf: ∀h,L1,T1,U,l. ⦃h, L1⦄ ⊢ T1 :[l] U →
+                            ∀L2,d,e. L1 ▶* [d, e] L2 →
+                            ∀T2. L2 ⊢ T1 ▶* [d, e] T2 → ⦃h, L2⦄ ⊢ T2 :[l] U.
+#h #L1 #T1 #U #l #H elim H -L1 -T1 -U -l
+[ #L1 #k #L2 #d #e #_ #T2 #H
+  >(tpss_inv_sort1 … H) -H //
+| #L1 #K1 #V1 #W #U #i #l #HLK1 #_ #HWU #IHV1 #L2 #d #e #HL12 #T2 #H
+  elim (tpss_inv_lref1 … H) -H
+  [ #H destruct
+    elim (lt_or_ge i d) #Hdi
+    [ elim (ltpss_ldrop_conf_le … HL12 … HLK1 ?) -L1 /2 width=2/ #X #H #HLK2
+      elim (ltpss_inv_tpss11 … H ?) -H /2 width=1/ -Hdi #K2 #V2 #HK12 #HV12 #H destruct
+      /3 width=7/
+    | elim (lt_or_ge i (d + e)) #Hide [ | -Hdi ]
+      [ elim (ltpss_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HLK2
+        elim (ltpss_inv_tpss21 … H ?) -H /2 width=1/ -Hdi -Hide #K2 #V2 #HK12 #HV12 #H destruct
+        /3 width=7/
+      | lapply (ltpss_ldrop_conf_ge … HL12 … HLK1 ?) -L1 // -Hide /3 width=7/
+      ]
+    ]
+  | * #K2 #V2 #W2 #Hdi #Hide #HLK2 #HVW2 #HWT2
+    elim (ltpss_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HL2K0
+    elim (ltpss_inv_tpss21 … H ?) -H /2 width=1/ -Hdi -Hide #K0 #V0 #HK12 #HV12 #H destruct
+    lapply (ldrop_mono … HL2K0 … HLK2) -HL2K0 #H destruct
+    lapply (ldrop_fwd_ldrop2 … HLK2) -HLK2 #HLK2
+    lapply (tpss_trans_eq … HV12 HVW2) -V2 /3 width=9/
+  ]
+| #L1 #K1 #W1 #V1 #U1 #i #l #HLK1 #HWV1 #HWU1 #IHWV1 #L2 #d #e #HL12 #T2 #H
+  elim (tpss_inv_lref1 … H) -H [ | -HWV1 -HWU1 -IHWV1 ]
+  [ #H destruct
+    elim (lift_total V1 0 (i+1)) #W #HW
+    elim (lt_or_ge i d) #Hdi [ -HWV1 ]
+    [ elim (ltpss_ldrop_conf_le … HL12 … HLK1 ?) -L1 /2 width=2/ #X #H #HLK2
+      elim (ltpss_inv_tpss11 … H ?) -H /2 width=1/ -Hdi #K2 #W2 #HK12 #HW12 #H destruct
+      lapply (ldrop_fwd_ldrop2 … HLK2) #HLK
+      lapply (snta_lift h … HLK … HWU1 … HW) [ /2 width=4/ | skip ] -HW #H
+      elim (lift_total W2 0 (i+1)) #U2 #HWU2
+      lapply (tpss_lift_ge … HW12 … HLK … HWU1 … HWU2) -HLK -HWU1 // #HU12
+      lapply (cpr_tpss … HU12) -HU12 #HU12
+      @(snta_conv … U2) // /2 width=1/ /3 width=6/ (**) (* explicit constructor, /4 width=6/ is too slow *)
+    | elim (lt_or_ge i (d + e)) #Hide [ -HWV1 | -IHWV1 -HW -Hdi ]
+      [ elim (ltpss_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HLK2
+        elim (ltpss_inv_tpss21 … H ?) -H /2 width=1/ -Hdi -Hide #K2 #W2 #HK12 #HW12 #H destruct
+        lapply (ldrop_fwd_ldrop2 … HLK2) #HLK
+        lapply (snta_lift h … HLK … HWU1 … HW) [ /2 width=4/ | skip ] -HW #H
+        elim (lift_total W2 0 (i+1)) #U2 #HWU2
+        lapply (tpss_lift_ge … HW12 … HLK … HWU1 … HWU2) -HLK -HWU1 // #HU12
+        lapply (cpr_tpss … HU12) -HU12 #HU12
+        @(snta_conv … U2) // /2 width=1/ /3 width=6/ (**) (* explicit constructor, /4 width=6/ is too slow *)
+      | lapply (ltpss_ldrop_conf_ge … HL12 … HLK1 ?) -L1 // -Hide /2 width=6/
+      ]
+    ]
+  | * #K2 #V2 #W2 #Hdi #Hide #HLK2 #_ #_
+    elim (ltpss_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HL2K0
+    elim (ltpss_inv_tpss21 … H ?) -H /2 width=1/ -Hdi -Hide #K0 #V0 #_ #_ #H destruct
+    lapply (ldrop_mono … HL2K0 … HLK2) -HL2K0 -HLK2 #H destruct
+  ]
+| #I #L1 #V1 #W1 #T1 #U1 #l1 #l2 #_ #_ #IHVW1 #IHTU1 #L2 #d #e #HL12 #X #H
+  elim (tpss_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
+  lapply (cpr_tpss … HV12) #HV
+  lapply (IHTU1 (L2.ⓑ{I}V1) (d+1) e ? T1 ?) // /2 width=1/ #H
+  elim (snta_fwd_correct … H) -H #U2 #HU12
+  @(snta_conv … (ⓑ{I}V2.U1)) /3 width=2/ /3 width=4/ /4 width=4/ (**) (* explicit constructor, /5 width=6/ is too slow *)
+| #L1 #V1 #W11 #W12 #T1 #U1 #l1 #l2 #_ #_ #IHVW1 #IHTU1 #L2 #d #e #HL12 #X #H
+  elim (tpss_inv_flat1 … H) -H #V2 #Y #HV12 #HY #H destruct
+  elim (tpss_inv_bind1 … HY) -HY #W21 #T2 #HW121 #HT12 #H destruct
+  lapply (cpr_tpss … HV12) #HVV12
+  lapply (IHTU1 L2 d e ? (ⓛW21.T2) ?) -IHTU1 // /2 width=1/ -HW121 -HT12 #H0
+  elim (snta_fwd_correct … H0) #X #H
+  elim (snta_inv_bind1 … H) -H #W #U #l0 #HW #HU #_
+  @(snta_conv … (ⓐV2.ⓛW12.U1)) /3 width=2/ /3 width=4/ /3 width=5/ (**) (* explicit constructor, /4 width=5/ is too slow *)
+| #L1 #V1 #T1 #U1 #W1 #l #_ #_ #IHTU1 #IHUW1 #L2 #d #e #HL12 #X #H
+  elim (tpss_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
+  lapply (cpr_tpss … HV12) #HV
+  elim (snta_fwd_correct h L2 (ⓐV1.T1) (ⓐV1.U1) (l+1) ?) [2: /3 width=4/ ] #U
+  @(snta_conv … (ⓐV2.U1)) /3 width=1/ /4 width=5/ (**) (* explicit constructor, /5 width=5/ is too slow *)
+| #L1 #T1 #U1 #W1 #l1 #l2 #HTU1 #HUW1 #IHTU1 #IHUW1 #L2 #d #e #HL12 #X #H
+  elim (snta_fwd_correct … HTU1) -HTU1 #U #H
+  elim (snta_mono … HUW1 … H) -HUW1 -H #H #_ -U destruct
+  elim (tpss_inv_flat1 … H) -H #U2 #T2 #HU12 #HT12 #H destruct
+  lapply (cpr_tpss … HU12) #HU /4 width=4/
+| #L1 #T1 #U11 #U12 #U #l #_ #HU112 #_ #IHTU11 #IHU12 #L2 #d #e #HL12 #T2 #HT12
+  @(snta_conv … U11) /2 width=5/ (**) (* explicit constructor, /3 width=7/ is too slow *)
+]
+qed.
+
+lemma snta_ltpss_tps_conf: ∀h,L1,T1,U,l. ⦃h, L1⦄ ⊢ T1 :[l] U →
+                           ∀L2,d,e. L1 ▶* [d, e] L2 →
+                           ∀T2. L2 ⊢ T1 ▶ [d, e] T2 → ⦃h, L2⦄ ⊢ T2 :[l] U.
+/3 width=7/ qed.
+
+lemma snta_ltpss_conf: ∀h,L1,T,U,l. ⦃h, L1⦄ ⊢ T :[l] U →
+                       ∀L2,d,e. L1 ▶* [d, e] L2 → ⦃h, L2⦄ ⊢ T :[l] U.
+/2 width=7/ qed.
+
+lemma snta_tpss_conf: ∀h,L,T1,U,l. ⦃h, L⦄ ⊢ T1 :[l] U →
+                      ∀T2,d,e. L ⊢ T1 ▶* [d, e] T2 → ⦃h, L⦄ ⊢ T2 :[l] U.
+/2 width=7/ qed.
+
+lemma snta_tps_conf: ∀h,L,T1,U,l. ⦃h, L⦄ ⊢ T1 :[l] U →
+                     ∀T2,d,e. L ⊢ T1 ▶ [d, e] T2 → ⦃h, L⦄ ⊢ T2 :[l] U.
+/2 width=7/ qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta_snta.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta_snta.etc
new file mode 100644
index 000000000..db71e1192
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta_snta.etc
@@ -0,0 +1,65 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/snta_lift.ma".
+
+(* STRATIFIED NATIVE TYPE ASSIGNMENT ON TERMS *******************************)
+
+(* Main properties **********************************************************)
+
+theorem snta_mono: ∀h,L,T,U1,l1. ⦃h, L⦄ ⊢ T :[l1] U1 →
+                   ∀U2,l2. ⦃h, L⦄ ⊢ T :[l2] U2 → l1 = l2 ∧ L ⊢ U1 ⬌* U2.
+#h #L #T #U1 #l1 #H elim H -L -T -U1 -l1
+[ #L #k #X #l2 #H
+  lapply (snta_inv_sort1 … H) -H * /2 width=1/
+| #L #K #V #W11 #W12 #i #l1 #HLK #_ #HW112 #IHVW11 #X #l2 #H
+  elim (snta_inv_lref1 … H) -H * #K0 #V0 #W21 #W22 #HLK0 #HVW21 #HW212 #HX
+  lapply (ldrop_mono … HLK0 … HLK) -HLK0 #H destruct
+  lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
+  elim (IHVW11 … HVW21) -IHVW11 -HVW21 #Hl12 #HW121
+  lapply (cpcs_lift … HLK … HW112 … HW212 ?) // -K -W11 -W21 /3 width=3/
+| #L #K #W #V1 #V #i #l1 #HLK #_ #HWV #IHWV1 #X #l2 #H
+  elim (snta_inv_lref1 … H) -H * #K0 #W0 #V2 #V0 #HLK0 #HW0V2 #HWV0 [2: #HL2 ] #HX
+  lapply (ldrop_mono … HLK0 … HLK) -HLK0 -HLK #H destruct
+  lapply (lift_mono … HWV0 … HWV) -HWV0 -HWV #H destruct
+  elim (IHWV1 … HW0V2) -IHWV1 -HW0V2 /3 width=1/
+| #I #L #V #W1 #T #U1 #l10 #l1 #_ #_ #_ #IHTU1 #X #l2 #H
+  elim (snta_inv_bind1 … H) -H #W2 #U2 #l20 #_ #HTU2 #H
+  elim (IHTU1 … HTU2) -IHTU1 -HTU2 #Hl12 #HU12
+  lapply (cpcs_trans … (ⓑ{I}V.U1) … H) -H /2 width=1/
+| #L #V #W #W1 #T #U1 #l10 #l1 #_ #_ #_ #IHTU1 #X #l2 #H
+  elim (snta_fwd_pure1 … H) -H #U2 #W2 #l20 #_ #HTU2 #H
+  elim (IHTU1 … HTU2) -IHTU1 -HTU2 #Hl12 #HU12
+  lapply (cpcs_trans … (ⓐV.ⓛW1.U1) … H) -H /2 width=1/
+| #L #V #T #U1 #W1 #l1 #_ #_ #IHTU1 #_ #X #l2 #H
+  elim (snta_fwd_pure1 … H) -H #U2 #W2 #l20 #_ #HTU2 #H
+  elim (IHTU1 … HTU2) -IHTU1 -HTU2 #Hl12 #HU12
+  lapply (cpcs_trans … (ⓐV.U1) … H) -H /2 width=1/
+| #L #T #U1 #W1 #l10 #l1 #_ #_ #IHTU1 #_ #X #l2 #H
+  elim (snta_inv_cast1 … H) -H #HTU1
+  elim (IHTU1 … HTU1) -IHTU1 -HTU1 /2 width=1/
+| #L #T #U11 #U12 #V12 #l1 #_ #HU112 #_ #IHTU11 #_ #U2 #l2 #HTU2
+  elim (IHTU11 … HTU2) -IHTU11 -HTU2 #Hl12 #H
+  lapply (cpcs_canc_sn … HU112 … H) -U11 /2 width=1/
+]
+qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma snta_cast_alt: ∀h,L,T,W,U,l. ⦃h, L⦄ ⊢ T :[l] W → ⦃h, L⦄ ⊢ T :[l] U →
+             ⦃h, L⦄ ⊢ ⓝW.T :[l] U.
+#h #L #T #W #U #l #HTW #HTU
+elim (snta_mono … HTW … HTU) #_ #HWU
+elim (snta_fwd_correct … HTU) -HTU /3 width=3/
+qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta_thin.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta_thin.etc
new file mode 100644
index 000000000..ceb5375bf
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta_thin.etc
@@ -0,0 +1,116 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/thin_ldrop.ma".
+include "basic_2/equivalence/cpcs_delift.ma".
+include "basic_2/dynamic/snta_lift.ma".
+
+(* STRATIFIED NATIVE TYPE ASSIGNMENT ON TERMS *******************************)
+
+(* Properties on basic local environment thinning ***************************)
+
+(* Note: this is known as the substitution lemma *)
+lemma snta_thin_conf: ∀h,L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 :[l] U1 →
+                      ∀L2,d,e. ≽ [d, e] L1 → L1 ▼*[d, e] ≡ L2 →
+                      ∃∃T2,U2. ⦃h, L2⦄ ⊢ T2 :[l] U2 &
+                               L1 ⊢ T1 ▼*[d, e] ≡ T2 & L1 ⊢ U1 ▼*[d, e] ≡ U2.
+#h #L1 #T1 #U1 #l #H elim H -L1 -T1 -U1 -l
+[ /2 width=5/
+| #L1 #K1 #V1 #W1 #U1 #i #l #HLK1 #HVW1 #HWU1 #IHVW1 #L2 #d #e #HL1 #HL12
+  elim (lt_or_ge i d) #Hdi [ -HVW1 ]
+  [ lapply (sfr_ldrop_trans_ge … HLK1 … HL1 ?) -HL1 /2 width=2/ #H
+    lapply (sfr_inv_skip … H ?) -H /2 width=1/ #HK1
+    elim (thin_ldrop_conf_le … HL12 … HLK1 ?) -HL12 /2 width=2/ #X #H #HLK2
+    elim (thin_inv_delift1 … H ?) -H /2 width=1/ #K2 #V2 #HK12 #HV12 #H destruct
+    elim (IHVW1 … HK1 HK12) -IHVW1 -HK1 -HK12 #X2 #W2 #HVW2 #H #HW12
+    lapply (delift_mono … H … HV12) -H -HV12 #H destruct
+    elim (lift_total W2 0 (i+1)) #U2 #HWU2
+    lapply (ldrop_fwd_ldrop2 … HLK1) -V1 #HLK1
+    lapply (delift_lift_ge … HW12 … HLK1 HWU1 … HWU2) -HW12 -HLK1 -HWU1 //
+    >minus_plus <plus_minus_m_m // /3 width=6/
+  | elim (lt_or_ge i (d+e)) #Hide [ -HVW1 | -Hdi -IHVW1 -HL1 ]
+    [ lapply (sfr_ldrop_trans_be_up … HLK1 … HL1 ? ?) -HL1 // /2 width=2/ <minus_n_O #H
+      elim (sfr_inv_bind … H ?) -H /2 width=1/ #HK1 #_
+      elim (thin_ldrop_conf_be … HL12 … HLK1 ? ?) -HL12 /2 width=2/ #K2 #H #HLK2
+      lapply (thin_inv_thin1 … H ?) -H /2 width=1/ #HK12
+      elim (IHVW1 … HK1 HK12) -IHVW1 -HK1 -HK12 #V2 #W2 #HVW2 #HV12 #HW12
+      elim (lift_total V2 0 d) #T2 #HVT2
+      elim (lift_total W2 0 d) #U2 #HWU2
+      elim (lift_total W2 0 (i+1)) #U #HW2U
+      lapply (snta_lift … HVW2 … HLK2 … HVT2 … HWU2) -HVW2 -HLK2 #HTU2
+      lapply (ldrop_fwd_ldrop2 … HLK1) #HLK0
+      lapply (delift_lift_ge … HW12 … HLK0 HWU1 … HW2U) -HW12 -HLK0 -HWU1 // >minus_plus #HU1
+      lapply (lift_conf_be … HWU2 … HW2U ?) -W2 /2 width=1/ #HU2
+      lapply (delift_lift_div_be … HU1 … HU2 ? ?) -U // /2 width=1/ /3 width=8/
+    | lapply (transitive_le … (i+1) Hide ?) /2 width=1/ #Hdei
+      lapply (thin_ldrop_conf_ge … HL12 … HLK1 ?) -HL12 -HLK1 // #HL2K1
+      elim (lift_split … HWU1 d (i+1-e) ? ? ?) -HWU1 // /2 width=1/ #W
+      <plus_minus in ⊢ (??%??→?); /2 width=2/ #HW1
+      <minus_minus // /2 width=2/ -Hdei >commutative_plus <minus_n_n /3 width=6/
+    ]
+  ]
+| #L1 #K1 #W1 #V1 #U1 #i #l #HLK1 #HWV1 #HWU1 #IHWV1 #L2 #d #e #HL1 #HL12
+  elim (lt_or_ge i d) #Hdi [ -HWV1 | -IHWV1 ]
+  [ lapply (sfr_ldrop_trans_ge … HLK1 … HL1 ?) -HL1 /2 width=2/ #H
+    lapply (sfr_inv_skip … H ?) -H /2 width=1/ #HK1
+    elim (thin_ldrop_conf_le … HL12 … HLK1 ?) -HL12 /2 width=2/ #X #H #HLK2
+    elim (thin_inv_delift1 … H ?) -H /2 width=1/ #K2 #W2 #HK12 #HW12 #H destruct
+    elim (IHWV1 … HK1 HK12) -IHWV1 -HK1 -HK12 #X2 #V2 #HWV2 #H #_
+    lapply (delift_mono … H … HW12) -H #H destruct
+    elim (lift_total W2 0 (i+1)) #U2 #HWU2
+    lapply (ldrop_fwd_ldrop2 … HLK1) -HLK1 #HLK1
+    lapply (delift_lift_ge … HW12 … HLK1 HWU1 … HWU2) -HW12 -HLK1 -HWU1 //
+    >minus_plus <plus_minus_m_m // /3 width=6/
+  | elim (lt_or_ge i (d+e)) #Hide [ -HWV1 -HWU1 -HL12 | -Hdi -HL1 ]
+    [ lapply (sfr_inv_ldrop … HLK1 … HL1 ? ?) -HLK1 -HL1 // -Hdi -Hide #H destruct 
+    | lapply (transitive_le … (i+1) Hide ?) /2 width=1/ #Hdei
+      lapply (thin_ldrop_conf_ge … HL12 … HLK1 ?) -HL12 -HLK1 // #HL2K1
+      elim (lift_split … HWU1 d (i+1-e) ? ? ?) -HWU1 // /2 width=1/ #W
+      <plus_minus in ⊢ (??%??→?); /2 width=2/ #HW1
+      <minus_minus // /2 width=2/ -Hdei >commutative_plus <minus_n_n /3 width=6/
+    ]
+  ]
+| #I #L1 #V1 #W1 #T1 #U1 #l1 #l2 #_ #_ #IHVW1 #IHTU1 #L2 #d #e #HL1 #HL12
+  elim (IHVW1 … HL1 HL12) -IHVW1 #V2 #W2 #HVW2 #HV12 #_
+  elim (IHTU1 (L2.ⓑ{I}V2) (d+1) e ? ?) -IHTU1 /2 width=1/ -HL1 -HL12 #T2 #U2 #HTU2 #HT12 #HU12
+  lapply (delift_lsubs_trans … HT12 (L1.ⓑ{I}V2) ?) -HT12 /2 width=1/
+  lapply (delift_lsubs_trans … HU12 (L1.ⓑ{I}V2) ?) -HU12 /2 width=1/ /3 width=7/
+| #L1 #V1 #W11 #W12 #T1 #U1 #l1 #l2 #_ #_ #IHVW1 #IHTU1 #L2 #d #e #HL1 #HL12
+  elim (IHVW1 … HL1 HL12) -IHVW1 #V2 #W22 #HVW2 #HV12 #HW122
+  elim (IHTU1 … HL1 HL12) -IHTU1 -HL1 -HL12 #X2 #Y2 #HXY2 #HX2 #HY2
+  elim (delift_inv_bind1 … HX2) -HX2 #W21 #T2 #W121 #HT12 #H destruct
+  elim (delift_inv_bind1 … HY2) -HY2 #X #U2 #HX #HU12 #H destruct
+  lapply (delift_mono … HX … HW122) -HX #H destruct
+  @(ex3_2_intro … (ⓐV2.ⓛW21.T2) (ⓐV2.ⓛW22.U2)) [ /2 width=2/ | 2,3: /3 width=1/ ] (**) (* explict constructor, /4 depth=?/ is too slow *)
+| #L1 #V1 #T1 #U1 #W1 #l #_ #_ #IHTU1 #IHUW1 #L2 #d #e #HL1 #HL12
+  elim (IHTU1 … HL1 HL12) -IHTU1 #T2 #U2 #HTU2 #HT12 #HU12
+  elim (IHUW1 … HL1 HL12) -IHUW1 -HL1 -HL12 #X2 #W2 #HXW2 #H #HW12
+  elim (delift_inv_flat1 … H) -H #V2 #Y2 #HV12 #HY2 #H destruct
+  lapply (delift_mono … HY2 … HU12) -HY2 #H destruct /3 width=7/
+| #L1 #T1 #U1 #W1 #l1 #l2 #_ #_ #IHTU1 #IHUW1 #L2 #d #e #HL1 #HL12
+  elim (IHTU1 … HL1 HL12) -IHTU1 #T2 #U2 #HTU2 #HT12 #HU12
+  elim (IHUW1 … HL1 HL12) -IHUW1 -HL1 -HL12 #Y2 #W2 #HUW2 #HY2 #HW12
+  lapply (delift_mono … HY2 … HU12) -HY2 #H destruct /3 width=5/
+| #L1 #T1 #U11 #U12 #V1 #l #_ #HU112 #_ #IHT1 #IHU12 #L2 #d #e #HL1 #HL12
+  elim (IHT1 … HL1 HL12) -IHT1 #T2 #U21 #HT2 #HT12 #HU121
+  elim (IHU12 … HL1 HL12) -IHU12 -HL1 #U22 #V2 #HU22 #HU122 #_
+  lapply (thin_cpcs_delift_mono … HU112 … HL12 … HU121 … HU122) -HU112 -HL12 -HU121 /3 width=5/
+]
+qed.
+
+lemma snta_ldrop_conf: ∀h,L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 :[l] U1 →
+                       ∀L2,d,e. ≽ [d, e] L1 → ⇩[d, e] L1 ≡ L2 →
+                       ∃∃T2,U2. ⦃h, L2⦄ ⊢ T2 :[l] U2 &
+                                L1 ⊢ T1 ▼*[d, e] ≡ T2 & L1 ⊢ U1 ▼*[d, e] ≡ U2.
+/3 width=1/ qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/sta.ma b/matita/matita/contribs/lambda_delta/basic_2/etc/sta/sta.etc
similarity index 100%
rename from matita/matita/contribs/lambda_delta/basic_2/static/sta.ma
rename to matita/matita/contribs/lambda_delta/basic_2/etc/sta/sta.etc
diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/sta_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/etc/sta/sta_lift.etc
similarity index 100%
rename from matita/matita/contribs/lambda_delta/basic_2/static/sta_lift.ma
rename to matita/matita/contribs/lambda_delta/basic_2/etc/sta/sta_lift.etc
diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/sta_ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/etc/sta/sta_ltpss.etc
similarity index 100%
rename from matita/matita/contribs/lambda_delta/basic_2/static/sta_ltpss.ma
rename to matita/matita/contribs/lambda_delta/basic_2/etc/sta/sta_ltpss.etc
diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/sta_sta.ma b/matita/matita/contribs/lambda_delta/basic_2/etc/sta/sta_sta.etc
similarity index 100%
rename from matita/matita/contribs/lambda_delta/basic_2/static/sta_sta.ma
rename to matita/matita/contribs/lambda_delta/basic_2/etc/sta/sta_sta.etc
diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/term_simple.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/term_simple.ma
index 4c02d521d..83aff07c4 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/grammar/term_simple.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/term_simple.ma
@@ -39,3 +39,8 @@ lemma simple_inv_pair: ∀I,V,T.  𝐒⦃②{I}V.T⦄ → ∃J. I = Flat2 J.
 * /2 width=2/ #I #V #T #H
 elim (simple_inv_bind … H)
 qed-.
+
+(*
+lemma mt: ∀R1,R2:Prop. (R1 → R2) → (R2 → ⊥) → R1 → ⊥.
+/3 width=1/ qed-.
+*)
diff --git a/matita/matita/contribs/lambda_delta/basic_2/names.txt b/matita/matita/contribs/lambda_delta/basic_2/names.txt
index 31ae26c39..1a4b33044 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/names.txt
+++ b/matita/matita/contribs/lambda_delta/basic_2/names.txt
@@ -10,19 +10,28 @@ I,J    : item
 K,L    : local environment
 M,N    : reserved: future use
 O      : 
-P,Q    : reserved: future use
+P,Q    : reserved: future use (lambda_delta 4)
 R      : generic predicate (relation)
 S      : RTM stack
 T,U,V,W: term
 X,Y,Z  : reserved: transient objet denoted by a capital letter
 
+a,b    : reserved: future use (lambda_delta 4)
+c      : reserved: future use (lambda_delta 3)
 d      : relocation depth
 e      : relocation height
+f      :
+g      : sort degree parameter
 h      : sort hierarchy parameter
 i,j    : local reference position index (de Bruijn's)
 k      : sort index
+l      : term degree
+m,n    : reserved: future use
+o      :
 p,q    : global reference position
+r,s    :
 t,u    : local reference position level (de Bruijn's)
+v,w    :
 x,y,z  : reserved: transient objet denoted by a small letter
 
 NAMING CONVENTIONS FOR CONSTRUCTORS
diff --git a/matita/matita/contribs/lambda_delta/basic_2/notation.ma b/matita/matita/contribs/lambda_delta/basic_2/notation.ma
index 31126679f..6bbde1839 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/notation.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/notation.ma
@@ -222,15 +222,15 @@ notation "hvbox( T1 ÷ ⊑ break term 46 T2 )"
    non associative with precedence 45
    for @{ 'CrSubEqB $T1 $T2 }.
 
-notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 • break term 46 T2 )"
+notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 • break [ g , break l ] break term 46 T2 )"
    non associative with precedence 45
-   for @{ 'StaticType $h $L $T1 $T2 }.
+   for @{ 'StaticType $h $g $l $L $T1 $T2 }.
 
 (* Unwind *******************************************************************)
 
-notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 •* break term 46 T2 )"
+notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 •* break [ g ] break term 46 T2 )"
    non associative with precedence 45
-   for @{ 'StaticTypeStar $h $L $T1 $T2 }.
+   for @{ 'StaticTypeStar $h $g $L $T1 $T2 }.
 
 (* Reducibility *************************************************************)
 
@@ -294,6 +294,10 @@ notation "hvbox( L1 ⊢ ➡ break term 46 L2 )"
    non associative with precedence 45
    for @{ 'CPRed $L1 $L2 }.
 
+notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 ➸ break [ g ] break term 46 T2 )"
+   non associative with precedence 45
+   for @{ 'XRed $h $g $L $T1 $T2 }.
+
 (* Computation **************************************************************)
 
 notation "hvbox( T1 ➡* break term 46 T2 )"
@@ -316,11 +320,11 @@ notation "hvbox( ⬇ * term 46 T  )"
    non associative with precedence 45
    for @{ 'SN $T }.
 
-notation "hvbox( L ⊢ break ⬇ * term 46 T )"
+notation "hvbox( L ⊢ ⬇ * break term 46 T )"
    non associative with precedence 45
    for @{ 'SN $L $T }.
 
-notation "hvbox( L ⊢ break ⬇ ⬇ * term 46 T )"
+notation "hvbox( L ⊢ ⬇ ⬇ * break term 46 T )"
    non associative with precedence 45
    for @{ 'SNAlt $L $T }.
 
@@ -332,6 +336,14 @@ notation "hvbox( T1 ⊑ break [ R ] break term 46 T2 )"
    non associative with precedence 45
    for @{ 'CrSubEq $T1 $R $T2 }.
 
+notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 ➸ * break [ g ] break term 46 T2 )"
+   non associative with precedence 45
+   for @{ 'XRedStar $h $g $L $T1 $T2 }.
+
+notation "hvbox( ⦃ h , break L ⦄ ⊢ ➷ * break [ g ] break term 46 T2 )"
+   non associative with precedence 45
+   for @{ 'XSN $h $g $L $T }.
+
 (* Conversion ***************************************************************)
 
 notation "hvbox( L ⊢ break term 46 T1 ⬌ break term 46 T2 )"
@@ -354,20 +366,20 @@ notation "hvbox( T1 ⊢ ⬌* break term 46 T2 )"
 
 (* Dynamic typing ***********************************************************)
 
+notation "hvbox( ⦃ h , break L ⦄ ⊩ break term 46 T : break [ g ] )"
+   non associative with precedence 45
+   for @{ 'NativeValid $h $g $L $T }.
+
 notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 : break term 46 T2 )"
    non associative with precedence 45
    for @{ 'NativeType $h $L $T1 $T2 }.
 
-notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 :: break term 46 T2 )"
+notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 : : break term 46 T2 )"
    non associative with precedence 45
    for @{ 'NativeTypeAlt $h $L $T1 $T2 }.
 
-notation "hvbox( h ⊢ break term 46 L1 : ⊑ break term 46 L2 )"
-   non associative with precedence 45
-   for @{ 'CrSubEqN $h $L1 $L2 }.
-
 (* Higher order dynamic typing **********************************************)
 
-notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 :* break term 46 T2 )"
+notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 : * break term 46 T2 )"
    non associative with precedence 45
    for @{ 'NativeTypeStar $h $L $T1 $T2 }.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma
index 068a5f751..b3dbcf40c 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma
@@ -78,7 +78,7 @@ elim (tpr_inv_abbr1 … H1) -H1 *
   lapply (tps_weak_all … HT0) -HT0 #HT0
   lapply (tpss_lsubs_trans … HT02 (L. ⓓV) ?) -HT02 /2 width=1/ #HT02
   lapply (tpss_weak_all … HT02) -HT02 #HT02
-  lapply (tpss_strap … HT0 HT02) -T0 /4 width=7/
+  lapply (tpss_strap2 … HT0 HT02) -T0 /4 width=7/
 | #T2 #HT12 #HXT2
   elim (lift_total Y 0 1) #Z #HYZ
   lapply (tpss_lift_ge … H2 (L.ⓓV1) … HXT2 … HYZ) -X // /2 width=1/ #H
diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/sd.ma b/matita/matita/contribs/lambda_delta/basic_2/static/sd.ma
new file mode 100644
index 000000000..04adbae95
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/static/sd.ma
@@ -0,0 +1,105 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/sh.ma".
+
+(* SORT DEGREE **************************************************************)
+
+(* sort degree specification *)
+record sd (h:sh): Type[0] ≝ {
+   deg      : relation nat;                                 (* degree of the sort *)
+   deg_total: ∀k. ∃l. deg k l;                              (* functional relation axioms *)
+   deg_mono : ∀k,l1,l2. deg k l1 → deg k l2 → l1 = l2;
+   deg_next : ∀k,l. deg k l → deg (next h k) (l - 1);       (* compatibility condition *)
+   deg_prev : ∀k,l. deg (next h k) (l + 1) → deg k (l + 2)
+}.
+
+(* Notable specifications ***************************************************)
+
+definition deg_O: relation nat ≝ λk,l. l = 0.
+
+definition sd_O: ∀h. sd h ≝ λh. mk_sd h deg_O ….
+// /2 width=1/ /2 width=2/ qed.
+
+inductive deg_SO (h:sh) (k:nat) (k0:nat): predicate nat ≝
+| deg_SO_pos : ∀l0. (next h)^l0 k0 = k → deg_SO h k k0 (l0 + 1)
+| deg_SO_zero: ((∃l0. (next h)^l0 k0 = k) → ⊥) → deg_SO h k k0 0
+.
+
+fact deg_SO_inv_pos_aux: ∀h,k,k0,l0. deg_SO h k k0 l0 → ∀l. l0 = l + 1 →
+                         (next h)^l k0 = k.
+#h #k #k0 #l0 * -l0
+[ #l0 #Hl0 #l #H
+  lapply (injective_plus_l … H) -H #H destruct //
+| #_ #l0 <plus_n_Sm #H destruct
+]
+qed.
+
+lemma deg_SO_inv_pos: ∀h,k,k0,l0. deg_SO h k k0 (l0 + 1) → (next h)^l0 k0 = k.
+/2 width=3/ qed-.
+
+lemma deg_SO_refl: ∀h,k. deg_SO h k k 1.
+#h #k @(deg_SO_pos … 0 ?) //
+qed.
+
+lemma deg_SO_gt: ∀h,k1,k2. k1 < k2 → deg_SO h k1 k2 0.
+#h #k1 #k2 #HK12 @deg_SO_zero * #l elim l -l normalize
+[ #H destruct
+  elim (lt_refl_false … HK12)
+| #l #_ #H
+  lapply (next_lt h ((next h)^l k2)) >H -H #H
+  lapply (transitive_lt … H HK12) -k1 #H1
+  lapply (nexts_le h k2 l) #H2
+  lapply (le_to_lt_to_lt … H2 H1) -h -l #H
+  elim (lt_refl_false … H)
+qed.
+
+definition sd_SO: ∀h. nat → sd h ≝ λh,k. mk_sd h (deg_SO h k) ….
+[ #k0
+  lapply (nexts_dec h k0 k) * [ * /3 width=2/ | /4 width=2/ ]
+| #K0 #l1 #l2 * [ #l01 ] #H1 * [1,3: #l02 ] #H2 //
+  [ < H2 in H1; -H2 #H
+    lapply (nexts_inj … H) -H #H destruct //
+  | elim (H1 ?) /2 width=2/
+  | elim (H2 ?) /2 width=2/
+  ]
+| #k0 #l0 *
+  [ #l #H destruct elim l -l normalize /2 width=1/
+  | #H1 @deg_SO_zero * #l #H2 destruct
+    @H1 -H1 @(ex_intro … (S l)) /2 width=1/ (**) (* explicit constructor *)
+  ]
+| #K0 #l0 #H
+  <(deg_SO_inv_pos … H) -H >plus_n_2
+  @deg_SO_pos >iter_SO /2 width=1/ (**) (* explicit constructor: iter_SO is needed *)
+]
+qed.
+
+let rec sd_l (h:sh) (k:nat) (l:nat) on l : sd h ≝
+   match l with 
+   [ O   ⇒ sd_O h
+   | S l ⇒ match l with
+           [ O ⇒ sd_SO h k
+           | _ ⇒ sd_l h (next h k) l
+           ]
+   ].
+
+(* Basic properties *********************************************************)
+
+lemma sd_l_SS: ∀h,k,l. sd_l h k (l + 2) = sd_l h (next h k) (l + 1).
+#h #k #l <plus_n_Sm <plus_n_Sm //
+qed.
+
+lemma sd_l_correct: ∀h,l,k. deg h (sd_l h k l) k l.
+#h #l @(nat_ind_plus … l) -l // #l @(nat_ind_plus … l) -l // /3 width=1/
+qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/sh.ma b/matita/matita/contribs/lambda_delta/basic_2/static/sh.ma
index 0577b0015..72df7717e 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/static/sh.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/static/sh.ma
@@ -18,6 +18,19 @@ include "ground_2/arith.ma".
 
 (* sort hierarchy specification *)
 record sh: Type[0] ≝ {
-   next: nat → nat;        (* next sort in the hierarchy *)
+   next   : nat → nat;     (* next sort in the hierarchy *)
    next_lt: ∀k. k < next k (* strict monotonicity condition *)
 }.
+
+(* Basic properties *********************************************************)
+
+lemma nexts_le: ∀h,k,l. k ≤ (next h)^l k.
+#h #k #l elim l -l // normalize #l #IHl
+lapply (next_lt h ((next h)^l k)) #H
+lapply (le_to_lt_to_lt … IHl H) -IHl -H /2 width=2/
+qed.
+
+axiom nexts_dec: ∀h,k1,k2. Decidable (∃l. (next h)^l k1 = k2).
+
+axiom nexts_inj: ∀h,k,l1,l2. (next h)^l1 k = (next h)^l2 k → l1 = l2.
+
diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/ssta.ma b/matita/matita/contribs/lambda_delta/basic_2/static/ssta.ma
new file mode 100644
index 000000000..e01b48d57
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/static/ssta.ma
@@ -0,0 +1,134 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/substitution/ldrop.ma".
+include "basic_2/static/sd.ma".
+
+(* STRATIFIED STATIC TYPE ASSIGNMENT ON TERMS *******************************)
+
+inductive ssta (h:sh) (g:sd h): nat → lenv → relation term ≝
+| ssta_sort: ∀L,k,l. deg h g k l → ssta h g l L (⋆k) (⋆(next h k))
+| ssta_ldef: ∀L,K,V,W,U,i,l. ⇩[0, i] L ≡ K. ⓓV → ssta h g l K V W →
+             ⇧[0, i + 1] W ≡ U → ssta h g l L (#i) U
+| ssta_ldec: ∀L,K,W,V,U,i,l. ⇩[0, i] L ≡ K. ⓛW → ssta h g l K W V →
+             ⇧[0, i + 1] W ≡ U → ssta h g (l+1) L (#i) U
+| ssta_bind: ∀I,L,V,T,U,l. ssta h g l (L. ⓑ{I} V) T U →
+             ssta h g l L (ⓑ{I}V.T) (ⓑ{I}V.U)
+| ssta_appl: ∀L,V,T,U,l. ssta h g l L T U →
+             ssta h g l L (ⓐV.T) (ⓐV.U)
+| ssta_cast: ∀L,V,W,T,U,l. ssta h g (l - 1) L V W → ssta h g l L T U →
+                           ssta h g l L (ⓝV. T) (ⓝW. U)
+.
+
+interpretation "stratified static type assignment (term)"
+   'StaticType h g l L T U = (ssta h g l L T U).
+
+(* Basic inversion lemmas ************************************************)
+
+fact ssta_inv_sort1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → ∀k0. T = ⋆k0 →
+                         deg h g k0 l ∧ U = ⋆(next h k0).
+#h #g #L #T #U #l * -L -T -U -l
+[ #L #k #l #Hkl #k0 #H destruct /2 width=1/
+| #L #K #V #W #U #i #l #_ #_ #_ #k0 #H destruct
+| #L #K #W #V #U #i #l #_ #_ #_ #k0 #H destruct
+| #I #L #V #T #U #l #_ #k0 #H destruct
+| #L #V #T #U #l #_ #k0 #H destruct
+| #L #V #W #T #U #l #_ #_ #k0 #H destruct
+qed.
+
+(* Basic_1: was just: sty0_gen_sort *)
+lemma ssta_inv_sort1: ∀h,g,L,U,k,l. ⦃h, L⦄ ⊢ ⋆k •[g, l] U →
+                      deg h g k l ∧ U = ⋆(next h k).
+/2 width=4/ qed-.
+
+fact ssta_inv_lref1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → ∀j. T = #j →
+                         (∃∃K,V,W. ⇩[0, j] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V •[g, l] W &
+                                   ⇧[0, j + 1] W ≡ U
+                         ) ∨
+                         (∃∃K,W,V,l0. ⇩[0, j] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W •[g, l0] V &
+                                      ⇧[0, j + 1] W ≡ U & l = l0 + 1
+                         ).
+#h #g #L #T #U #l * -L -T -U -l
+[ #L #k #l #_ #j #H destruct
+| #L #K #V #W #U #i #l #HLK #HVW #HWU #j #H destruct /3 width=6/
+| #L #K #W #V #U #i #l #HLK #HWV #HWU #j #H destruct /3 width=8/
+| #I #L #V #T #U #l #_ #j #H destruct
+| #L #V #T #U #l #_ #j #H destruct
+| #L #V #W #T #U #l #_ #_ #j #H destruct
+]
+qed.
+
+(* Basic_1: was just: sty0_gen_lref *)
+lemma ssta_inv_lref1: ∀h,g,L,U,i,l. ⦃h, L⦄ ⊢ #i •[g, l] U →
+                      (∃∃K,V,W. ⇩[0, i] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V •[g, l] W &
+                                ⇧[0, i + 1] W ≡ U
+                      ) ∨
+                      (∃∃K,W,V,l0. ⇩[0, i] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W •[g, l0] V &
+                                   ⇧[0, i + 1] W ≡ U & l = l0 + 1
+                      ).
+/2 width=3/ qed-.
+
+fact ssta_inv_bind1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U →
+                         ∀J,X,Y. T = ⓑ{J}Y.X →
+                         ∃∃Z. ⦃h, L.ⓑ{J}Y⦄ ⊢ X •[g, l] Z & U = ⓑ{J}Y.Z.
+#h #g #L #T #U #l * -L -T -U -l
+[ #L #k #l #_ #J #X #Y #H destruct
+| #L #K #V #W #U #i #l #_ #_ #_ #J #X #Y #H destruct
+| #L #K #W #V #U #i #l #_ #_ #_ #J #X #Y #H destruct
+| #I #L #V #T #U #l #HTU #J #X #Y #H destruct /2 width=3/
+| #L #V #T #U #l #_ #J #X #Y #H destruct
+| #L #V #W #T #U #l #_ #_ #J #X #Y #H destruct
+]
+qed.
+
+(* Basic_1: was just: sty0_gen_bind *)
+lemma ssta_inv_bind1: ∀h,g,J,L,Y,X,U,l. ⦃h, L⦄ ⊢ ⓑ{J}Y.X •[g, l] U →
+                      ∃∃Z. ⦃h, L.ⓑ{J}Y⦄ ⊢ X •[g, l] Z & U = ⓑ{J}Y.Z.
+/2 width=3/ qed-.
+
+fact ssta_inv_appl1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → ∀X,Y. T = ⓐY.X →
+                         ∃∃Z. ⦃h, L⦄ ⊢ X •[g, l] Z & U = ⓐY.Z.
+#h #g #L #T #U #l * -L -T -U -l
+[ #L #k #l #_ #X #Y #H destruct
+| #L #K #V #W #U #i #l #_ #_ #_ #X #Y #H destruct
+| #L #K #W #V #U #i #l #_ #_ #_ #X #Y #H destruct
+| #I #L #V #T #U #l #_ #X #Y #H destruct
+| #L #V #T #U #l #HTU #X #Y #H destruct /2 width=3/
+| #L #V #W #T #U #l #_ #_ #X #Y #H destruct
+]
+qed.
+
+(* Basic_1: was just: sty0_gen_appl *)
+lemma ssta_inv_appl1: ∀h,g,L,Y,X,U,l. ⦃h, L⦄ ⊢ ⓐY.X •[g, l] U →
+                      ∃∃Z. ⦃h, L⦄ ⊢ X •[g, l] Z & U = ⓐY.Z.
+/2 width=3/ qed-.
+
+fact ssta_inv_cast1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → ∀X,Y. T = ⓝY.X →
+                         ∃∃Z1,Z2. ⦃h, L⦄ ⊢ Y •[g, l-1] Z1 & ⦃h, L⦄ ⊢ X •[g, l] Z2 &
+                                  U = ⓝZ1.Z2.
+#h #g #L #T #U #l * -L -T -U -l
+[ #L #k #l #_ #X #Y #H destruct
+| #L #K #V #W #U #l #i #_ #_ #_ #X #Y #H destruct
+| #L #K #W #V #U #l #i #_ #_ #_ #X #Y #H destruct
+| #I #L #V #T #U #l #_ #X #Y #H destruct
+| #L #V #T #U #l #_ #X #Y #H destruct
+| #L #V #W #T #U #l #HVW #HTU #X #Y #H destruct /2 width=5/
+]
+qed.
+
+(* Basic_1: was just: sty0_gen_cast *)
+lemma ssta_inv_cast1: ∀h,g,L,X,Y,U,l. ⦃h, L⦄ ⊢ ⓝY.X •[g, l] U →
+                      ∃∃Z1,Z2. ⦃h, L⦄ ⊢ Y •[g, l-1] Z1 & ⦃h, L⦄ ⊢ X •[g, l] Z2 &
+                               U = ⓝZ1.Z2.
+/2 width=4/ qed-.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/ssta_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/static/ssta_lift.ma
new file mode 100644
index 000000000..77a3c4fef
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/static/ssta_lift.ma
@@ -0,0 +1,124 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/substitution/ldrop_ldrop.ma".
+include "basic_2/static/ssta.ma".
+
+(* STRATIFIED STATIC TYPE ASSIGNMENT ON TERMS *******************************)
+
+(* Properties on relocation *************************************************)
+
+(* Basic_1: was just: sty0_lift *)
+lemma ssta_lift: ∀h,g,L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 →
+                 ∀L2,d,e. ⇩[d, e] L2 ≡ L1 → ∀T2. ⇧[d, e] T1 ≡ T2 →
+                 ∀U2. ⇧[d, e] U1 ≡ U2 → ⦃h, L2⦄ ⊢ T2 •[g, l] U2.
+#h #g #L1 #T1 #U1 #l #H elim H -L1 -T1 -U1 -l
+[ #L1 #k #l #Hkl #L2 #d #e #HL21 #X1 #H1 #X2 #H2
+  >(lift_inv_sort1 … H1) -X1
+  >(lift_inv_sort1 … H2) -X2 /2 width=1/
+| #L1 #K1 #V1 #W1 #W #i #l #HLK1 #_ #HW1 #IHVW1 #L2 #d #e #HL21 #X #H #U2 #HWU2
+  elim (lift_inv_lref1 … H) * #Hid #H destruct
+  [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // #W2 #HW12 #HWU2
+    elim (ldrop_trans_le … HL21 … HLK1 ?) -L1 /2 width=2/ #X #HLK2 #H
+    elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K2 #V2 #HK21 #HV12 #H destruct
+    /3 width=8/
+  | lapply (lift_trans_be … HW1 … HWU2 ? ?) -W // /2 width=1/ #HW1U2
+    lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/
+  ]
+| #L1 #K1 #W1 #V1 #W #i #l #HLK1 #_ #HW1 #IHWV1 #L2 #d #e #HL21 #X #H #U2 #HWU2
+  elim (lift_inv_lref1 … H) * #Hid #H destruct
+  [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // <minus_plus #W #HW1 #HWU2
+    elim (ldrop_trans_le … HL21 … HLK1 ?) -L1 /2 width=2/ #X #HLK2 #H
+    elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K2 #W2 #HK21 #HW12 #H destruct
+    lapply (lift_mono … HW1 … HW12) -HW1 #H destruct
+    elim (lift_total V1 (d-i-1) e) /3 width=8/
+  | lapply (lift_trans_be … HW1 … HWU2 ? ?) -W // /2 width=1/ #HW1U2
+    lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/
+  ]
+| #I #L1 #V1 #T1 #U1 #l #_ #IHTU1 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
+  elim (lift_inv_bind1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H destruct
+  elim (lift_inv_bind1 … H2) -H2 #X #U2 #H1 #HU12 #H2 destruct
+  lapply (lift_mono … H1 … HV12) -H1 #H destruct /4 width=5/
+| #L1 #V1 #T1 #U1 #l #_ #IHTU1 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
+  elim (lift_inv_flat1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H destruct
+  elim (lift_inv_flat1 … H2) -H2 #X #U2 #H1 #HU12 #H2 destruct
+  lapply (lift_mono … H1 … HV12) -H1 #H destruct /4 width=5/
+| #L1 #V1 #W1 #T1 #U1 #l #_ #_ #IHVW1 #IHTU1 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
+  elim (lift_inv_flat1 … H1) -H1 #V2 #W2 #HV12 #HW12 #H destruct
+  elim (lift_inv_flat1 … H2) -H2 #T2 #U2 #HT12 #HU12 #H destruct /3 width=5/
+]
+qed.
+
+(* Note: apparently this was missing in basic_1 *)
+lemma ssta_inv_lift1: ∀h,g,L2,T2,U2,l. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 →
+                      ∀L1,d,e. ⇩[d, e] L2 ≡ L1 → ∀T1. ⇧[d, e] T1 ≡ T2 →
+                      ∃∃U1. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 & ⇧[d, e] U1 ≡ U2.
+#h #g #L2 #T2 #U2 #l #H elim H -L2 -T2 -U2 -l
+[ #L2 #k #l #Hkl #L1 #d #e #_ #X #H
+  >(lift_inv_sort2 … H) -X /3 width=3/
+| #L2 #K2 #V2 #W2 #W #i #l #HLK2 #HVW2 #HW2 #IHVW2 #L1 #d #e #HL21 #X #H
+  elim (lift_inv_lref2 … H) * #Hid #H destruct [ -HVW2 | -IHVW2 ]
+  [ elim (ldrop_conf_lt … HL21 … HLK2 ?) -L2 // #K1 #V1 #HLK1 #HK21 #HV12
+    elim (IHVW2 … HK21 … HV12) -K2 -V2 #W1 #HVW1 #HW12
+    elim (lift_trans_le … HW12 … HW2 ?) -W2 // >minus_plus <plus_minus_m_m // -Hid /3 width=6/
+  | lapply (ldrop_conf_ge … HL21 … HLK2 ?) -L2 // #HL1K2
+    elim (le_inv_plus_l … Hid) -Hid #Hdie #ei
+    elim (lift_split … HW2 d (i-e+1) ? ? ?) -HW2 // [3: /2 width=1/ ]
+    [ #W0 #HW20 <le_plus_minus_comm // >minus_minus_m_m /2 width=1/ /3 width=6/
+    | <le_plus_minus_comm // /2 width=1/
+    ]
+  ]
+| #L2 #K2 #W2 #V2 #W #i #l #HLK2 #HWV2 #HW2 #IHWV2 #L1 #d #e #HL21 #X #H
+  elim (lift_inv_lref2 … H) * #Hid #H destruct [ -HWV2 | -IHWV2 ]
+  [ elim (ldrop_conf_lt … HL21 … HLK2 ?) -L2 // #K1 #W1 #HLK1 #HK21 #HW12
+    elim (IHWV2 … HK21 … HW12) -K2 #V1 #HWV1 #_
+    elim (lift_trans_le … HW12 … HW2 ?) -W2 // >minus_plus <plus_minus_m_m // -Hid /3 width=6/
+  | lapply (ldrop_conf_ge … HL21 … HLK2 ?) -L2 // #HL1K2
+    elim (le_inv_plus_l … Hid) -Hid #Hdie #ei
+    elim (lift_split … HW2 d (i-e+1) ? ? ?) -HW2 // [3: /2 width=1/ ]
+    [ #W0 #HW20 <le_plus_minus_comm // >minus_minus_m_m /2 width=1/ /3 width=6/
+    | <le_plus_minus_comm // /2 width=1/
+    ]
+  ]
+| #I #L2 #V2 #T2 #U2 #l #_ #IHTU2 #L1 #d #e #HL21 #X #H
+  elim (lift_inv_bind2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct
+  elim (IHTU2 (L1.ⓑ{I}V1) … HT12) -IHTU2 -HT12 /2 width=1/ -HL21 /3 width=5/
+| #L2 #V2 #T2 #U2 #l #_ #IHTU2 #L1 #d #e #HL21 #X #H
+  elim (lift_inv_flat2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct
+  elim (IHTU2 … HL21 … HT12) -L2 -HT12 /3 width=5/
+| #L2 #V2 #W2 #T2 #U2 #l #_ #_ #IHVW2 #IHTU2 #L1 #d #e #HL21 #X #H
+  elim (lift_inv_flat2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct
+  elim (IHVW2 … HL21 … HV12) -IHVW2
+  elim (IHTU2 … HL21 … HT12) -L2 -HT12 /3 width=5/
+]
+qed.
+
+(* Advanced forvard lemmas **************************************************)
+
+(* Basic_1: was just: sty0_correct *)
+lemma ssta_fwd_correct: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U →
+                        ∃T0. ⦃h, L⦄ ⊢ U •[g, l - 1] T0.
+#h #g #L #T #U #l #H elim H -L -T -U -l
+[ /4 width=2/
+| #L #K #V #W #W0 #i #l #HLK #_ #HW0 * #V0 #HWV0
+  lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
+  elim (lift_total V0 0 (i+1)) /3 width=10/
+| #L #K #W #V #V0 #i #l #HLK #HWV #HWV0 #_
+  lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
+  elim (lift_total V 0 (i+1)) /3 width=10/
+| #I #L #V #T #U #l #_ * /3 width=2/
+| #L #V #T #U #l #_ * #T0 #HUT0 /3 width=2/
+| #L #V #W #T #U #l #_ #_ * #W0 #HW0  * /3 width=2/
+]
+qed-.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/ssta_ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/static/ssta_ltpss.ma
new file mode 100644
index 000000000..d77d958e1
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/static/ssta_ltpss.ma
@@ -0,0 +1,125 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/tpss_tpss.ma".
+include "basic_2/unfold/ltpss_tpss.ma".
+include "basic_2/static/ssta_lift.ma".
+
+(* STRATIFIED STATIC TYPE ASSIGNMENT ON TERMS *******************************)
+
+(* Properties about parallel unfold *****************************************)
+
+(* Note: apparently this was missing in basic_1 *)
+lemma ssta_ltpss_tpss_conf: ∀h,g,L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 →
+                            ∀L2,d,e. L1 ▶* [d, e] L2 →
+                            ∀T2. L2 ⊢ T1 ▶* [d, e] T2 →
+                            ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 &
+                                  L2 ⊢ U1 ▶* [d, e] U2.
+#h #g #L1 #T1 #U #l #H elim H -L1 -T1 -U -l
+[ #L1 #k1 #l1 #Hkl1 #L2 #d #e #_ #T2 #H
+  >(tpss_inv_sort1 … H) -H /3 width=3/
+| #L1 #K1 #V1 #W1 #U1 #i #l #HLK1 #HVW1 #HWU1 #IHVW1 #L2 #d #e #HL12 #T2 #H
+  elim (tpss_inv_lref1 … H) -H [ | -HVW1 ]
+  [ #H destruct
+    elim (lt_or_ge i d) #Hdi [ -HVW1 | ]
+    [ elim (ltpss_ldrop_conf_le … HL12 … HLK1 ?) -L1 /2 width=2/ #X #H #HLK2
+      elim (ltpss_inv_tpss11 … H ?) -H /2 width=1/ #K2 #V2 #HK12 #HV12 #H destruct
+      elim (IHVW1 … HK12 … HV12) -IHVW1 -HK12 -HV12 #W2 #HVW2 #HW12
+      lapply (ldrop_fwd_ldrop2 … HLK2) #H
+      elim (lift_total W2 0 (i+1)) #U2 #HWU2
+      lapply (tpss_lift_ge … HW12 … H … HWU1 … HWU2) // -HW12 -H -HWU1
+      >minus_plus <plus_minus_m_m // -Hdi /3 width=6/
+    | elim (lt_or_ge i (d + e)) #Hide [ -HVW1 | -Hdi -IHVW1 ]
+      [ elim (ltpss_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HLK2
+        elim (ltpss_inv_tpss21 … H ?) -H /2 width=1/ #K2 #V2 #HK12 #HV12 #H destruct
+        elim (IHVW1 … HK12 … HV12) -IHVW1 -HK12 -HV12 #W2 #HVW2 #HW12
+        lapply (ldrop_fwd_ldrop2 … HLK2) #H
+        elim (lift_total W2 0 (i+1)) #U2 #HWU2
+        lapply (tpss_lift_ge … HW12 … H … HWU1 … HWU2) // -HW12 -H -HWU1 >minus_plus #H
+        lapply (tpss_weak … H d e ? ?) [1,2: normalize [ >commutative_plus <plus_minus_m_m // | /2 width=1/ ]] -Hdi -Hide /3 width=6/
+      | lapply (ltpss_ldrop_conf_ge … HL12 … HLK1 ?) -L1 // -Hide /3 width=6/
+      ]
+    ]
+  | * #K2 #V2 #W2 #Hdi #Hide #HLK2 #HVW2 #HWT2
+    elim (ltpss_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HL2K0
+    elim (ltpss_inv_tpss21 … H ?) -H /2 width=1/ #K0 #V0 #HK12 #HV12 #H destruct
+    lapply (ldrop_mono … HL2K0 … HLK2) -HL2K0 #H destruct
+    lapply (ldrop_fwd_ldrop2 … HLK2) -HLK2 #HLK2
+    lapply (tpss_trans_eq … HV12 HVW2) -V2 #HV1W2
+    elim (IHVW1 … HK12 … HV1W2) -IHVW1 -HK12 -HV1W2 #V2 #HWV2 #HW1V2
+    elim (lift_total V2 0 (i+1)) #U2 #HVU2
+    lapply (ssta_lift … HWV2 … HLK2 … HWT2 … HVU2) -HWV2 -HWT2 #HTU2
+    lapply (tpss_lift_ge … HW1V2 … HLK2 … HWU1 … HVU2) // -HW1V2 -HLK2 -HWU1 -HVU2 >minus_plus #H
+    lapply (tpss_weak … H d e ? ?) [1,2: normalize [ >commutative_plus <plus_minus_m_m // | /2 width=1/ ]] -Hdi -Hide /2 width=3/
+  ]
+| #L1 #K1 #W1 #V1 #U1 #i #l #HLK1 #HWV1 #HWU1 #IHWV1 #L2 #d #e #HL12 #T2 #H
+  elim (tpss_inv_lref1 … H) -H [ | -HWV1 -HWU1 -IHWV1 ]
+  [ #H destruct
+    elim (lt_or_ge i d) #Hdi [ -HWV1 ]
+    [ elim (ltpss_ldrop_conf_le … HL12 … HLK1 ?) -L1 /2 width=2/ #X #H #HLK2
+      elim (ltpss_inv_tpss11 … H ?) -H /2 width=1/ #K2 #W2 #HK12 #HW12 #H destruct
+      elim (IHWV1 … HK12 … HW12) -IHWV1 -HK12 #V2 #HWV2 #_
+      lapply (ldrop_fwd_ldrop2 … HLK2) #HLK
+      elim (lift_total W2 0 (i+1)) #U2 #HWU2
+      lapply (tpss_lift_ge … HW12 … HLK … HWU1 … HWU2) // -HW12 -HLK -HWU1
+      >minus_plus <plus_minus_m_m // -Hdi /3 width=6/
+    | elim (lt_or_ge i (d + e)) #Hide [ -HWV1 | -IHWV1 -Hdi ]
+      [ elim (ltpss_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HLK2
+        elim (ltpss_inv_tpss21 … H ?) -H /2 width=1/ #K2 #W2 #HK12 #HW12 #H destruct
+        elim (IHWV1 … HK12 … HW12) -IHWV1 -HK12 #V2 #HWV2 #_
+        lapply (ldrop_fwd_ldrop2 … HLK2) #HLK
+        elim (lift_total W2 0 (i+1)) #U2 #HWU2
+        lapply (tpss_lift_ge … HW12 … HLK … HWU1 … HWU2) // -HW12 -HLK -HWU1 >minus_plus #H
+        lapply (tpss_weak … H d e ? ?) [1,2: normalize [ >commutative_plus <plus_minus_m_m // | /2 width=1/ ]] -Hdi -Hide /3 width=6/
+      | lapply (ltpss_ldrop_conf_ge … HL12 … HLK1 ?) -L1 // -Hide /3 width=6/
+      ]
+    ]
+  | * #K2 #V2 #W2 #Hdi #Hide #HLK2 #_ #_
+    elim (ltpss_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HL2K0
+    elim (ltpss_inv_tpss21 … H ?) -H /2 width=1/ -Hdi -Hide #K0 #V0 #_ #_ #H destruct
+    lapply (ldrop_mono … HL2K0 … HLK2) -HL2K0 -HLK2 #H destruct
+  ]
+| #I #L1 #V1 #T1 #U1 #l #_ #IHTU1 #L2 #d #e #HL12 #X #H
+  elim (tpss_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
+  elim (IHTU1 … HT12) -IHTU1 -HT12 /2 width=1/ -HL12 /3 width=5/
+| #L1 #V1 #T1 #U1 #l #_ #IHTU1 #L2 #d #e #HL12 #X #H
+  elim (tpss_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
+  elim (IHTU1 … HT12) -IHTU1 -HT12 // -HL12 /3 width=5/
+| #L1 #V1 #W1 #T1 #U1 #l #_ #_ #IHVW1 #IHTU1 #L2 #d #e #HL12 #X #H
+  elim (tpss_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
+  elim (IHVW1 … HV12) -IHVW1 -HV12 //
+  elim (IHTU1 … HT12) -IHTU1 -HT12 // -HL12 /3 width=5/
+]
+qed.
+
+lemma ssta_ltpss_tps_conf: ∀h,g,L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 →
+                           ∀L2,d,e. L1 ▶* [d, e] L2 →
+                           ∀T2. L2 ⊢ T1 ▶ [d, e] T2 →
+                           ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & L2 ⊢ U1 ▶* [d, e] U2.
+/3 width=5/ qed.
+
+lemma ssta_ltpss_conf: ∀h,g,L1,T,U1,l. ⦃h, L1⦄ ⊢ T •[g, l] U1 →
+                       ∀L2,d,e. L1 ▶* [d, e] L2 →
+                       ∃∃U2. ⦃h, L2⦄ ⊢ T •[g, l] U2 & L2 ⊢ U1 ▶* [d, e] U2.
+/2 width=5/ qed.
+
+lemma ssta_tpss_conf: ∀h,g,L,T1,U1,l. ⦃h, L⦄ ⊢ T1 •[g, l] U1 →
+                      ∀T2,d,e. L ⊢ T1 ▶* [d, e] T2 →
+                      ∃∃U2. ⦃h, L⦄ ⊢ T2 •[g, l] U2 & L ⊢ U1 ▶* [d, e] U2.
+/2 width=5/ qed.
+
+lemma ssta_tps_conf: ∀h,g,L,T1,U1,l. ⦃h, L⦄ ⊢ T1 •[g, l] U1 →
+                     ∀T2,d,e. L ⊢ T1 ▶ [d, e] T2 →
+                     ∃∃U2. ⦃h, L⦄ ⊢ T2 •[g, l] U2 & L ⊢ U1 ▶* [d, e] U2.
+/2 width=5/ qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/ssta_ssta.ma b/matita/matita/contribs/lambda_delta/basic_2/static/ssta_ssta.ma
new file mode 100644
index 000000000..5e699fd55
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/static/ssta_ssta.ma
@@ -0,0 +1,50 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/substitution/ldrop_ldrop.ma".
+include "basic_2/static/ssta.ma".
+
+(* STRATIFIED STATIC TYPE ASSIGNMENT ON TERMS *******************************)
+
+(* Main properties **********************************************************)
+
+(* Note: apparently this was missing in basic_1 *)
+theorem ssta_mono: ∀h,g,L,T,U1,l1. ⦃h, L⦄ ⊢ T •[g, l1] U1 →
+                   ∀U2,l2. ⦃h, L⦄ ⊢ T •[g, l2] U2 → l1 = l2 ∧ U1 = U2.
+#h #g #L #T #U1 #l1 #H elim H -L -T -U1 -l1
+[ #L #k #l #Hkl #X #l2 #H
+  elim (ssta_inv_sort1 … H) -H #Hkl2 #H destruct
+  >(deg_mono … Hkl2 … Hkl) -g -L -l2 /2 width=1/
+| #L #K #V #W #U1 #i #l1 #HLK #_ #HWU1 #IHVW #U2 #l2 #H
+  elim (ssta_inv_lref1 … H) -H * #K0 #V0 #W0 [2: #l0] #HLK0 #HVW0 #HW0U2
+  lapply (ldrop_mono … HLK0 … HLK) -HLK -HLK0 #H destruct
+  lapply (IHVW … HVW0) -IHVW -HVW0 * #H1 #H2 destruct
+  >(lift_mono … HWU1 … HW0U2) -W0 -U1 /2 width=1/
+| #L #K #W #V #U1 #i #l1 #HLK #_ #HWU1 #IHWV #U2 #l2 #H
+  elim (ssta_inv_lref1 … H) -H * #K0 #W0 #V0 [2: #l0 ] #HLK0 #HWV0 #HV0U2
+  lapply (ldrop_mono … HLK0 … HLK) -HLK -HLK0 #H destruct
+  lapply (IHWV … HWV0) -IHWV -HWV0 * #H1 #H2 destruct
+  >(lift_mono … HWU1 … HV0U2) -W -U1 /2 width=1/
+| #I #L #V #T #U1 #l1 #_ #IHTU1 #X #l2 #H
+  elim (ssta_inv_bind1 … H) -H #U2 #HTU2 #H destruct
+  elim (IHTU1 … HTU2) -T /3 width=1/
+| #L #V #T #U1 #l1 #_ #IHTU1 #X #l2 #H
+  elim (ssta_inv_appl1 … H) -H #U2 #HTU2 #H destruct
+  elim (IHTU1 … HTU2) -T /3 width=1/
+| #L #V #W1 #T #U1 #l1 #_ #_ #IHVW1 #IHTU1 #U2 #l2 #H
+  elim (ssta_inv_cast1 … H) -H #W2 #T2 #HVW2 #HTU2 #H destruct
+  elim (IHVW1 … HVW2) -V
+  elim (IHTU1 … HTU2) -T /2 width=1/
+]
+qed-.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma
index 2608f02ce..bb5b3ac4e 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma
@@ -99,3 +99,10 @@ lemma delift_inv_refl_O2: ∀L,T1,T2,d. L ⊢ T1 ▼*[d, 0] ≡ T2 → T1 = T2.
 >(tpss_inv_refl_O2 … HT1) -HT1 #HT2
 >(lift_inv_refl_O2 … HT2) -HT2 //
 qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma delift_fwd_tw: ∀L,T1,T2,d,e. L ⊢ T1 ▼*[d, e] ≡ T2 → #[T1] ≤ #[T2].
+#L #T1 #T2 #d #e * #T #HT1 #HT2
+>(tw_lift … HT2) -T2 /2 width=4 by tpss_fwd_tw /
+qed-.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/thin_delift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/thin_delift.ma
index 7166fa221..97f4e1fde 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/thin_delift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/thin_delift.ma
@@ -81,7 +81,7 @@ lemma thin_delift_tps_conf_le_up: ∀L,U1,U2,d,e. L ⊢ U1 ▶ [d, e] U2 →
                                   d ≤ dd → dd ≤ d + e → d + e ≤ dd + ee →
                                   ∃∃T2. K ⊢ T1 ▶* [d, dd - d] T2 &
                                         L ⊢ U2 ▼*[dd, ee] ≡ T2.
-/3 width=6 by thin_delift_tpss_conf_le_up, tpss_strap/ qed. (**) (* too slow without trace *)
+/3 width=6 by thin_delift_tpss_conf_le_up, tpss_strap2/ qed. (**) (* too slow without trace *)
 
 lemma thin_delift_tpss_conf_be: ∀L,U1,U2,d,e. L ⊢ U1 ▶* [d, e] U2 →
                                 ∀T1,dd,ee. L ⊢ U1 ▼*[dd, ee] ≡ T1 →
diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma
index 0e98ece73..b44570c2f 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma
@@ -40,8 +40,8 @@ qed-.
 
 (* Basic properties *********************************************************)
 
-lemma tpss_strap: ∀L,T1,T,T2,d,e.
-                  L ⊢ T1 ▶ [d, e] T → L ⊢ T ▶* [d, e] T2 → L ⊢ T1 ▶* [d, e] T2. 
+lemma tpss_strap2: ∀L,T1,T,T2,d,e.
+                   L ⊢ T1 ▶ [d, e] T → L ⊢ T ▶* [d, e] T2 → L ⊢ T1 ▶* [d, e] T2. 
 /2 width=3/ qed.
 
 lemma tpss_lsubs_trans: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶* [d, e] T2 →
diff --git a/matita/matita/contribs/lambda_delta/basic_2/unwind/sstas.ma b/matita/matita/contribs/lambda_delta/basic_2/unwind/sstas.ma
new file mode 100644
index 000000000..9152b44ae
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/unwind/sstas.ma
@@ -0,0 +1,106 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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".
+
+(* STRATIFIED UNWIND ON TERMS ***********************************************)
+
+inductive sstas (h:sh) (g:sd h) (L:lenv): relation term ≝
+| sstas_refl: ∀T,U. ⦃h, L⦄ ⊢ T •[g, 0] 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 "stratified unwind (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. ⦃h, L⦄ ⊢ U2 •[g , 0] 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=2/ /3 width=5/
+qed-.
+
+lemma sstas_ind_alt: ∀h,g,L,U2. ∀R:predicate term.
+                     (∀T. ⦃h, L⦄ ⊢ U2 •[g , 0] 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_sort1_aux: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U → ∀k. T = ⋆k →
+                          ∀l. deg h g k l → U = ⋆((next h)^l k).
+#h #g #L #T #U #H @(sstas_ind_alt … H) -T
+[ #U0 #HU0 #k #H #l #Hkl destruct
+  elim (ssta_inv_sort1 … HU0) -L #HkO #_ -U0
+  >(deg_mono … Hkl HkO) -g -l //
+| #T0 #U0 #l0 #HTU0 #_ #IHU0 #k #H #l #Hkl destruct
+  elim (ssta_inv_sort1 … HTU0) -L #HkS #H destruct
+  lapply (deg_mono … Hkl HkS) -Hkl #H destruct
+  >(IHU0 (next h k) ? l0) -IHU0 // /2 width=1/ >iter_SO >iter_n_Sm //
+]
+qed.
+
+lemma sstas_inv_sort1: ∀h,g,L,U,k. ⦃h, L⦄ ⊢ ⋆k •*[g] U → ∀l. deg h g k l →
+                       U = ⋆((next h)^l k).
+/2 width=6/ qed-.
+
+fact sstas_inv_bind1_aux: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U →
+                          ∀J,X,Y. T = ⓑ{J}Y.X →
+                          ∃∃Z. ⦃h, L.ⓑ{J}Y⦄ ⊢ X •*[g] Z & U = ⓑ{J}Y.Z.
+#h #g #L #T #U #H @(sstas_ind_alt … H) -T
+[ #U0 #HU0 #J #X #Y #H destruct
+  elim (ssta_inv_bind1 … HU0) -HU0 #X0 #HX0 #H destruct /3 width=3/
+| #T0 #U0 #l #HTU0 #_ #IHU0 #J #X #Y #H destruct
+  elim (ssta_inv_bind1 … HTU0) -HTU0 #X0 #HX0 #H destruct
+  elim (IHU0 J X0 Y ?) -IHU0 // #X1 #HX01 #H destruct /3 width=4/
+]
+qed.
+
+lemma sstas_inv_bind1: ∀h,g,J,L,Y,X,U. ⦃h, L⦄ ⊢ ⓑ{J}Y.X •*[g] U →
+                       ∃∃Z. ⦃h, L.ⓑ{J}Y⦄ ⊢ X •*[g] Z & U = ⓑ{J}Y.Z.
+/2 width=3/ 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 #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/ qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma sstas_fwd_correct: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U →
+                         ∃∃W. ⦃h, L⦄ ⊢ U •[g, 0] W & ⦃h, L⦄ ⊢ U •*[g] U.
+#h #g #L #T #U #H @(sstas_ind_alt … H) -T /2 width=1/ /3 width=2/
+qed-.
+
+(* Basic_1: removed theorems 7:
+            sty1_bind sty1_abbr sty1_appl sty1_cast2
+	    sty1_lift sty1_correct sty1_trans
+*)
diff --git a/matita/matita/contribs/lambda_delta/basic_2/unwind/sstas_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/unwind/sstas_lift.ma
new file mode 100644
index 000000000..28302d71b
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/unwind/sstas_lift.ma
@@ -0,0 +1,57 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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".
+
+(* STRATIFIED UNWIND ON TERMS ***********************************************)
+
+(* Advanced properties ******************************************************)
+
+lemma sstas_total_S: ∀h,g,L,l,T,U. ⦃h, L⦄ ⊢ T•[g, l + 1]U →
+                     ∃∃W. ⦃h, L⦄ ⊢ T •*[g] W & ⦃h, L⦄ ⊢ U •*[g] W.
+#h #g #L #l @(nat_ind_plus … l) -l
+[ #T #U #HTU
+  elim (ssta_fwd_correct … HTU) /4 width=4/
+| #l #IHl #T #U #HTU
+  elim (ssta_fwd_correct … HTU) <minus_plus_m_m #V #HUV
+  elim (IHl … HUV) -IHl -HUV /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 #HUT1 #L2 #d #e #HL21 #X #HX #U2 #HU12
+  >(lift_mono … HX … HU12) -X
+  elim (lift_total T1 d e) /3 width=10/
+| #T0 #U0 #l0 #HTU0 #_ #IHU01 #L2 #d #e #HL21 #T2 #HT02 #U2 #HU12
+  elim (lift_total U0 d e) /3 width=10/
+]
+qed.
+
+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 #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/lambda_delta/basic_2/unwind/sstas_ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unwind/sstas_ltpss.ma
new file mode 100644
index 000000000..0ef8f47e7
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/unwind/sstas_ltpss.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.ma".
+include "basic_2/unwind/sstas.ma".
+
+(* STRATIFIED UNWIND ON TERMS ***********************************************)
+
+(* Properties about parallel unfold *****************************************)
+
+lemma sstas_ltpss_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 #HUT1 #L2 #d #e #HL12 #U2 #HU12
+  elim (ssta_ltpss_tpss_conf … HUT1 … HL12 … HU12) -HUT1 -HL12 /3 width=3/
+| #T0 #U0 #l0 #HTU0 #_ #IHU01 #L2 #d #e #HL12 #T #HT0
+  elim (ssta_ltpss_tpss_conf … HTU0 … HL12 … HT0) -HTU0 -HT0 #U #HTU #HU0
+  elim (IHU01 … HL12 … HU0) -IHU01 -HL12 -U0 /3 width=4/
+]
+qed.
+
+lemma sstas_ltpss_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_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/lambda_delta/basic_2/unwind/sstas_sstas.ma b/matita/matita/contribs/lambda_delta/basic_2/unwind/sstas_sstas.ma
new file mode 100644
index 000000000..9df5b0b47
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/unwind/sstas_sstas.ma
@@ -0,0 +1,74 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/delift_lift.ma".
+include "basic_2/static/ssta_ssta.ma".
+include "basic_2/unwind/sstas_lift.ma".
+
+(* STRATIFIED UNWIND ON 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-.
+
+lemma sstas_inv_S: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U →
+                   ∀T0,l. ⦃h, L⦄ ⊢ T •[g , l+1] T0 → ⦃h, L⦄ ⊢ T0 •*[g] U.
+#h #g #L #T #U #H @(sstas_ind_alt … H) -T
+[ #U0 #HU0 #T #l #HUT
+  elim (ssta_mono … HUT … HU0) <plus_n_Sm #H destruct
+| #T0 #U0 #l0 #HTU0 #HU0 #_ #T #l #HT0
+  elim (ssta_mono … HT0 … HTU0) -T0 #_ #H destruct -l0 //
+]
+qed-.
+
+(* Main properties **********************************************************)
+
+theorem sstas_mono: ∀h,g,L,T,U1. ⦃h, L⦄ ⊢ T •*[g] U1 →
+                    ∀U2. ⦃h, L⦄ ⊢ T •*[g] U2 → U1 = U2.
+#h #g #L #T #U1 #H @(sstas_ind_alt … H) -T
+[ #T1 #HUT1 #U2 #HU12
+  >(sstas_inv_O … HU12 … HUT1) -h -L -T1 -U2 //
+| #T0 #U0 #l0 #HTU0 #_ #IHU01 #U2 #HU12
+  lapply (sstas_inv_S … HU12 … HTU0) -T0 -l0 /2 width=1/
+]
+qed-.
+
+(* More advancd inversion lemmas ********************************************)
+
+fact sstas_inv_lref1_aux: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U → ∀j. T = #j →
+                          ∃∃I,K,V,W. ⇩[0, j] L ≡ K. ⓑ{I}V & ⦃h, K⦄ ⊢ V •*[g] W &
+                                     L ⊢ U ▼*[0, j + 1] ≡ W.
+#h #g #L #T #U #H @(sstas_ind_alt … H) -T
+[ #T #HUT #j #H destruct
+  elim (ssta_inv_lref1 … HUT) -HUT * #K #V #W [2: #l] #HLK #HVW #HVT
+  [ <plus_n_Sm #H destruct
+  | /3 width=12/
+  ]
+| #T0 #U0 #l0 #HTU0 #HU0 #_ #j #H destruct
+  elim (ssta_inv_lref1 … HTU0) -HTU0 * #K #V #W [2: #l] #HLK #HVW #HVU0
+  [ #_ -HVW
+    lapply (ldrop_fwd_ldrop2 … HLK) #H
+    elim (sstas_inv_lift1 … HU0 … H … HVU0) -HU0 -H -HVU0 /3 width=7/
+  | elim (sstas_total_S … HVW) -HVW #T #HVT #HWT
+    lapply (ldrop_fwd_ldrop2 … HLK) #H
+    elim (sstas_inv_lift1 … HU0 … H … HVU0) -HU0 -H -HVU0 #X #HWX
+    >(sstas_mono … HWX … HWT) -X -W /3 width=7/
+  ]
+]
+qed-.
diff --git a/matita/matita/contribs/lambda_delta/ground_2/arith.ma b/matita/matita/contribs/lambda_delta/ground_2/arith.ma
index c65a47bcc..c51873baa 100644
--- a/matita/matita/contribs/lambda_delta/ground_2/arith.ma
+++ b/matita/matita/contribs/lambda_delta/ground_2/arith.ma
@@ -19,6 +19,9 @@ include "ground_2/star.ma".
 
 (* Equations ****************************************************************)
 
+lemma plus_n_2: ∀n. n + 2 = n + 1 + 1.
+// qed.
+
 lemma le_plus_minus: ∀m,n,p. p ≤ n → m + n - p = m + (n - p).
 /2 by plus_minus/ qed.
 
@@ -66,11 +69,21 @@ lemma false_lt_to_le: ∀x,y. (x < y → ⊥) → y ≤ x.
 #Hxy elim (H Hxy)
 qed-.
 
-(*
-lemma pippo: ∀x,y,z. x < z → y < z - x → x + y < z.
-/3 width=2/
+(* iterators ****************************************************************)
 
-lemma le_or_ge: ∀m,n. m ≤ n ∨ n ≤ m.
-#m #n elim (lt_or_ge m n) /2 width=1/ /3 width=2/
-qed-.
-*)
+(* Note: see also: lib/arithemetcs/bigops.ma *)
+let rec iter (n:nat) (B:Type[0]) (op: B → B) (nil: B) ≝
+  match n with
+   [ O   ⇒ nil
+   | S k ⇒ op (iter k B op nil)
+   ].
+
+interpretation "iterated function" 'exp op n = (iter n ? op).
+
+lemma iter_SO: ∀B:Type[0]. ∀f:B→B. ∀b,l. f^(l+1) b = f (f^l b).
+#B #f #b #l >commutative_plus //
+qed.
+
+lemma iter_n_Sm: ∀B:Type[0]. ∀f:B→B. ∀b,l. f^l (f b) = f (f^l b).
+#B #f #b #l elim l -l normalize //
+qed.
-- 
2.39.2