From f16bbb93ecb40fa40f736e0b1158e1c7676a640a Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sat, 20 Apr 2013 18:21:31 +0000
Subject: [PATCH] - we are committing just the components before "reducibility"
 - first definition of "unfold" - notation bugfix - some refactoring

---
 .../lambdadelta/basic_2/grammar/lenv_px_sn.ma |   9 +-
 .../contribs/lambdadelta/basic_2/notation.ma  | 102 +-----
 .../{substitution => relocation}/fsup.ma      |   2 +-
 .../{substitution => relocation}/gdrop.ma     |   0
 .../gdrop_gdrop.ma                            |   2 +-
 .../{substitution => relocation}/ldrop.ma     |   4 +-
 .../ldrop_append.ma                           |   2 +-
 .../ldrop_lbotr.ma                            |   4 +-
 .../ldrop_ldrop.ma                            |   4 +-
 .../{substitution => relocation}/ldrop_lpx.ma |   2 +-
 .../ldrop_lpx_sn.ma                           |   2 +-
 .../{substitution => relocation}/lift.ma      |   0
 .../{substitution => relocation}/lift_lift.ma |   2 +-
 .../lift_lift_vector.ma                       |   4 +-
 .../lift_vector.ma                            |   2 +-
 .../{substitution => relocation}/lsubr.ma     |   0
 .../lsubr_lbotr.ma                            |   2 +-
 .../lambdadelta/basic_2/static/aaa.ma         |   2 +-
 .../lambdadelta/basic_2/static/aaa_aaa.ma     |   2 +-
 .../lambdadelta/basic_2/static/aaa_lift.ma    |   2 +-
 .../lambdadelta/basic_2/static/aaa_lifts.ma   |   2 +-
 .../lambdadelta/basic_2/static/aaa_lpss.ma    |   4 +-
 .../lambdadelta/basic_2/static/ssta.ma        |   2 +-
 .../lambdadelta/basic_2/static/ssta_lift.ma   |   2 +-
 .../lambdadelta/basic_2/static/ssta_lpss.ma   |   4 +-
 .../basic_2/{unfold => substitution}/cpss.ma  |   6 +-
 .../{unfold => substitution}/cpss_lift.ma     |   6 +-
 .../basic_2/{unfold => substitution}/fsupp.ma |   2 +-
 .../{unfold => substitution}/fsupp_fsupp.ma   |   2 +-
 .../basic_2/{unfold => substitution}/fsups.ma |   4 +-
 .../{unfold => substitution}/fsups_fsups.ma   |   2 +-
 .../basic_2/{unfold => substitution}/gr2.ma   |   0
 .../{unfold => substitution}/gr2_gr2.ma       |   2 +-
 .../{unfold => substitution}/gr2_minus.ma     |   2 +-
 .../{unfold => substitution}/gr2_plus.ma      |   2 +-
 .../{unfold => substitution}/ldrops.ma        |   6 +-
 .../{unfold => substitution}/ldrops_ldrop.ma  |   4 +-
 .../{unfold => substitution}/ldrops_ldrops.ma |   2 +-
 .../basic_2/{unfold => substitution}/lifts.ma |   4 +-
 .../{unfold => substitution}/lifts_lift.ma    |   6 +-
 .../lifts_lift_vector.ma                      |   6 +-
 .../{unfold => substitution}/lifts_lifts.ma   |   2 +-
 .../{unfold => substitution}/lifts_vector.ma  |   4 +-
 .../basic_2/{unfold => substitution}/lpss.ma  |   6 +-
 .../{unfold => substitution}/lpss_cpss.ma     |  10 +-
 .../{unfold => substitution}/lpss_ldrop.ma    |   8 +-
 .../{unfold => substitution}/lpss_lpss.ma     |   4 +-
 .../lambdadelta/basic_2/unfold/cpqs.ma        | 228 ++++++++++++++
 .../lambdadelta/basic_2/unfold/cpqs_lift.ma   |  81 +++++
 .../lambdadelta/basic_2/unfold/lpqs.ma        |  67 ++++
 .../lambdadelta/basic_2/unfold/lpqs_cpqs.ma   | 297 ++++++++++++++++++
 .../lambdadelta/basic_2/unfold/lpqs_ldrop.ma  |  30 ++
 .../lambdadelta/basic_2/unfold/lpqs_lpqs.ma   |  46 +++
 .../lambdadelta/basic_2/unfold/sstas.ma       |  80 +++++
 .../lambdadelta/basic_2/unfold/sstas_aaa.ma   |  25 ++
 .../lambdadelta/basic_2/unfold/sstas_lift.ma  |  52 +++
 .../lambdadelta/basic_2/unfold/sstas_lpss.ma  |  39 +++
 .../lambdadelta/basic_2/unfold/sstas_sstas.ma |  54 ++++
 .../lambdadelta/basic_2/unfold/unfold.ma      |  31 ++
 .../lambdadelta/basic_2/web/basic_2_src.tbl   |  28 +-
 60 files changed, 1134 insertions(+), 177 deletions(-)
 rename matita/matita/contribs/lambdadelta/basic_2/{substitution => relocation}/fsup.ma (98%)
 rename matita/matita/contribs/lambdadelta/basic_2/{substitution => relocation}/gdrop.ma (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{substitution => relocation}/gdrop_gdrop.ma (97%)
 rename matita/matita/contribs/lambdadelta/basic_2/{substitution => relocation}/ldrop.ma (99%)
 rename matita/matita/contribs/lambdadelta/basic_2/{substitution => relocation}/ldrop_append.ma (98%)
 rename matita/matita/contribs/lambdadelta/basic_2/{substitution => relocation}/ldrop_lbotr.ma (97%)
 rename matita/matita/contribs/lambdadelta/basic_2/{substitution => relocation}/ldrop_ldrop.ma (98%)
 rename matita/matita/contribs/lambdadelta/basic_2/{substitution => relocation}/ldrop_lpx.ma (98%)
 rename matita/matita/contribs/lambdadelta/basic_2/{substitution => relocation}/ldrop_lpx_sn.ma (98%)
 rename matita/matita/contribs/lambdadelta/basic_2/{substitution => relocation}/lift.ma (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{substitution => relocation}/lift_lift.ma (99%)
 rename matita/matita/contribs/lambdadelta/basic_2/{substitution => relocation}/lift_lift_vector.ma (94%)
 rename matita/matita/contribs/lambdadelta/basic_2/{substitution => relocation}/lift_vector.ma (98%)
 rename matita/matita/contribs/lambdadelta/basic_2/{substitution => relocation}/lsubr.ma (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{substitution => relocation}/lsubr_lbotr.ma (98%)
 rename matita/matita/contribs/lambdadelta/basic_2/{unfold => substitution}/cpss.ma (97%)
 rename matita/matita/contribs/lambdadelta/basic_2/{unfold => substitution}/cpss_lift.ma (96%)
 rename matita/matita/contribs/lambdadelta/basic_2/{unfold => substitution}/fsupp.ma (98%)
 rename matita/matita/contribs/lambdadelta/basic_2/{unfold => substitution}/fsupp_fsupp.ma (96%)
 rename matita/matita/contribs/lambdadelta/basic_2/{unfold => substitution}/fsups.ma (98%)
 rename matita/matita/contribs/lambdadelta/basic_2/{unfold => substitution}/fsups_fsups.ma (96%)
 rename matita/matita/contribs/lambdadelta/basic_2/{unfold => substitution}/gr2.ma (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{unfold => substitution}/gr2_gr2.ma (97%)
 rename matita/matita/contribs/lambdadelta/basic_2/{unfold => substitution}/gr2_minus.ma (98%)
 rename matita/matita/contribs/lambdadelta/basic_2/{unfold => substitution}/gr2_plus.ma (97%)
 rename matita/matita/contribs/lambdadelta/basic_2/{unfold => substitution}/ldrops.ma (96%)
 rename matita/matita/contribs/lambdadelta/basic_2/{unfold => substitution}/ldrops_ldrop.ma (95%)
 rename matita/matita/contribs/lambdadelta/basic_2/{unfold => substitution}/ldrops_ldrops.ma (96%)
 rename matita/matita/contribs/lambdadelta/basic_2/{unfold => substitution}/lifts.ma (98%)
 rename matita/matita/contribs/lambdadelta/basic_2/{unfold => substitution}/lifts_lift.ma (95%)
 rename matita/matita/contribs/lambdadelta/basic_2/{unfold => substitution}/lifts_lift_vector.ma (92%)
 rename matita/matita/contribs/lambdadelta/basic_2/{unfold => substitution}/lifts_lifts.ma (96%)
 rename matita/matita/contribs/lambdadelta/basic_2/{unfold => substitution}/lifts_vector.ma (96%)
 rename matita/matita/contribs/lambdadelta/basic_2/{unfold => substitution}/lpss.ma (95%)
 rename matita/matita/contribs/lambdadelta/basic_2/{unfold => substitution}/lpss_cpss.ma (96%)
 rename matita/matita/contribs/lambdadelta/basic_2/{unfold => substitution}/lpss_ldrop.ma (87%)
 rename matita/matita/contribs/lambdadelta/basic_2/{unfold => substitution}/lpss_lpss.ma (95%)
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/unfold/cpqs.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/unfold/cpqs_lift.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/unfold/lpqs.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/unfold/lpqs_cpqs.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/unfold/lpqs_ldrop.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/unfold/lpqs_lpqs.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/unfold/sstas.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/unfold/sstas_aaa.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/unfold/sstas_lift.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/unfold/sstas_lpss.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/unfold/sstas_sstas.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/unfold/unfold.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_px_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_px_sn.ma
index e746586ae..d7cdcf595 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_px_sn.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_px_sn.ma
@@ -26,7 +26,7 @@ inductive lpx_sn (R:lenv→relation term): relation lenv ≝
 definition lpx_sn_confluent: relation (lenv→relation term) ≝ λR1,R2.
                              ∀L0,T0,T1. R1 L0 T0 T1 → ∀T2. R2 L0 T0 T2 →
                              ∀L1. lpx_sn R1 L0 L1 → ∀L2. lpx_sn R2 L0 L2 →
-                             ∃∃T. R1 L1 T1 T & R2 L2 T2 T.
+                             ∃∃T. R2 L1 T1 T & R1 L2 T2 T.
 
 definition lpx_sn_transitive: relation (lenv→relation term) ≝ λR1,R2.
                               ∀L1,T1,T. R1 L1 T1 T → ∀L2. lpx_sn R1 L1 L2 →
@@ -130,8 +130,9 @@ lemma lpx_sn_trans: ∀R. lpx_sn_transitive R R → Transitive … (lpx_sn R).
 elim (lpx_sn_inv_pair1 … H) -H #L2 #V2 #HL2 #HV2 #H destruct /3 width=5/
 qed-.
 
-lemma lpx_sn_conf: ∀R. lpx_sn_confluent R R → confluent … (lpx_sn R).
-#R #HR #L0 @(f_ind … length … L0) -L0 #n #IH *
+lemma lpx_sn_conf: ∀R1,R2. lpx_sn_confluent R1 R2 →
+                   confluent2 … (lpx_sn R1) (lpx_sn R2).
+#R1 #R2 #HR12 #L0 @(f_ind … length … L0) -L0 #n #IH *
 [ #_ #X1 #H1 #X2 #H2 -n
   >(lpx_sn_inv_atom1 … H1) -X1
   >(lpx_sn_inv_atom1 … H2) -X2 /2 width=3/
@@ -139,6 +140,6 @@ lemma lpx_sn_conf: ∀R. lpx_sn_confluent R R → confluent … (lpx_sn R).
   elim (lpx_sn_inv_pair1 … H1) -H1 #L1 #V1 #HL01 #HV01 #H destruct
   elim (lpx_sn_inv_pair1 … H2) -H2 #L2 #V2 #HL02 #HV02 #H destruct
   elim (IH … HL01 … HL02) -IH normalize // #L #HL1 #HL2
-  elim (HR … HV01 … HV02 … HL01 … HL02) -L0 -V0 /3 width=5/
+  elim (HR12 … HV01 … HV02 … HL01 … HL02) -L0 -V0 /3 width=5/
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation.ma b/matita/matita/contribs/lambdadelta/basic_2/notation.ma
index 689d6edc2..6a5b14e62 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation.ma
@@ -48,7 +48,7 @@ notation "hvbox( ② { term 46 I } break term 55 T1 . break term 55 T )"
  non associative with precedence 55
  for @{ 'SnItem2 $I $T1 $T }.
 
-notation "hvbox( ⓑ { term 46 a , term 46 I } break term 55 T1 . break term 55 T )"
+notation "hvbox( ⓑ { term 46 a , break term 46 I } break term 55 T1 . break term 55 T )"
  non associative with precedence 55
  for @{ 'SnBind2 $a $I $T1 $T }.
 
@@ -64,7 +64,7 @@ notation "hvbox( ⓕ { term 46 I } break term 55 T1 . break term 55 T )"
  non associative with precedence 55
  for @{ 'SnFlat2 $I $T1 $T }.
 
-notation "hvbox( ⓓ { term 46 a } term 55 T1 . break term 55 T2 )"
+notation "hvbox( ⓓ { term 46 a } break term 55 T1 . break term 55 T2 )"
  non associative with precedence 55
  for @{ 'SnAbbr $a $T1 $T2 }.
 
@@ -76,7 +76,7 @@ notation "hvbox( - ⓓ term 55 T1 . break term 55 T2 )"
  non associative with precedence 55
  for @{ 'SnAbbrNeg $T1 $T2 }.
 
-notation "hvbox( ⓛ { term 46 a } term 55 T1 . break term 55 T2 )"
+notation "hvbox( ⓛ { term 46 a } break term 55 T1 . break term 55 T2 )"
  non associative with precedence 55
  for @{ 'SnAbst $a $T1 $T2 }.
 
@@ -140,7 +140,7 @@ notation "hvbox( T1 ≃ break term 46 T2 )"
    non associative with precedence 45
    for @{ 'Iso $T1 $T2 }.
 
-(* Substitution *************************************************************)
+(* Relocation ***************************************************************)
 
 notation "hvbox( ⇧ [ term 46 d , break term 46 e ] break term 46 T1 ≡ break term 46 T2 )"
    non associative with precedence 45
@@ -170,7 +170,7 @@ notation "hvbox( L ⊢ break ⌘ ⦃ term 46 T ⦄ ≡ break term 46 k )"
    non associative with precedence 45
    for @{ 'ICM $L $T $k }.
 
-(* Unfold *******************************************************************)
+(* Substitution *************************************************************)
 
 notation "hvbox( @ ⦃ term 46 T1 , break term 46 f ⦄ ≡ break term 46 T2 )"
    non associative with precedence 45
@@ -204,22 +204,6 @@ notation "hvbox( T1 ⊢ ▶ * break term 46 T2 )"
    non associative with precedence 45
    for @{ 'PSubstStarSn $T1 $T2 }.
 
-notation "hvbox( ▼ * [ term 46 d , break term 46 e ] break term 46 T1 ≡ break term 46 T2 )"
-   non associative with precedence 45
-   for @{ 'TSubst $T1 $d $e $T2 }.
-
-notation "hvbox( L ⊢ break ▼ * [ term 46 d , break term 46 e ] break term 46 T1 ≡ break term 46 T2 )"
-   non associative with precedence 45
-   for @{ 'TSubst $L $T1 $d $e $T2 }.
-
-notation "hvbox( ▼ ▼ * [ term 46 d , break term 46 e ] break term 46 T1 ≡ break term 46 T2 )"
-   non associative with precedence 45
-   for @{ 'TSubstAlt $T1 $d $e $T2 }.
-
-notation "hvbox( L ⊢ break ▼ ▼ * [ term 46 d , break term 46 e ] break term 46 T1 ≡ break term 46 T2 )"
-   non associative with precedence 45
-   for @{ 'TSubstAlt $L $T1 $d $e $T2 }.
-
 (* Static typing ************************************************************)
 
 notation "hvbox( L ⊢ break term 46 T ⁝ break term 46 A )"
@@ -242,7 +226,7 @@ notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 • br
    non associative with precedence 45
    for @{ 'StaticType $h $g $L $T1 $T2 $l }.
 
-(* Unwind *******************************************************************)
+(* Unfold *******************************************************************)
 
 notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 •* break [ term 46 g ] break term 46 T2 )"
    non associative with precedence 45
@@ -250,9 +234,7 @@ notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 •* b
 
 notation "hvbox( L1 ⊢ ⧫ * break term 46 T ≡ break term 46 L2 )"
    non associative with precedence 45
-   for @{ 'Unwind $L1 $T $L2 }.
-
-(* Restricted ***************************************************************)
+   for @{ 'Unfold $L1 $T $L2 }.
 
 notation "hvbox( L ⊢ break term 46 T1 ➤ * break term 46 T2 )"
    non associative with precedence 45
@@ -262,7 +244,7 @@ notation "hvbox( T1 ⊢ ➤ * break term 46 T2 )"
    non associative with precedence 45
    for @{ 'PRestStarSn $T1 $T2 }.
 
-(* Reducibility *************************************************************)
+(* Reduction ****************************************************************)
 
 notation "hvbox( L ⊢ break 𝐑 ⦃ term 46 T ⦄ )"
    non associative with precedence 45
@@ -314,47 +296,15 @@ notation "hvbox( L1 ⊢ ➡ break term 46 L2 )"
    non associative with precedence 45
    for @{ 'PRedSn $L1 $L2 }.
 
-notation "hvbox( L1 ⊢ ➡ ➡ break term 46 L2 )"
-   non associative with precedence 45
-   for @{ 'PRedSnAlt $L1 $L2 }.
-
-notation "hvbox( ⦃ term 46 L1, break term 46 T1 ⦄ ➡ break ⦃ term 46 L2 , break term 46 T2 ⦄ )"
-   non associative with precedence 45
-   for @{ 'FocalizedPRed $L1 $T1 $L2 $T2 }.
-
-notation "hvbox( L ⊢ break ⦃ term 46 L1, break term 46 T1 ⦄ ➡ break ⦃ term 46 L2 , break term 46 T2 ⦄ )"
-   non associative with precedence 45
-   for @{ 'FocalizedPRed $L $L1 $T1 $L2 $T2 }.
-
 (* Computation **************************************************************)
 
-notation "hvbox( T1 ➡ * break term 46 T2 )"
-   non associative with precedence 45
-   for @{ 'PRedStar $T1 $T2 }.
-
 notation "hvbox( L ⊢ break term 46 T1 ➡ * break term 46 T2 )"
    non associative with precedence 45
    for @{ 'PRedStar $L $T1 $T2 }.
 
-notation "hvbox( T1 ➡ ➡ * break term 46 T2 )"
+notation "hvbox( L1 ⊢ ➡* break term 46 L2 )"
    non associative with precedence 45
-   for @{ 'PRedStarAlt $T1 $T2 }.
-
-notation "hvbox( ⦃ term 46 L1 ⦄ ➡ * break ⦃ term 46 L2 ⦄ )"
-   non associative with precedence 45
-   for @{ 'FocalizedPRedStar $L1 $L2 }.
-
-notation "hvbox( ⦃ term 46 L1 , term 46 T1 ⦄ ➡ * break ⦃ term 46 L2 , term 46 T2 ⦄ )"
-   non associative with precedence 45
-   for @{ 'FocalizedPRedStar $L1 $T1 $L2 $T2 }.
-
-notation "hvbox( ⦃ term 46 L1 ⦄ ➡ ➡ * break ⦃ term 46 L2 ⦄ )"
-   non associative with precedence 45
-   for @{ 'FocalizedPRedStarAlt $L1 $L2 }.
-
-notation "hvbox( ⦃ term 46 L1 , term 46 T1 ⦄ ➡ ➡ * break ⦃ term 46 L2 , term 46 T2 ⦄ )"
-   non associative with precedence 45
-   for @{ 'FocalizedPRedStarAlt $L1 $T1 $L2 $T2 }.
+   for @{ 'PRedSnStar $L1 $L2 }.
 
 notation "hvbox( L ⊢ break term 46 T1 ➡ * break 𝐍 ⦃ term 46 T2 ⦄ )"
    non associative with precedence 45
@@ -394,21 +344,9 @@ notation "hvbox( L ⊢ break term 46 T1 ⬌ break term 46 T2 )"
    non associative with precedence 45
    for @{ 'PConv $L $T1 $T2 }.
 
-notation "hvbox( ⦃ term 46 L1 ⦄ ⬌ break ⦃ term 46 L2 ⦄ )"
-   non associative with precedence 45
-   for @{ 'FocalizedPConv $L1 $L2 }.
-
-notation "hvbox( ⦃ term 46 L1 , break term 46 T1 ⦄ ⬌ break ⦃ term 46 L2 , break term 46 T2 ⦄ )"
+notation "hvbox( L1 ⊢ ⬌ break term 46 L2 )"
    non associative with precedence 45
-   for @{ 'FocalizedPConv $L1 $T1 $L2 $T2 }.
-
-notation "hvbox( ⦃ term 46 L1 ⦄ ⬌ ⬌ break ⦃ term 46 L2 ⦄ )"
-   non associative with precedence 45
-   for @{ 'FocalizedPConvAlt $L1 $L2 }.
-
-notation "hvbox( ⦃ term 46 L1 , break term 46 T1 ⦄ ⬌ ⬌ break ⦃ term 46 L2 , break term 46 T2 ⦄ )"
-   non associative with precedence 45
-   for @{ 'FocalizedPConvAlt $L1 $T1 $L2 $T2 }.
+   for @{ 'PConvSn $L1 $L2 }.
 
 (* Equivalence **************************************************************)
 
@@ -420,21 +358,9 @@ notation "hvbox( h ⊢ break term 46 L1 • ⊑ break [ term 46 g ] break term 4
    non associative with precedence 45
    for @{ 'CrSubEqS $h $g $L1 $L2 }.
 
-notation "hvbox( ⦃ term 46 L1 ⦄ ⬌ * break ⦃ term 46 L2 ⦄ )"
-   non associative with precedence 45
-   for @{ 'FocalizedPConvStar $L1 $L2 }.
-
-notation "hvbox( ⦃ term 46 L1 , break term 46 T1 ⦄ ⬌ * break ⦃ term 46 L2 , break term 46 T2 ⦄ )"
-   non associative with precedence 45
-   for @{ 'FocalizedPConvStar $L1 $T1 $L2 $T2 }.
-
-notation "hvbox( ⦃ term 46 L1 ⦄ ⬌ ⬌ * break ⦃ term 46 L2 ⦄ )"
-   non associative with precedence 45
-   for @{ 'FocalizedPConvStarAlt $L1 $L2 }.
-
-notation "hvbox( ⦃ term 46 L1 , break term 46 T1 ⦄ ⬌ ⬌ * break ⦃ term 46 L2 , break term 46 T2 ⦄ )"
+notation "hvbox( L1 ⊢ ⬌* break term 46 L2 )"
    non associative with precedence 45
-   for @{ 'FocalizedPConvStarAlt $L1 $T1 $L2 $T2 }.
+   for @{ 'PConvSnStar $L1 $L2 }.
 
 (* Dynamic typing ***********************************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fsup.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/fsup.ma
similarity index 98%
rename from matita/matita/contribs/lambdadelta/basic_2/substitution/fsup.ma
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/fsup.ma
index c8e78d9a9..6b0ee2185 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/fsup.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/fsup.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/substitution/ldrop.ma".
+include "basic_2/relocation/ldrop.ma".
 
 (* SUPCLOSURE ***************************************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/gdrop.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/gdrop.ma
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/substitution/gdrop.ma
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/gdrop.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/gdrop_gdrop.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/gdrop_gdrop.ma
similarity index 97%
rename from matita/matita/contribs/lambdadelta/basic_2/substitution/gdrop_gdrop.ma
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/gdrop_gdrop.ma
index 0bc1a40d5..a133e29c6 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/gdrop_gdrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/gdrop_gdrop.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/substitution/gdrop.ma".
+include "basic_2/relocation/gdrop.ma".
 
 (* GLOBAL ENVIRONMENT SLICING ***********************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma
similarity index 99%
rename from matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop.ma
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma
index 8782fa93d..6d91d0aa0 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma
@@ -13,8 +13,8 @@
 (**************************************************************************)
 
 include "basic_2/grammar/cl_weight.ma".
-include "basic_2/substitution/lift.ma".
-include "basic_2/substitution/lsubr.ma".
+include "basic_2/relocation/lift.ma".
+include "basic_2/relocation/lsubr.ma".
 
 (* LOCAL ENVIRONMENT SLICING ************************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_append.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_append.ma
similarity index 98%
rename from matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_append.ma
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_append.ma
index a122f9d45..762911576 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_append.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_append.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/substitution/ldrop.ma".
+include "basic_2/relocation/ldrop.ma".
 
 (* DROPPING *****************************************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_lbotr.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lbotr.ma
similarity index 97%
rename from matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_lbotr.ma
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lbotr.ma
index 1ff849657..df6b2c11e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_lbotr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lbotr.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/substitution/lsubr_lbotr.ma".
-include "basic_2/substitution/ldrop_ldrop.ma".
+include "basic_2/relocation/lsubr_lbotr.ma".
+include "basic_2/relocation/ldrop_ldrop.ma".
 
 (* DROPPING *****************************************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_ldrop.ma
similarity index 98%
rename from matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_ldrop.ma
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_ldrop.ma
index ccbf607ea..88f37fcfb 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_ldrop.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/substitution/lift_lift.ma".
-include "basic_2/substitution/ldrop.ma".
+include "basic_2/relocation/lift_lift.ma".
+include "basic_2/relocation/ldrop.ma".
 
 (* DROPPING *****************************************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lpx.ma
similarity index 98%
rename from matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_lpx.ma
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lpx.ma
index adfbbc038..d23ed28e5 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_lpx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lpx.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/grammar/lenv_px.ma".
-include "basic_2/substitution/ldrop.ma".
+include "basic_2/relocation/ldrop.ma".
 
 (* DROPPING *****************************************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_lpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lpx_sn.ma
similarity index 98%
rename from matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_lpx_sn.ma
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lpx_sn.ma
index 33c1ba2e8..98a7c7157 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_lpx_sn.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lpx_sn.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/grammar/lenv_px_sn.ma".
-include "basic_2/substitution/ldrop.ma".
+include "basic_2/relocation/ldrop.ma".
 
 (* DROPPING *****************************************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lift.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lift.ma
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/substitution/lift.ma
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/lift.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lift_lift.ma
similarity index 99%
rename from matita/matita/contribs/lambdadelta/basic_2/substitution/lift_lift.ma
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/lift_lift.ma
index 804c903d1..c0805dd87 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lift_lift.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/substitution/lift.ma".
+include "basic_2/relocation/lift.ma".
 
 (* BASIC TERM RELOCATION ****************************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_lift_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lift_lift_vector.ma
similarity index 94%
rename from matita/matita/contribs/lambdadelta/basic_2/substitution/lift_lift_vector.ma
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/lift_lift_vector.ma
index cdc11129d..f3ff80d11 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_lift_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lift_lift_vector.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/substitution/lift_lift.ma".
-include "basic_2/substitution/lift_vector.ma".
+include "basic_2/relocation/lift_lift.ma".
+include "basic_2/relocation/lift_vector.ma".
 
 (* BASIC TERM VECTOR RELOCATION *********************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lift_vector.ma
similarity index 98%
rename from matita/matita/contribs/lambdadelta/basic_2/substitution/lift_vector.ma
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/lift_vector.ma
index 35ecb6535..482eea166 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lift_vector.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/grammar/term_vector.ma".
-include "basic_2/substitution/lift.ma".
+include "basic_2/relocation/lift.ma".
 
 (* BASIC TERM VECTOR RELOCATION *********************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lsubr.ma
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr.ma
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/lsubr.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr_lbotr.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lsubr_lbotr.ma
similarity index 98%
rename from matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr_lbotr.ma
rename to matita/matita/contribs/lambdadelta/basic_2/relocation/lsubr_lbotr.ma
index 92593a2ad..26a9530d0 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr_lbotr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lsubr_lbotr.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/substitution/lsubr.ma".
+include "basic_2/relocation/lsubr.ma".
 
 (* LOCAL ENVIRONMENT REFINEMENT FOR SUBSTITUTION ****************************)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/static/aaa.ma
index f9a98fec1..c834d095e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/aaa.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/grammar/aarity.ma".
-include "basic_2/substitution/ldrop.ma".
+include "basic_2/relocation/ldrop.ma".
 
 (* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_aaa.ma
index 9d9017cb5..fce1c02e4 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_aaa.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/substitution/ldrop_ldrop.ma".
+include "basic_2/relocation/ldrop_ldrop.ma".
 include "basic_2/static/aaa.ma".
 
 (* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lift.ma
index b40f1a9b1..992c8139c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lift.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/substitution/ldrop_ldrop.ma".
+include "basic_2/relocation/ldrop_ldrop.ma".
 include "basic_2/static/aaa.ma".
 
 (* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lifts.ma
index 7514f6dc5..7afcc4131 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lifts.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lifts.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/unfold/ldrops.ma".
+include "basic_2/substitution/ldrops.ma".
 include "basic_2/static/aaa_lift.ma".
 
 (* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lpss.ma b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lpss.ma
index c85d406e8..e930823ad 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lpss.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lpss.ma
@@ -12,12 +12,12 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/unfold/lpss_ldrop.ma".
+include "basic_2/substitution/lpss_ldrop.ma".
 include "basic_2/static/aaa_lift.ma".
 
 (* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************)
 
-(* Properties about sn parallel unfold **************************************)
+(* Properties about sn parallel substitution ********************************)
 
 (* Note: lemma 500 *)
 lemma aaa_cpss_lpss_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → ∀T2. L1 ⊢ T1 ▶* T2 →
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ssta.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ssta.ma
index 4f0300f00..7f86bf0af 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/ssta.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/ssta.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/substitution/ldrop.ma".
+include "basic_2/relocation/ldrop.ma".
 include "basic_2/static/sd.ma".
 
 (* STRATIFIED STATIC TYPE ASSIGNMENT ON TERMS *******************************)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_lift.ma
index c0a6b2b97..10585d61d 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_lift.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/substitution/ldrop_ldrop.ma".
+include "basic_2/relocation/ldrop_ldrop.ma".
 include "basic_2/static/ssta.ma".
 
 (* STRATIFIED STATIC TYPE ASSIGNMENT ON TERMS *******************************)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_lpss.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_lpss.ma
index 0aacb2b63..5012fd975 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_lpss.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_lpss.ma
@@ -12,12 +12,12 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/unfold/lpss_ldrop.ma".
+include "basic_2/substitution/lpss_ldrop.ma".
 include "basic_2/static/ssta_lift.ma".
 
 (* STRATIFIED STATIC TYPE ASSIGNMENT ON TERMS *******************************)
 
-(* Properties about sn parallel unfold **************************************)
+(* Properties about sn parallel substitution ********************************)
 
 (* Note: apparently this was missing in basic_1 *)
 lemma ssta_tpss_lpss_conf: ∀h,g,L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l, U1⦄ →
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/cpss.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpss.ma
similarity index 97%
rename from matita/matita/contribs/lambdadelta/basic_2/unfold/cpss.ma
rename to matita/matita/contribs/lambdadelta/basic_2/substitution/cpss.ma
index 4bbf47bdf..993669ad4 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/cpss.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpss.ma
@@ -12,9 +12,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/substitution/ldrop_append.ma".
+include "basic_2/relocation/ldrop_append.ma".
 
-(* CONTEXT-SENSITIVE PARALLEL UNFOLD FOR TERMS ******************************)
+(* CONTEXT-SENSITIVE PARALLEL SUBSTITUTION FOR TERMS ************************)
 
 inductive cpss: lenv → relation term ≝
 | cpss_atom : ∀I,L. cpss L (⓪{I}) (⓪{I})
@@ -29,7 +29,7 @@ inductive cpss: lenv → relation term ≝
               cpss L (ⓕ{I} V1. T1) (ⓕ{I} V2. T2)
 .
 
-interpretation "context-sensitive parallel unfold (term)"
+interpretation "context-sensitive parallel substitution (term)"
    'PSubstStar L T1 T2 = (cpss L T1 T2).
 
 (* Basic properties *********************************************************)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/cpss_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpss_lift.ma
similarity index 96%
rename from matita/matita/contribs/lambdadelta/basic_2/unfold/cpss_lift.ma
rename to matita/matita/contribs/lambdadelta/basic_2/substitution/cpss_lift.ma
index d41e0ac18..9745b6cde 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/cpss_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpss_lift.ma
@@ -12,10 +12,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/substitution/ldrop_ldrop.ma".
-include "basic_2/unfold/cpss.ma".
+include "basic_2/relocation/ldrop_ldrop.ma".
+include "basic_2/substitution/cpss.ma".
 
-(* CONTEXT-SENSITIVE PARALLEL UNFOLD FOR TERMS ******************************)
+(* CONTEXT-SENSITIVE PARALLEL SUBSTITUTION FOR TERMS ************************)
 
 (* Relocation properties ****************************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/fsupp.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fsupp.ma
similarity index 98%
rename from matita/matita/contribs/lambdadelta/basic_2/unfold/fsupp.ma
rename to matita/matita/contribs/lambdadelta/basic_2/substitution/fsupp.ma
index f0fde0f1f..a35be783f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/fsupp.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fsupp.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/substitution/fsup.ma".
+include "basic_2/relocation/fsup.ma".
 
 (* PLUS-ITERATED SUPCLOSURE *************************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/fsupp_fsupp.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fsupp_fsupp.ma
similarity index 96%
rename from matita/matita/contribs/lambdadelta/basic_2/unfold/fsupp_fsupp.ma
rename to matita/matita/contribs/lambdadelta/basic_2/substitution/fsupp_fsupp.ma
index a546fc265..9380a99df 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/fsupp_fsupp.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fsupp_fsupp.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/unfold/fsupp.ma".
+include "basic_2/substitution/fsupp.ma".
 
 (* PLUS-ITERATED SUPCLOSURE *************************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/fsups.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fsups.ma
similarity index 98%
rename from matita/matita/contribs/lambdadelta/basic_2/unfold/fsups.ma
rename to matita/matita/contribs/lambdadelta/basic_2/substitution/fsups.ma
index bee55674d..a7a4dbde4 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/fsups.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fsups.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/unfold/fsupp.ma".
+include "basic_2/substitution/fsupp.ma".
 
 (* STAR-ITERATED SUPCLOSURE *************************************************)
 
@@ -90,4 +90,4 @@ lemma fsupp_inv_flat1_fsups: ∀J,L1,L2,W,U,T2. ⦃L1, ⓕ{J}W.U⦄ ⊃+ ⦃L2,
 | #L #T #L2 #T2 #_ #HT2 * /3 width=4/
 ]
 qed-.
-*)
\ No newline at end of file
+*)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/fsups_fsups.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fsups_fsups.ma
similarity index 96%
rename from matita/matita/contribs/lambdadelta/basic_2/unfold/fsups_fsups.ma
rename to matita/matita/contribs/lambdadelta/basic_2/substitution/fsups_fsups.ma
index 1c4b366c4..ff3bdb494 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/fsups_fsups.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fsups_fsups.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/unfold/fsups.ma".
+include "basic_2/substitution/fsups.ma".
 
 (* STAR-ITERATED SUPCLOSURE *************************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/gr2.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/gr2.ma
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/unfold/gr2.ma
rename to matita/matita/contribs/lambdadelta/basic_2/substitution/gr2.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/gr2_gr2.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/gr2_gr2.ma
similarity index 97%
rename from matita/matita/contribs/lambdadelta/basic_2/unfold/gr2_gr2.ma
rename to matita/matita/contribs/lambdadelta/basic_2/substitution/gr2_gr2.ma
index 20ce856d6..9e8ced3a8 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/gr2_gr2.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/gr2_gr2.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/unfold/gr2.ma".
+include "basic_2/substitution/gr2.ma".
 
 (* GENERIC RELOCATION WITH PAIRS ********************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/gr2_minus.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/gr2_minus.ma
similarity index 98%
rename from matita/matita/contribs/lambdadelta/basic_2/unfold/gr2_minus.ma
rename to matita/matita/contribs/lambdadelta/basic_2/substitution/gr2_minus.ma
index 41d18409b..3a98ab728 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/gr2_minus.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/gr2_minus.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/unfold/gr2.ma".
+include "basic_2/substitution/gr2.ma".
 
 (* GENERIC RELOCATION WITH PAIRS ********************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/gr2_plus.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/gr2_plus.ma
similarity index 97%
rename from matita/matita/contribs/lambdadelta/basic_2/unfold/gr2_plus.ma
rename to matita/matita/contribs/lambdadelta/basic_2/substitution/gr2_plus.ma
index 82366bc72..fc1618572 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/gr2_plus.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/gr2_plus.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/unfold/gr2.ma".
+include "basic_2/substitution/gr2.ma".
 
 (* GENERIC RELOCATION WITH PAIRS ********************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/ldrops.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops.ma
similarity index 96%
rename from matita/matita/contribs/lambdadelta/basic_2/unfold/ldrops.ma
rename to matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops.ma
index 9af21a0f1..328860016 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/ldrops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops.ma
@@ -12,9 +12,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/substitution/ldrop.ma".
-include "basic_2/unfold/gr2_minus.ma".
-include "basic_2/unfold/lifts.ma".
+include "basic_2/relocation/ldrop.ma".
+include "basic_2/substitution/gr2_minus.ma".
+include "basic_2/substitution/lifts.ma".
 
 (* GENERIC LOCAL ENVIRONMENT SLICING ****************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/ldrops_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops_ldrop.ma
similarity index 95%
rename from matita/matita/contribs/lambdadelta/basic_2/unfold/ldrops_ldrop.ma
rename to matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops_ldrop.ma
index 6ca2f73df..9712e3277 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/ldrops_ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops_ldrop.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/substitution/ldrop_ldrop.ma".
-include "basic_2/unfold/ldrops.ma".
+include "basic_2/relocation/ldrop_ldrop.ma".
+include "basic_2/substitution/ldrops.ma".
 
 (* GENERIC LOCAL ENVIRONMENT SLICING ****************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/ldrops_ldrops.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops_ldrops.ma
similarity index 96%
rename from matita/matita/contribs/lambdadelta/basic_2/unfold/ldrops_ldrops.ma
rename to matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops_ldrops.ma
index 7709561a2..a4dbfb02e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/ldrops_ldrops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops_ldrops.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/unfold/ldrops_ldrop.ma".
+include "basic_2/substitution/ldrops_ldrop.ma".
 
 (* GENERIC LOCAL ENVIRONMENT SLICING ****************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lifts.ma
similarity index 98%
rename from matita/matita/contribs/lambdadelta/basic_2/unfold/lifts.ma
rename to matita/matita/contribs/lambdadelta/basic_2/substitution/lifts.ma
index 40158acbe..8d1576005 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/lifts.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lifts.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/substitution/lift.ma".
-include "basic_2/unfold/gr2_plus.ma".
+include "basic_2/relocation/lift.ma".
+include "basic_2/substitution/gr2_plus.ma".
 
 (* GENERIC TERM RELOCATION **************************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lifts_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lifts_lift.ma
similarity index 95%
rename from matita/matita/contribs/lambdadelta/basic_2/unfold/lifts_lift.ma
rename to matita/matita/contribs/lambdadelta/basic_2/substitution/lifts_lift.ma
index 0710f34ae..a9c70ba7a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/lifts_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lifts_lift.ma
@@ -12,9 +12,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/substitution/lift_lift.ma".
-include "basic_2/unfold/gr2_minus.ma".
-include "basic_2/unfold/lifts.ma".
+include "basic_2/relocation/lift_lift.ma".
+include "basic_2/substitution/gr2_minus.ma".
+include "basic_2/substitution/lifts.ma".
 
 (* GENERIC TERM RELOCATION **************************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lifts_lift_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lifts_lift_vector.ma
similarity index 92%
rename from matita/matita/contribs/lambdadelta/basic_2/unfold/lifts_lift_vector.ma
rename to matita/matita/contribs/lambdadelta/basic_2/substitution/lifts_lift_vector.ma
index 7d1419747..9bb8d0023 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/lifts_lift_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lifts_lift_vector.ma
@@ -12,9 +12,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/substitution/lift_lift_vector.ma".
-include "basic_2/unfold/lifts_lift.ma".
-include "basic_2/unfold/lifts_vector.ma".
+include "basic_2/relocation/lift_lift_vector.ma".
+include "basic_2/substitution/lifts_lift.ma".
+include "basic_2/substitution/lifts_vector.ma".
 
 (* GENERIC RELOCATION *******************************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lifts_lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lifts_lifts.ma
similarity index 96%
rename from matita/matita/contribs/lambdadelta/basic_2/unfold/lifts_lifts.ma
rename to matita/matita/contribs/lambdadelta/basic_2/substitution/lifts_lifts.ma
index 72948f04b..bfe0d2529 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/lifts_lifts.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lifts_lifts.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/unfold/lifts_lift.ma".
+include "basic_2/substitution/lifts_lift.ma".
 
 (* GENERIC RELOCATION *******************************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lifts_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lifts_vector.ma
similarity index 96%
rename from matita/matita/contribs/lambdadelta/basic_2/unfold/lifts_vector.ma
rename to matita/matita/contribs/lambdadelta/basic_2/substitution/lifts_vector.ma
index 9ea173a56..7046c9d32 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/lifts_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lifts_vector.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/substitution/lift_vector.ma".
-include "basic_2/unfold/lifts.ma".
+include "basic_2/relocation/lift_vector.ma".
+include "basic_2/substitution/lifts.ma".
 
 (* GENERIC TERM VECTOR RELOCATION *******************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lpss.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lpss.ma
similarity index 95%
rename from matita/matita/contribs/lambdadelta/basic_2/unfold/lpss.ma
rename to matita/matita/contribs/lambdadelta/basic_2/substitution/lpss.ma
index d0c856b9f..d440960f1 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/lpss.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lpss.ma
@@ -13,14 +13,14 @@
 (**************************************************************************)
 
 include "basic_2/grammar/lenv_px_sn.ma".
-include "basic_2/unfold/cpss.ma".
+include "basic_2/substitution/cpss.ma".
 
-(* SN PARALLEL UNFOLD FOR LOCAL ENVIRONMENTS ********************************)
+(* SN PARALLEL SUBSTITUTION FOR LOCAL ENVIRONMENTS **************************)
 
 (* Basic_1: includes: csubst1_bind *)
 definition lpss: relation lenv ≝ lpx_sn cpss. 
 
-interpretation "parallel unfold (local environment, sn variant)"
+interpretation "parallel substitution (local environment, sn variant)"
    'PSubstStarSn L1 L2 = (lpss L1 L2).
 
 (* Basic inversion lemmas ***************************************************)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lpss_cpss.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lpss_cpss.ma
similarity index 96%
rename from matita/matita/contribs/lambdadelta/basic_2/unfold/lpss_cpss.ma
rename to matita/matita/contribs/lambdadelta/basic_2/substitution/lpss_cpss.ma
index 6c060f88f..a67eaeb05 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/lpss_cpss.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lpss_cpss.ma
@@ -12,12 +12,12 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/substitution/fsup.ma".
-include "basic_2/unfold/lpss_ldrop.ma".
+include "basic_2/relocation/fsup.ma".
+include "basic_2/substitution/lpss_ldrop.ma".
 
-(* SN PARALLEL UNFOLD FOR LOCAL ENVIRONMENTS ********************************)
+(* SN PARALLEL SUBSTITUTION FOR LOCAL ENVIRONMENTS **************************)
 
-(* Main properties on context-sensitive parallel unfold for terms ***********)
+(* Main properties on context-sensitive parallel substitution for terms *****)
 
 fact cpss_conf_lpss_atom_atom:
    ∀I,L1,L2. ∃∃T. L1 ⊢ ⓪{I} ▶* T & L2 ⊢ ⓪{I} ▶* T.
@@ -171,7 +171,7 @@ qed-.
 theorem cpss_trans: ∀L. Transitive … (cpss L).
 /2 width=5 by cpss_trans_lpss/ qed-.
 
-(* Properties on context-sensitive parallel unfold for terms ****************)
+(* Properties on context-sensitive parallel substitution for terms **********)
 
 (* Basic_1: was only: subst1_subst1_back *)
 lemma lpss_cpss_conf_dx: ∀L0,T0,T1. L0 ⊢ T0 ▶* T1 → ∀L1. L0 ⊢ ▶* L1 →
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lpss_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lpss_ldrop.ma
similarity index 87%
rename from matita/matita/contribs/lambdadelta/basic_2/unfold/lpss_ldrop.ma
rename to matita/matita/contribs/lambdadelta/basic_2/substitution/lpss_ldrop.ma
index 06a1f0569..044293b27 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/lpss_ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lpss_ldrop.ma
@@ -12,11 +12,11 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/substitution/ldrop_lpx_sn.ma".
-include "basic_2/unfold/cpss_lift.ma".
-include "basic_2/unfold/lpss.ma".
+include "basic_2/relocation/ldrop_lpx_sn.ma".
+include "basic_2/substitution/cpss_lift.ma".
+include "basic_2/substitution/lpss.ma".
 
-(* SN PARALLEL UNFOLD FOR LOCAL ENVIRONMENTS ********************************)
+(* SN PARALLEL SUBSTITUTION FOR LOCAL ENVIRONMENTS **************************)
 
 (* Properies on local environment slicing ***********************************)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lpss_lpss.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lpss_lpss.ma
similarity index 95%
rename from matita/matita/contribs/lambdadelta/basic_2/unfold/lpss_lpss.ma
rename to matita/matita/contribs/lambdadelta/basic_2/substitution/lpss_lpss.ma
index 8f0225255..06223fbee 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/lpss_lpss.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lpss_lpss.ma
@@ -12,9 +12,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/unfold/lpss_cpss.ma".
+include "basic_2/substitution/lpss_cpss.ma".
 
-(* SN PARALLEL UNFOLD ON LOCAL ENVIRONMENTS *********************************)
+(* SN PARALLEL SUBSTITUTION ON LOCAL ENVIRONMENTS ***************************)
 
 (* Main properties **********************************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/cpqs.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/cpqs.ma
new file mode 100644
index 000000000..dbe7beff1
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/cpqs.ma
@@ -0,0 +1,228 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/cpss.ma".
+
+(* CONTEXT-SENSITIVE RESTRICTED PARALLEL COMPUTATION FOR TERMS **************)
+
+inductive cpqs: lenv → relation term ≝
+| cpqs_atom : ∀I,L. cpqs L (⓪{I}) (⓪{I})
+| cpqs_delta: ∀L,K,V,V2,W2,i.
+              ⇩[0, i] L ≡ K. ⓓV → cpqs K V V2 →
+              ⇧[0, i + 1] V2 ≡ W2 → cpqs L (#i) W2
+| cpqs_bind : ∀a,I,L,V1,V2,T1,T2.
+              cpqs L V1 V2 → cpqs (L. ⓑ{I} V1) T1 T2 →
+              cpqs L (ⓑ{a,I} V1. T1) (ⓑ{a,I} V2. T2)
+| cpqs_flat : ∀I,L,V1,V2,T1,T2.
+              cpqs L V1 V2 → cpqs L T1 T2 →
+              cpqs L (ⓕ{I} V1. T1) (ⓕ{I} V2. T2)
+| cpqs_zeta : ∀L,V,T1,T,T2. cpqs (L.ⓓV) T1 T →
+              ⇧[0, 1] T2 ≡ T → cpqs L (+ⓓV. T1) T2
+| cpqs_tau  : ∀L,V,T1,T2. cpqs L T1 T2 → cpqs L (ⓝV. T1) T2
+.
+
+interpretation "context-sensitive restricted parallel computation (term)"
+   'PRestStar L T1 T2 = (cpqs L T1 T2).
+
+(* Basic properties *********************************************************)
+
+(* Note: it does not hold replacing |L1| with |L2| *)
+lemma cpqs_lsubr_trans: ∀L1,T1,T2. L1 ⊢ T1 ➤* T2 →
+                        ∀L2. L2 ⊑ [0, |L1|] L1 → L2 ⊢ T1 ➤* T2.
+#L1 #T1 #T2 #H elim H -L1 -T1 -T2
+[ //
+| #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
+  lapply (ldrop_fwd_ldrop2_length … HLK1) #Hi
+  lapply (ldrop_fwd_O1_length … HLK1) #H2i
+  elim (ldrop_lsubr_ldrop2_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // -Hi
+  <H2i -H2i <minus_plus_m_m /3 width=6/
+| /4 width=1/
+|4,6: /3 width=1/
+| /4 width=3/
+]
+qed-.
+
+lemma cpss_cpqs: ∀L,T1,T2. L ⊢ T1 ▶* T2 → L ⊢ T1 ➤* T2.
+#L #T1 #T2 #H elim H -L -T1 -T2 // /2 width=1/ /2 width=6/
+qed.
+
+lemma cpqs_refl: ∀T,L. L ⊢ T ➤* T.
+/2 width=1/ qed.
+
+lemma cpqs_delift: ∀L,K,V,T1,d. ⇩[0, d] L ≡ (K. ⓓV) →
+                   ∃∃T2,T. L ⊢ T1 ➤* T2 & ⇧[d, 1] T ≡ T2.
+#L #K #V #T1 #d #HLK
+elim (cpss_delift … T1 … HLK) -HLK /3 width=4/
+qed-.
+
+lemma cpqs_append: l_appendable_sn … cpqs.
+#K #T1 #T2 #H elim H -K -T1 -T2 // /2 width=1/ /2 width=3/
+#K #K0 #V1 #V2 #W2 #i #HK0 #_ #HVW2 #IHV12 #L
+lapply (ldrop_fwd_ldrop2_length … HK0) #H
+@(cpqs_delta … (L@@K0) V1 … HVW2) //
+@(ldrop_O1_append_sn_le … HK0) /2 width=2/ (**) (* /3/ does not work *)
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact cpqs_inv_atom1_aux: ∀L,T1,T2. L ⊢ T1 ➤* T2 → ∀I. T1 = ⓪{I} →
+                         T2 = ⓪{I} ∨
+                         ∃∃K,V,V2,i. ⇩[O, i] L ≡ K. ⓓV &
+                                     K ⊢ V ➤* V2 &
+                                     ⇧[O, i + 1] V2 ≡ T2 &
+                                     I = LRef i.
+#L #T1 #T2 * -L -T1 -T2
+[ #I #L #J #H destruct /2 width=1/
+| #L #K #V #V2 #T2 #i #HLK #HV2 #HVT2 #J #H destruct /3 width=8/
+| #a #I #L #V1 #V2 #T1 #T2 #_ #_ #J #H destruct
+| #I #L #V1 #V2 #T1 #T2 #_ #_ #J #H destruct
+| #L #V #T1 #T #T2 #_ #_ #J #H destruct
+| #L #V #T1 #T2 #_ #J #H destruct
+]
+qed-.
+
+lemma cpqs_inv_atom1: ∀I,L,T2. L ⊢ ⓪{I} ➤* T2 →
+                      T2 = ⓪{I} ∨
+                      ∃∃K,V,V2,i. ⇩[O, i] L ≡ K. ⓓV &
+                                  K ⊢ V ➤* V2 &
+                                  ⇧[O, i + 1] V2 ≡ T2 &
+                                  I = LRef i.
+/2 width=3 by cpqs_inv_atom1_aux/ qed-.
+
+lemma cpqs_inv_sort1: ∀L,T2,k. L ⊢ ⋆k ➤* T2 → T2 = ⋆k.
+#L #T2 #k #H
+elim (cpqs_inv_atom1 … H) -H //
+* #K #V #V2 #i #_ #_ #_ #H destruct
+qed-.
+
+lemma cpqs_inv_lref1: ∀L,T2,i. L ⊢ #i ➤* T2 →
+                      T2 = #i ∨
+                      ∃∃K,V,V2. ⇩[O, i] L ≡ K. ⓓV &
+                                K ⊢ V ➤* V2 &
+                                ⇧[O, i + 1] V2 ≡ T2.
+#L #T2 #i #H
+elim (cpqs_inv_atom1 … H) -H /2 width=1/
+* #K #V #V2 #j #HLK #HV2 #HVT2 #H destruct /3 width=6/
+qed-.
+
+lemma cpqs_inv_gref1: ∀L,T2,p. L ⊢ §p ➤* T2 → T2 = §p.
+#L #T2 #p #H
+elim (cpqs_inv_atom1 … H) -H //
+* #K #V #V2 #i #_ #_ #_ #H destruct
+qed-.
+
+fact cpqs_inv_bind1_aux: ∀L,U1,U2. L ⊢ U1 ➤* U2 →
+                         ∀a,I,V1,T1. U1 = ⓑ{a,I} V1. T1 → (
+                         ∃∃V2,T2. L ⊢ V1 ➤* V2 &
+                                  L. ⓑ{I} V1 ⊢ T1 ➤* T2 &
+                                  U2 = ⓑ{a,I} V2. T2
+                         ) ∨
+                         ∃∃T. L.ⓓV1 ⊢ T1 ➤* T & ⇧[0, 1] U2 ≡ T & a = true & I = Abbr.
+#L #U1 #U2 * -L -U1 -U2
+[ #I #L #b #J #W1 #U1 #H destruct
+| #L #K #V #V2 #W2 #i #_ #_ #_ #b #J #W1 #U1 #H destruct
+| #a #I #L #V1 #V2 #T1 #T2 #HV12 #HT12 #b #J #W1 #U1 #H destruct /3 width=5/
+| #I #L #V1 #V2 #T1 #T2 #_ #_ #b #J #W1 #U1 #H destruct
+| #L #V #T1 #T #T2 #HT1 #HT2 #b #J #W1 #U1 #H destruct /3 width=3/
+| #L #V #T1 #T2 #_ #b #J #W1 #U1 #H destruct
+]
+qed-.
+
+lemma cpqs_inv_bind1: ∀a,I,L,V1,T1,U2. L ⊢ ⓑ{a,I} V1. T1 ➤* U2 → (
+                      ∃∃V2,T2. L ⊢ V1 ➤* V2 &
+                               L. ⓑ{I} V1 ⊢ T1 ➤* T2 &
+                               U2 = ⓑ{a,I} V2. T2
+                      ) ∨
+                      ∃∃T. L.ⓓV1 ⊢ T1 ➤* T & ⇧[0, 1] U2 ≡ T & a = true & I = Abbr.
+/2 width=3 by cpqs_inv_bind1_aux/ qed-.
+
+lemma cpqs_inv_abbr1: ∀a,L,V1,T1,U2. L ⊢ ⓓ{a} V1. T1 ➤* U2 → (
+                      ∃∃V2,T2. L ⊢ V1 ➤* V2 &
+                               L. ⓓ V1 ⊢ T1 ➤* T2 &
+                               U2 = ⓓ{a} V2. T2
+                      ) ∨
+                      ∃∃T. L.ⓓV1 ⊢ T1 ➤* T & ⇧[0, 1] U2 ≡ T & a = true.
+#a #L #V1 #T1 #U2 #H
+elim (cpqs_inv_bind1 … H) -H * /3 width=3/ /3 width=5/
+qed-.
+
+lemma cpqs_inv_abst1: ∀a,L,V1,T1,U2. L ⊢ ⓛ{a} V1. T1 ➤* U2 →
+                      ∃∃V2,T2. L ⊢ V1 ➤* V2 &
+                               L. ⓛ V1 ⊢ T1 ➤* T2 &
+                               U2 = ⓛ{a} V2. T2.
+#a #L #V1 #T1 #U2 #H
+elim (cpqs_inv_bind1 … H) -H *
+[ /3 width=5/
+| #T #_ #_ #_ #H destruct
+]
+qed-.
+
+fact cpqs_inv_flat1_aux: ∀L,U1,U2. L ⊢ U1 ➤* U2 →
+                         ∀I,V1,T1. U1 = ⓕ{I} V1. T1 → (
+                         ∃∃V2,T2. L ⊢ V1 ➤* V2 & L ⊢ T1 ➤* T2 &
+                                  U2 = ⓕ{I} V2. T2
+                         ) ∨
+                         (L ⊢ T1 ➤* U2 ∧ I = Cast).
+#L #U1 #U2 * -L -U1 -U2
+[ #I #L #J #W1 #U1 #H destruct
+| #L #K #V #V2 #W2 #i #_ #_ #_ #J #W1 #U1 #H destruct
+| #a #I #L #V1 #V2 #T1 #T2 #_ #_ #J #W1 #U1 #H destruct
+| #I #L #V1 #V2 #T1 #T2 #HV12 #HT12 #J #W1 #U1 #H destruct /3 width=5/
+| #L #V #T1 #T #T2 #_ #_ #J #W1 #U1 #H destruct
+| #L #V #T1 #T2 #HT12 #J #W1 #U1 #H destruct /3 width=1/
+]
+qed-.
+
+lemma cpqs_inv_flat1: ∀I,L,V1,T1,U2. L ⊢ ⓕ{I} V1. T1 ➤* U2 → (
+                      ∃∃V2,T2. L ⊢ V1 ➤* V2 & L ⊢ T1 ➤* T2 &
+                               U2 = ⓕ{I} V2. T2
+                      ) ∨
+                      (L ⊢ T1 ➤* U2 ∧ I = Cast).
+/2 width=3 by cpqs_inv_flat1_aux/ qed-.
+
+lemma cpqs_inv_appl1: ∀L,V1,T1,U2. L ⊢ ⓐ V1. T1 ➤* U2 →
+                      ∃∃V2,T2. L ⊢ V1 ➤* V2 & L ⊢ T1 ➤* T2 &
+                               U2 = ⓐ V2. T2.
+#L #V1 #T1 #U2 #H elim (cpqs_inv_flat1 … H) -H *
+[ /3 width=5/
+| #_ #H destruct
+]
+qed-.
+
+lemma cpqs_inv_cast1: ∀L,V1,T1,U2. L ⊢ ⓝ V1. T1 ➤* U2 → (
+                      ∃∃V2,T2. L ⊢ V1 ➤* V2 & L ⊢ T1 ➤* T2 &
+                               U2 = ⓝ V2. T2
+                      ) ∨
+                      L ⊢ T1 ➤* U2.
+#L #V1 #T1 #U2 #H elim (cpqs_inv_flat1 … H) -H * /2 width=1/ /3 width=5/
+qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma cpqs_fwd_shift1: ∀L1,L,T1,T. L ⊢ L1 @@ T1 ➤* T →
+                       ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2.
+#L1 @(lenv_ind_dx … L1) -L1 normalize
+[ #L #T1 #T #HT1
+  @(ex2_2_intro … (⋆)) // (**) (* explicit constructor *)
+| #I #L1 #V1 #IH #L #T1 #X
+  >shift_append_assoc normalize #H
+  elim (cpqs_inv_bind1 … H) -H *
+  [ #V0 #T0 #_ #HT10 #H destruct
+    elim (IH … HT10) -IH -HT10 #L2 #T2 #HL12 #H destruct
+    >append_length >HL12 -HL12
+    @(ex2_2_intro … (⋆.ⓑ{I}V0@@L2) T2) [ >append_length ] // /2 width=3/ (**) (* explicit constructor *)
+  | #T #_ #_ #H destruct
+  ]
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/cpqs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/cpqs_lift.ma
new file mode 100644
index 000000000..78529b6b1
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/cpqs_lift.ma
@@ -0,0 +1,81 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/relocation/ldrop_ldrop.ma".
+include "basic_2/unfold/cpqs.ma".
+
+(* CONTEXT-SENSITIVE RESTRICTED PARALLEL COMPUTATION FOR TERMS **************)
+
+(* Relocation properties ****************************************************)
+
+lemma cpqs_lift: l_liftable cpqs.
+#K #T1 #T2 #H elim H -K -T1 -T2
+[ #I #K #L #d #e #_ #U1 #H1 #U2 #H2
+  >(lift_mono … H1 … H2) -H1 -H2 //
+| #K #KV #V #V2 #W2 #i #HKV #HV2 #HVW2 #IHV2 #L #d #e #HLK #U1 #H #U2 #HWU2
+  elim (lift_inv_lref1 … H) * #Hid #H destruct
+  [ elim (lift_trans_ge … HVW2 … HWU2) -W2 // <minus_plus #W2 #HVW2 #HWU2
+    elim (ldrop_trans_le … HLK … HKV) -K /2 width=2/ #X #HLK #H
+    elim (ldrop_inv_skip2 … H) -H /2 width=1/ -Hid #K #Y #HKV #HVY #H destruct /3 width=8/
+  | lapply (lift_trans_be … HVW2 … HWU2 ? ?) -W2 // /2 width=1/ >plus_plus_comm_23 #HVU2
+    lapply (ldrop_trans_ge_comm … HLK … HKV ?) -K // -Hid /3 width=6/
+  ]
+| #a #I #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #U1 #H1 #U2 #H2
+  elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct
+  elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /4 width=5/
+| #I #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #U1 #H1 #U2 #H2
+  elim (lift_inv_flat1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct
+  elim (lift_inv_flat1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /3 width=6/
+| #K #V #T1 #T #T2 #_ #HT2 #IHT1 #L #d #e #HLK #U1 #H #U2 #HTU2
+  elim (lift_inv_bind1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct
+  elim (lift_conf_O1 … HTU2 … HT2) -T2 /4 width=5/
+| #K #V #T1 #T2 #_ #IHT12 #L #d #e #HLK #U1 #H #U2 #HTU2
+  elim (lift_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct /3 width=5/
+] 
+qed.
+
+lemma cpqs_inv_lift1: l_deliftable_sn cpqs.
+#L #U1 #U2 #H elim H -L -U1 -U2
+[ * #L #i #K #d #e #_ #T1 #H
+  [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3/
+  | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3/
+  | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3/
+  ]
+| #L #LV #V #V2 #W2 #i #HLV #HV2 #HVW2 #IHV2 #K #d #e #HLK #T1 #H
+  elim (lift_inv_lref2 … H) -H * #Hid #H destruct
+  [ elim (ldrop_conf_lt … HLK … HLV) -L // #L #U #HKL #HLV #HUV
+    elim (IHV2 … HLV … HUV) -V #U2 #HUV2 #HU2
+    elim (lift_trans_le … HUV2 … HVW2) -V2 // >minus_plus <plus_minus_m_m // -Hid /3 width=8/
+  | elim (le_inv_plus_l … Hid) #Hdie #Hei
+    lapply (ldrop_conf_ge … HLK … HLV ?) -L // #HKLV
+    elim (lift_split … HVW2 d (i - e + 1)) -HVW2 [4: // |3: /2 width=1/ |2: /3 width=1/ ] -Hid -Hdie
+    #V1 #HV1 >plus_minus // <minus_minus // /2 width=1/ <minus_n_n <plus_n_O /3 width=8/
+  ]
+| #a #I #L #V1 #V2 #U1 #U2 #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H
+  elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
+  elim (IHV12 … HLK … HWV1) -IHV12 #W2 #HW12 #HWV2
+  elim (IHU12 … HTU1) -IHU12 -HTU1 /3 width=5/
+| #I #L #V1 #V2 #U1 #U2 #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H
+  elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
+  elim (IHV12 … HLK … HWV1) -V1
+  elim (IHU12 … HLK … HTU1) -U1 -HLK /3 width=5/
+| #L #V #U1 #U #U2 #_ #HU2 #IHU1 #K #d #e #HLK #X #H
+  elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
+  elim (IHU1 (K.ⓓW1) … HTU1) /2 width=1/ -L -U1 #T #HTU #HT1
+  elim (lift_div_le … HU2 … HTU) -U // /3 width=5/
+| #L #V #U1 #U2 #_ #IHU12 #K #d #e #HLK #X #H
+  elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
+  elim (IHU12 … HLK … HTU1) -L -U1 /3 width=3/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lpqs.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lpqs.ma
new file mode 100644
index 000000000..b3f6ee4d0
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/lpqs.ma
@@ -0,0 +1,67 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/substitution/lpss.ma".
+include "basic_2/unfold/cpqs.ma".
+
+(* SN RESTRICTED PARALLEL COMPUTATION FOR LOCAL ENVIRONMENTS ****************)
+
+definition lpqs: relation lenv ≝ lpx_sn cpqs. 
+
+interpretation "restricted parallel computation (local environment, sn variant)"
+   'PRestStarSn L1 L2 = (lpqs L1 L2).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma lpqs_inv_atom1: ∀L2. ⋆ ⊢ ➤* L2 → L2 = ⋆.
+/2 width=4 by lpx_sn_inv_atom1_aux/ qed-.
+
+lemma lpqs_inv_pair1: ∀I,K1,V1,L2. K1. ⓑ{I} V1 ⊢ ➤* L2 →
+                      ∃∃K2,V2. K1 ⊢ ➤* K2 & K1 ⊢ V1 ➤* V2 & L2 = K2. ⓑ{I} V2.
+/2 width=3 by lpx_sn_inv_pair1_aux/ qed-.
+
+lemma lpqs_inv_atom2: ∀L1. L1 ⊢ ➤* ⋆ → L1 = ⋆.
+/2 width=4 by lpx_sn_inv_atom2_aux/ qed-.
+
+lemma lpqs_inv_pair2: ∀I,L1,K2,V2. L1 ⊢ ➤* K2. ⓑ{I} V2 →
+                      ∃∃K1,V1. K1 ⊢ ➤* K2 & K1 ⊢ V1 ➤* V2 & L1 = K1. ⓑ{I} V1.
+/2 width=3 by lpx_sn_inv_pair2_aux/ qed-.
+
+(* Basic properties *********************************************************)
+
+lemma lpqs_refl: ∀L. L ⊢ ➤* L.
+/2 width=1 by lpx_sn_refl/ qed.
+
+lemma lpqs_append: ∀K1,K2. K1 ⊢ ➤* K2 → ∀L1,L2. L1 ⊢ ➤* L2 →
+                   L1 @@ K1 ⊢ ➤* L2 @@ K2.
+/3 width=1 by lpx_sn_append, cpqs_append/ qed.
+
+lemma lpss_lpqs: ∀L1,L2. L1 ⊢ ▶* L2 → L1 ⊢ ➤* L2.
+#L1 #L2 #H elim H -L1 -L2 // /3 width=1/
+qed.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lpqs_fwd_length: ∀L1,L2. L1 ⊢ ➤* L2 → |L1| = |L2|.
+/2 width=2 by lpx_sn_fwd_length/ qed-.
+
+(* Advanced forward lemmas **************************************************)
+
+lemma lpqs_fwd_append1: ∀K1,L1,L. K1 @@ L1 ⊢ ➤* L →
+                        ∃∃K2,L2. K1 ⊢ ➤* K2 & L = K2 @@ L2.
+/2 width=2 by lpx_sn_fwd_append1/ qed-.
+
+lemma lpqs_fwd_append2: ∀L,K2,L2. L ⊢ ➤* K2 @@ L2 →
+                        ∃∃K1,L1. K1 ⊢ ➤* K2 & L = K1 @@ L1.
+/2 width=2 by lpx_sn_fwd_append2/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lpqs_cpqs.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lpqs_cpqs.ma
new file mode 100644
index 000000000..47d3b7cdf
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/lpqs_cpqs.ma
@@ -0,0 +1,297 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/relocation/fsup.ma".
+include "basic_2/unfold/lpqs_ldrop.ma".
+
+(* SN RESTRICTED PARALLEL COMPUTATION FOR LOCAL ENVIRONMENTS ****************)
+
+(* Main properties on context-sensitive rest parallel computation for terms *)
+
+fact cpqs_conf_lpqs_atom_atom:
+   ∀I,L1,L2. ∃∃T. L1 ⊢ ⓪{I} ➤* T & L2 ⊢ ⓪{I} ➤* T.
+/2 width=3/ qed-.
+
+fact cpqs_conf_lpqs_atom_delta:
+   ∀L0,i. (
+      ∀L,T.♯{L, T} < ♯{L0, #i} →
+      ∀T1. L ⊢ T ➤* T1 → ∀T2. L ⊢ T ➤* T2 →
+      ∀L1. L ⊢ ➤* L1 → ∀L2. L ⊢ ➤* L2 →
+      ∃∃T0. L1 ⊢ T1 ➤* T0 & L2 ⊢ T2 ➤* T0
+   ) →
+   ∀K0,V0. ⇩[O, i] L0 ≡ K0.ⓓV0 →
+   ∀V2. K0 ⊢ V0 ➤* V2 → ∀T2. ⇧[O, i + 1] V2 ≡ T2 →
+   ∀L1. L0 ⊢ ➤* L1 → ∀L2. L0 ⊢ ➤* L2 →
+   ∃∃T. L1 ⊢ #i ➤* T & L2 ⊢ T2 ➤* T.
+#L0 #i #IH #K0 #V0 #HLK0 #V2 #HV02 #T2 #HVT2 #L1 #HL01 #L2 #HL02
+elim (lpqs_ldrop_conf … HLK0 … HL01) -HL01 #X1 #H1 #HLK1
+elim (lpqs_inv_pair1 … H1) -H1 #K1 #V1 #HK01 #HV01 #H destruct
+elim (lpqs_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2
+elim (lpqs_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct
+lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2
+lapply (ldrop_pair2_fwd_fw … HLK0 (#i)) -HLK0 #HLK0
+elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2
+elim (lift_total V 0 (i+1)) #T #HVT
+lapply (cpqs_lift … HV2 … HLK2 … HVT2 … HVT) -K2 -V2 /3 width=6/
+qed-.
+
+fact cpqs_conf_lpqs_delta_delta:
+   ∀L0,i. (
+      ∀L,T.♯{L, T} < ♯{L0, #i} →
+      ∀T1. L ⊢ T ➤* T1 → ∀T2. L ⊢ T ➤* T2 →
+      ∀L1. L ⊢ ➤* L1 → ∀L2. L ⊢ ➤* L2 →
+      ∃∃T0. L1 ⊢ T1 ➤* T0 & L2 ⊢ T2 ➤* T0
+   ) →
+   ∀K0,V0. ⇩[O, i] L0 ≡ K0.ⓓV0 →
+   ∀V1. K0 ⊢ V0 ➤* V1 → ∀T1. ⇧[O, i + 1] V1 ≡ T1 →
+   ∀KX,VX. ⇩[O, i] L0 ≡ KX.ⓓVX →
+   ∀V2. KX ⊢ VX ➤* V2 → ∀T2. ⇧[O, i + 1] V2 ≡ T2 →
+   ∀L1. L0 ⊢ ➤* L1 → ∀L2. L0 ⊢ ➤* L2 →
+   ∃∃T. L1 ⊢ T1 ➤* T & L2 ⊢ T2 ➤* T.
+#L0 #i #IH #K0 #V0 #HLK0 #V1 #HV01 #T1 #HVT1
+#KX #VX #H #V2 #HV02 #T2 #HVT2 #L1 #HL01 #L2 #HL02
+lapply (ldrop_mono … H … HLK0) -H #H destruct
+elim (lpqs_ldrop_conf … HLK0 … HL01) -HL01 #X1 #H1 #HLK1
+elim (lpqs_inv_pair1 … H1) -H1 #K1 #W1 #HK01 #_ #H destruct
+lapply (ldrop_fwd_ldrop2 … HLK1) -W1 #HLK1
+elim (lpqs_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2
+elim (lpqs_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct
+lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2
+lapply (ldrop_pair2_fwd_fw … HLK0 (#i)) -HLK0 #HLK0
+elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2
+elim (lift_total V 0 (i+1)) #T #HVT
+lapply (cpqs_lift … HV1 … HLK1 … HVT1 … HVT) -K1 -V1
+lapply (cpqs_lift … HV2 … HLK2 … HVT2 … HVT) -K2 -V2 -V /2 width=3/
+qed-.
+
+fact cpqs_conf_lpqs_bind_bind:
+   ∀a,I,L0,V0,T0. (
+      ∀L,T.♯{L,T} < ♯{L0,ⓑ{a,I}V0.T0} →
+      ∀T1. L ⊢ T ➤* T1 → ∀T2. L ⊢ T ➤* T2 →
+      ∀L1. L ⊢ ➤* L1 → ∀L2. L ⊢ ➤* L2 →
+      ∃∃T0. L1 ⊢ T1 ➤* T0 & L2 ⊢ T2 ➤* T0
+   ) →
+   ∀V1. L0 ⊢ V0 ➤* V1 → ∀T1. L0.ⓑ{I}V0 ⊢ T0 ➤* T1 →
+   ∀V2. L0 ⊢ V0 ➤* V2 → ∀T2. L0.ⓑ{I}V0 ⊢ T0 ➤* T2 →
+   ∀L1. L0 ⊢ ➤* L1 → ∀L2. L0 ⊢ ➤* L2 →
+   ∃∃T. L1 ⊢ ⓑ{a,I}V1.T1 ➤* T & L2 ⊢ ⓑ{a,I}V2.T2 ➤* T.
+#a #I #L0 #V0 #T0 #IH #V1 #HV01 #T1 #HT01
+#V2 #HV02 #T2 #HT02 #L1 #HL01 #L2 #HL02
+elim (IH … HV01 … HV02 … HL01 … HL02) //
+elim (IH … HT01 … HT02 (L1.ⓑ{I}V1) … (L2.ⓑ{I}V2)) -IH // /2 width=1/ /3 width=5/
+qed-.
+
+fact cpqs_conf_lpqs_bind_zeta:
+   ∀L0,V0,T0. (
+      ∀L,T.♯{L,T} < ♯{L0,+ⓓV0.T0} →
+      ∀T1. L ⊢ T ➤* T1 → ∀T2. L ⊢ T ➤* T2 →
+      ∀L1. L ⊢ ➤* L1 → ∀L2. L ⊢ ➤* L2 →
+      ∃∃T0. L1 ⊢ T1 ➤* T0 & L2 ⊢ T2 ➤* T0
+   ) →
+   ∀V1. L0 ⊢ V0 ➤* V1 → ∀T1. L0.ⓓV0 ⊢ T0 ➤* T1 →
+   ∀T2. L0.ⓓV0 ⊢ T0 ➤* T2 → ∀X2. ⇧[O, 1] X2 ≡ T2 →
+   ∀L1. L0 ⊢ ➤* L1 → ∀L2. L0 ⊢ ➤* L2 →
+   ∃∃T. L1 ⊢ +ⓓV1.T1 ➤* T & L2 ⊢ X2 ➤* T.
+#L0 #V0 #T0 #IH #V1 #HV01 #T1 #HT01
+#T2 #HT02 #X2 #HXT2 #L1 #HL01 #L2 #HL02
+elim (IH … HT01 … HT02 (L1.ⓓV1) … (L2.ⓓV1)) -IH -HT01 -HT02 // /2 width=1/ -L0 -V0 -T0 #T #HT1 #HT2
+elim (cpqs_inv_lift1 … HT2 L2 … HXT2) -T2 /2 width=1/ /3 width=3/
+qed-.
+
+fact cpqs_conf_lpqs_zeta_zeta:
+   ∀L0,V0,T0. (
+      ∀L,T.♯{L,T} < ♯{L0,+ⓓV0.T0} →
+      ∀T1. L ⊢ T ➤* T1 → ∀T2. L ⊢ T ➤* T2 →
+      ∀L1. L ⊢ ➤* L1 → ∀L2. L ⊢ ➤* L2 →
+      ∃∃T0. L1 ⊢ T1 ➤* T0 & L2 ⊢ T2 ➤* T0
+   ) →
+   ∀T1. L0.ⓓV0 ⊢ T0 ➤* T1 → ∀X1. ⇧[O, 1] X1 ≡ T1 →
+   ∀T2. L0.ⓓV0 ⊢ T0 ➤* T2 → ∀X2. ⇧[O, 1] X2 ≡ T2 →
+   ∀L1. L0 ⊢ ➤* L1 → ∀L2. L0 ⊢ ➤* L2 →
+   ∃∃T. L1 ⊢ X1 ➤* T & L2 ⊢ X2 ➤* T.
+#L0 #V0 #T0 #IH #T1 #HT01 #X1 #HXT1
+#T2 #HT02 #X2 #HXT2 #L1 #HL01 #L2 #HL02
+elim (IH … HT01 … HT02 (L1.ⓓV0) … (L2.ⓓV0)) -IH -HT01 -HT02 // /2 width=1/ -L0 -T0 #T #HT1 #HT2
+elim (cpqs_inv_lift1 … HT1 L1 … HXT1) -T1 /2 width=1/ #T1 #HT1 #HXT1
+elim (cpqs_inv_lift1 … HT2 L2 … HXT2) -T2 /2 width=1/ #T2 #HT2 #HXT2 
+lapply (lift_inj … HT2 … HT1) -T #H destruct /2 width=3/
+qed-.
+
+fact cpqs_conf_lpqs_flat_flat:
+   ∀I,L0,V0,T0. (
+      ∀L,T.♯{L,T} < ♯{L0,ⓕ{I}V0.T0} →
+      ∀T1. L ⊢ T ➤* T1 → ∀T2. L ⊢ T ➤* T2 →
+      ∀L1. L ⊢ ➤* L1 → ∀L2. L ⊢ ➤* L2 →
+      ∃∃T0. L1 ⊢ T1 ➤* T0 & L2 ⊢ T2 ➤* T0
+   ) →
+   ∀V1. L0 ⊢ V0 ➤* V1 → ∀T1. L0 ⊢ T0 ➤* T1 →
+   ∀V2. L0 ⊢ V0 ➤* V2 → ∀T2. L0 ⊢ T0 ➤* T2 →
+   ∀L1. L0 ⊢ ➤* L1 → ∀L2. L0 ⊢ ➤* L2 →
+   ∃∃T. L1 ⊢ ⓕ{I}V1.T1 ➤* T & L2 ⊢ ⓕ{I}V2.T2 ➤* T.
+#I #L0 #V0 #T0 #IH #V1 #HV01 #T1 #HT01
+#V2 #HV02 #T2 #HT02 #L1 #HL01 #L2 #HL02
+elim (IH … HV01 … HV02 … HL01 … HL02) //
+elim (IH … HT01 … HT02 … HL01 … HL02) // /3 width=5/
+qed-.
+
+fact cpqs_conf_lpqs_flat_tau:
+   ∀L0,V0,T0. (
+      ∀L,T.♯{L,T} < ♯{L0,ⓝV0.T0} →
+      ∀T1. L ⊢ T ➤* T1 → ∀T2. L ⊢ T ➤* T2 →
+      ∀L1. L ⊢ ➤* L1 → ∀L2. L ⊢ ➤* L2 →
+      ∃∃T0. L1 ⊢ T1 ➤* T0 & L2 ⊢ T2 ➤* T0
+   ) →
+   ∀V1,T1. L0 ⊢ T0 ➤* T1 → ∀T2. L0 ⊢ T0 ➤* T2 →
+   ∀L1. L0 ⊢ ➤* L1 → ∀L2. L0 ⊢ ➤* L2 →
+   ∃∃T. L1 ⊢ ⓝV1.T1 ➤* T & L2 ⊢ T2 ➤* T.
+#L0 #V0 #T0 #IH #V1 #T1 #HT01
+#T2 #HT02 #L1 #HL01 #L2 #HL02
+elim (IH … HT01 … HT02 … HL01 … HL02) // -L0 -V0 -T0 /3 width=3/
+qed-.
+
+fact cpqs_conf_lpqs_tau_tau:
+   ∀L0,V0,T0. (
+      ∀L,T.♯{L,T} < ♯{L0,ⓝV0.T0} →
+      ∀T1. L ⊢ T ➤* T1 → ∀T2. L ⊢ T ➤* T2 →
+      ∀L1. L ⊢ ➤* L1 → ∀L2. L ⊢ ➤* L2 →
+      ∃∃T0. L1 ⊢ T1 ➤* T0 & L2 ⊢ T2 ➤* T0
+   ) →
+   ∀T1. L0 ⊢ T0 ➤* T1 → ∀T2. L0 ⊢ T0 ➤* T2 →
+   ∀L1. L0 ⊢ ➤* L1 → ∀L2. L0 ⊢ ➤* L2 →
+   ∃∃T. L1 ⊢ T1 ➤* T & L2 ⊢ T2 ➤* T.
+#L0 #V0 #T0 #IH #T1 #HT01
+#T2 #HT02 #L1 #HL01 #L2 #HL02
+elim (IH … HT01 … HT02 … HL01 … HL02) // -L0 -V0 -T0 /2 width=3/
+qed-.
+
+theorem cpqs_conf_lpqs: lpx_sn_confluent cpqs cpqs.
+#L0 #T0 @(f2_ind … fw … L0 T0) -L0 -T0 #n #IH #L0 * [|*]
+[ #I0 #Hn #T1 #H1 #T2 #H2 #L1 #HL01 #L2 #HL02 destruct
+  elim (cpqs_inv_atom1 … H1) -H1
+  elim (cpqs_inv_atom1 … H2) -H2
+  [ #H2 #H1 destruct
+    /2 width=1 by cpqs_conf_lpqs_atom_atom/
+  | * #K0 #V0 #V2 #i2 #HLK0 #HV02 #HVT2 #H2 #H1 destruct
+    /3 width=10 by cpqs_conf_lpqs_atom_delta/
+  | #H2 * #K0 #V0 #V1 #i1 #HLK0 #HV01 #HVT1 #H1 destruct
+    /4 width=10 by ex2_commute, cpqs_conf_lpqs_atom_delta/
+  | * #X #Y #V2 #z #H #HV02 #HVT2 #H2
+    * #K0 #V0 #V1 #i #HLK0 #HV01 #HVT1 #H1 destruct
+    /3 width=17 by cpqs_conf_lpqs_delta_delta/
+  ]
+| #a #I #V0 #T0 #Hn #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct
+  elim (cpqs_inv_bind1 … H1) -H1 *
+  [ #V1 #T1 #HV01 #HT01 #H1
+  | #T1 #HT01 #HXT1 #H11 #H12
+  ]
+  elim (cpqs_inv_bind1 … H2) -H2 *
+  [1,3: #V2 #T2 #HV02 #HT02 #H2
+  |2,4: #T2 #HT02 #HXT2 #H21 #H22
+  ] destruct
+  [ /3 width=10 by cpqs_conf_lpqs_bind_bind/
+  | /4 width=11 by ex2_commute, cpqs_conf_lpqs_bind_zeta/
+  | /3 width=11 by cpqs_conf_lpqs_bind_zeta/
+  | /3 width=12 by cpqs_conf_lpqs_zeta_zeta/
+  ]
+| #I #V0 #T0 #Hn #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct
+  elim (cpqs_inv_flat1 … H1) -H1 *
+  [ #V1 #T1 #HV01 #HT01 #H1
+  | #HX1 #H1
+  ]
+  elim (cpqs_inv_flat1 … H2) -H2 *
+  [1,3: #V2 #T2 #HV02 #HT02 #H2
+  |2,4: #HX2 #H2
+  ] destruct
+  [ /3 width=10 by cpqs_conf_lpqs_flat_flat/
+  | /4 width=8 by ex2_commute, cpqs_conf_lpqs_flat_tau/
+  | /3 width=8 by cpqs_conf_lpqs_flat_tau/
+  | /3 width=7 by cpqs_conf_lpqs_tau_tau/
+  ]
+]
+qed-.
+
+theorem cpqs_conf: ∀L. confluent … (cpqs L).
+/2 width=6 by cpqs_conf_lpqs/ qed-.
+
+theorem cpqs_trans_lpqs: lpx_sn_transitive cpqs cpqs.
+#L1 #T1 @(f2_ind … fw … L1 T1) -L1 -T1 #n #IH #L1 * [|*]
+[ #I #Hn #T #H1 #L2 #HL12 #T2 #HT2 destruct
+  elim (cpqs_inv_atom1 … H1) -H1
+  [ #H destruct
+    elim (cpqs_inv_atom1 … HT2) -HT2
+    [ #H destruct //
+    | * #K2 #V #V2 #i #HLK2 #HV2 #HVT2 #H destruct
+      elim (lpqs_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H
+      elim (lpqs_inv_pair2 … H) -H #K1 #V1 #HK12 #HV1 #H destruct
+      lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) /3 width=9/
+    ]
+  | * #K1 #V1 #V #i #HLK1 #HV1 #HVT #H destruct
+    elim (lpqs_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2
+    elim (lpqs_inv_pair1 … H) -H #K2 #W2 #HK12 #_ #H destruct
+    lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2
+    elim (cpqs_inv_lift1 … HT2 … HLK2 … HVT) -L2 -T
+    lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) /3 width=9/
+  ]
+| #a #I #V1 #T1 #Hn #X1 #H1 #L2 #HL12 #X2 #H2
+  elim (cpqs_inv_bind1 … H1) -H1 *
+  [ #V #T #HV1 #HT1 #H destruct
+    elim (cpqs_inv_bind1 … H2) -H2 *
+    [ #V2 #T2 #HV2 #HT2 #H destruct /4 width=5/
+    | #T2 #HT2 #HXT2 #H1 #H2 destruct /4 width=5/
+    ]
+  | #Y1 #HTY1 #HXY1 #H11 #H12 destruct
+    elim (lift_total X2 0 1) #Y2 #HXY2
+    lapply (cpqs_lift … H2 (L2.ⓓV1) … HXY1 … HXY2) /2 width=1/ -X1 /4 width=5/
+  ]
+| #I #V1 #T1 #Hn #X1 #H1 #L2 #HL12 #X2 #H2
+  elim (cpqs_inv_flat1 … H1) -H1 *
+  [ #V #T #HV1 #HT1 #H destruct
+    elim (cpqs_inv_flat1 … H2) -H2 *
+    [ #V2 #T2 #HV2 #HT2 #H destruct /3 width=5/
+    | #HX2 #H destruct /3 width=5/
+    ]
+  | #HX1 #H destruct /3 width=5/
+]
+qed-.
+
+theorem cpqs_trans: ∀L. Transitive … (cpqs L).
+/2 width=5 by cpqs_trans_lpqs/ qed-.
+
+(* Properties on context-sensitive rest. parallel computation for terms *****)
+
+lemma lpqs_cpqs_conf_dx: ∀L0,T0,T1. L0 ⊢ T0 ➤* T1 → ∀L1. L0 ⊢ ➤* L1 →
+                         ∃∃T. L1 ⊢ T0 ➤* T & L1 ⊢ T1 ➤* T.
+#L0 #T0 #T1 #HT01 #L1 #HL01
+elim (cpqs_conf_lpqs … HT01 T0 … HL01 … HL01) // -L0 /2 width=3/
+qed-.
+
+lemma lpqs_cpqs_conf_sn: ∀L0,T0,T1. L0 ⊢ T0 ➤* T1 → ∀L1. L0 ⊢ ➤* L1 →
+                         ∃∃T. L1 ⊢ T0 ➤* T & L0 ⊢ T1 ➤* T.
+#L0 #T0 #T1 #HT01 #L1 #HL01
+elim (cpqs_conf_lpqs … HT01 T0 … L0 … HL01) // -HT01 -HL01 /2 width=3/
+qed-.
+
+lemma lpqs_cpqs_trans: ∀L1,L2. L1 ⊢ ➤* L2 →
+                       ∀T1,T2. L2 ⊢ T1 ➤* T2 → L1 ⊢ T1 ➤* T2.
+/2 width=5 by cpqs_trans_lpqs/ qed-.
+
+lemma fsup_cpqs_trans: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ∀U2. L2 ⊢ T2 ➤* U2 →
+                       ∃∃L,U1. L1 ⊢ ➤* L & L ⊢ T1 ➤* U1 & ⦃L, U1⦄ ⊃ ⦃L2, U2⦄.
+#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 [1,2,3,4,5: /3 width=5/ ]
+#L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #U2 #HTU2
+elim (IHT12 … HTU2) -IHT12 -HTU2 #K #T #HK1 #HT1 #HT2
+elim (lift_total T d e) #U #HTU
+elim (ldrop_lpqs_trans … HLK1 … HK1) -HLK1 -HK1 #L2 #HL12 #HL2K
+lapply (cpqs_lift … HT1 … HL2K … HTU1 … HTU) -HT1 -HTU1 /3 width=11/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lpqs_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lpqs_ldrop.ma
new file mode 100644
index 000000000..bea4a9134
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/lpqs_ldrop.ma
@@ -0,0 +1,30 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/relocation/ldrop_lpx_sn.ma".
+include "basic_2/unfold/cpqs_lift.ma".
+include "basic_2/unfold/lpqs.ma".
+
+(* SN RESTRICTED PARALLEL COMPUTATION FOR LOCAL ENVIRONMENTS ****************)
+
+(* Properies on local environment slicing ***********************************)
+
+lemma lpqs_ldrop_conf: dropable_sn lpqs.
+/3 width=5 by lpx_sn_deliftable_dropable, cpqs_inv_lift1/ qed-.
+
+lemma ldrop_lpqs_trans: dedropable_sn lpqs.
+/3 width=9 by lpx_sn_liftable_dedropable, cpqs_lift/ qed-.
+
+lemma lpqs_ldrop_trans_O1: dropable_dx lpqs.
+/2 width=3 by lpx_sn_dropable/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lpqs_lpqs.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lpqs_lpqs.ma
new file mode 100644
index 000000000..c134c8880
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/lpqs_lpqs.ma
@@ -0,0 +1,46 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/unfold/lpqs_cpqs.ma".
+
+(* SN RESTRICTED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *****************)
+
+(* Main properties **********************************************************)
+
+theorem lpqs_conf: confluent … lpqs.
+/3 width=6 by lpx_sn_conf, cpqs_conf_lpqs/
+qed-.
+
+theorem lpqs_trans: Transitive … lpqs.
+/3 width=5 by lpx_sn_trans, cpqs_trans_lpqs/
+qed-.
+
+(* Advanced forward lemmas **************************************************)
+
+lemma cpqs_fwd_shift1: ∀L1,L,T1,T. L ⊢ L1 @@ T1 ➤* T →
+                       ∃∃L2,T2. L @@ L1 ⊢ ➤* L @@ L2 & L @@ L1 ⊢ T1 ➤* T2 &
+                                T = L2 @@ T2.
+#L1 @(lenv_ind_dx … L1) -L1
+[ #L #T1 #T #HT1
+  @ex3_2_intro [3: // |4,5: // |1,2: skip ] (**) (* /2 width=4/ does not work *)
+| #I #L1 #V1 #IH #L #T1 #T >shift_append_assoc #H <append_assoc
+  elim (cpqs_inv_bind1 … H) -H *
+  [ #V2 #T2 #HV12 #HT12 #H destruct
+    elim (IH … HT12) -IH -HT12 #L2 #T #HL12 #HT1 #H destruct
+    lapply (lpqs_trans … HL12 (L.ⓑ{I}V2@@L2) ?) -HL12 /3 width=1/ #HL12
+    @(ex3_2_intro … (⋆.ⓑ{I}V2@@L2)) [4: /2 width=3/ | skip ] <append_assoc // (**) (* explicit constructor *)
+  | #T #_ #_ #H destruct
+  ]
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/sstas.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/sstas.ma
new file mode 100644
index 000000000..5ff1bae0f
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/sstas.ma
@@ -0,0 +1,80 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/static/ssta.ma".
+
+(* ITERATED STRATIFIED STATIC TYPE ASSIGNMENT FOR TERMS *********************)
+
+(* Note: includes: stass_refl *)
+definition sstas: ∀h. sd h → lenv → relation term ≝
+                  λh,g,L. star … (ssta_step h g L).
+
+interpretation "iterated stratified static type assignment (term)"
+   'StaticTypeStar h g L T U = (sstas h g L T U).
+
+(* Basic eliminators ********************************************************)
+
+lemma sstas_ind: ∀h,g,L,T. ∀R:predicate term.
+                 R T → (
+                    ∀U1,U2,l. ⦃h, L⦄ ⊢ T •* [g] U1 →  ⦃h, L⦄ ⊢ U1 •[g] ⦃l+1, U2⦄ →
+                    R U1 → R U2
+                 ) →
+                 ∀U. ⦃h, L⦄ ⊢ T •*[g] U → R U.
+#h #g #L #T #R #IH1 #IH2 #U #H elim H -U //
+#U1 #U2 #H * /2 width=5/
+qed-.
+
+lemma sstas_ind_dx: ∀h,g,L,U2. ∀R:predicate term.
+                    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.
+#h #g #L #U2 #R #IH1 #IH2 #T #H @(star_ind_l … T H) -T //
+#T #T0 * /2 width=5/
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma sstas_refl: ∀h,g,L. reflexive … (sstas h g L).
+// qed.
+
+lemma ssta_sstas: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g] ⦃l+1, U⦄ → ⦃h, L⦄ ⊢ T •*[g] U.
+/3 width=2 by R_to_star, ex_intro/ qed. (**) (* auto fails without trace *)
+
+lemma sstas_strap1: ∀h,g,L,T1,T2,U2,l. ⦃h, L⦄ ⊢ T1 •*[g] T2 → ⦃h, L⦄ ⊢ T2 •[g] ⦃l+1, U2⦄ →
+                    ⦃h, L⦄ ⊢ T1 •*[g] U2.
+/3 width=4 by sstep, ex_intro/ (**) (* auto fails without trace *)
+qed.
+
+lemma sstas_strap2: ∀h,g,L,T1,U1,U2,l. ⦃h, L⦄ ⊢ T1 •[g] ⦃l+1, U1⦄ → ⦃h, L⦄ ⊢ U1 •*[g] U2 →
+                    ⦃h, L⦄ ⊢ T1 •*[g] U2.
+/3 width=3 by star_compl, ex_intro/ (**) (* auto fails without trace *)
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma sstas_inv_bind1: ∀h,g,a,I,L,Y,X,U. ⦃h, L⦄ ⊢ ⓑ{a,I}Y.X •*[g] U →
+                       ∃∃Z. ⦃h, L.ⓑ{I}Y⦄ ⊢ X •*[g] Z & U = ⓑ{a,I}Y.Z.
+#h #g #a #I #L #Y #X #U #H @(sstas_ind … H) -U /2 width=3/
+#T #U #l #_ #HTU * #Z #HXZ #H destruct
+elim (ssta_inv_bind1 … HTU) -HTU #Z0 #HZ0 #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.
+#h #g #L #Y #X #U #H @(sstas_ind … H) -U /2 width=3/
+#T #U #l #_ #HTU * #Z #HXZ #H destruct
+elim (ssta_inv_appl1 … HTU) -HTU #Z0 #HZ0 #H destruct /3 width=4/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/sstas_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/sstas_aaa.ma
new file mode 100644
index 000000000..36951ce08
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/sstas_aaa.ma
@@ -0,0 +1,25 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/static/ssta_aaa.ma".
+include "basic_2/unfold/sstas.ma".
+
+(* ITERATED STRATIFIED STATIC TYPE ASSIGNMENT FOR TERMS *********************)
+
+(* Properties on atomic arity assignment for terms **************************)
+
+lemma sstas_aaa: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U →
+                 ∀A. L ⊢ T ⁝ A → L ⊢ U ⁝ A.
+#h #g #L #T #U #H @(sstas_ind_dx … H) -T // /3 width=6/
+qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/sstas_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/sstas_lift.ma
new file mode 100644
index 000000000..f90629ebe
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/sstas_lift.ma
@@ -0,0 +1,52 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/static/ssta_lift.ma".
+include "basic_2/unfold/sstas.ma".
+
+(* ITERATED STRATIFIED STATIC TYPE ASSIGNMENT FOR TERMS *********************)
+
+(* Advanced forward lemmas **************************************************)
+
+lemma sstas_fwd_correct: ∀h,g,L,T1,U1,l1. ⦃h, L⦄ ⊢ T1 •[g] ⦃l1, U1⦄ →
+                         ∀T2. ⦃h, L⦄ ⊢ T1 •*[g] T2 →
+                         ∃∃U2,l2. ⦃h, L⦄ ⊢ T2 •[g] ⦃l2, U2⦄.
+#h #g #L #T1 #U1 #l1 #HTU1 #T2 #H @(sstas_ind … H) -T2 [ /2 width=3/ ] -HTU1
+#T #T2 #l #_ #HT2 * #U #l0 #_ -l0
+elim (ssta_fwd_correct … HT2) -T /2 width=3/
+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_dx … H) -T1
+[ #L2 #d #e #HL21 #X #HX #U2 #HU12
+  >(lift_mono … HX … HU12) -X //
+| #T0 #U0 #l0 #HTU0 #_ #IHU01 #L2 #d #e #HL21 #T2 #HT02 #U2 #HU12
+  elim (lift_total U0 d e) /3 width=10/
+]
+qed.
+
+(* Inversion lemmas on relocation *******************************************)
+
+lemma sstas_inv_lift1: ∀h,g,L2,T2,U2. ⦃h, L2⦄ ⊢ T2 •*[g] U2 →
+                       ∀L1,d,e. ⇩[d, e] L2 ≡ L1 → ∀T1. ⇧[d, e] T1 ≡ T2 →
+                       ∃∃U1. ⦃h, L1⦄ ⊢ T1 •*[g] U1 & ⇧[d, e] U1 ≡ U2.
+#h #g #L2 #T2 #U2 #H @(sstas_ind_dx … H) -T2 /2 width=3/
+#T0 #U0 #l0 #HTU0 #_ #IHU01 #L1 #d #e #HL21 #U1 #HU12
+elim (ssta_inv_lift1 … HTU0 … HL21 … HU12) -HTU0 -HU12 #U #HU1 #HU0
+elim (IHU01 … HL21 … HU0) -IHU01 -HL21 -U0 /3 width=4/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/sstas_lpss.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/sstas_lpss.ma
new file mode 100644
index 000000000..8f9eda109
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/sstas_lpss.ma
@@ -0,0 +1,39 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/static/ssta_lpss.ma".
+include "basic_2/unfold/sstas.ma".
+
+(* ITERATED STRATIFIED STATIC TYPE ASSIGNMENT FOR TERMS *********************)
+
+(* Properties about sn parallel substitution ********************************)
+
+lemma sstas_tpss_lpss_conf: ∀h,g,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 •*[g] U1 →
+                            ∀T2. L1 ⊢ T1 ▶* T2 → ∀L2. L1 ⊢ ▶* L2 →
+                            ∃∃U2. ⦃h, L2⦄ ⊢ T2 •*[g] U2 & L1 ⊢ U1 ▶* U2.
+#h #g #L1 #T1 #U1 #H @(sstas_ind_dx … H) -T1 /2 width=3/
+#T0 #U0 #l0 #HTU0 #_ #IHU01 #T #HT0 #L2 #HL12
+elim (ssta_tpss_lpss_conf … HTU0 … HT0 … HL12) -HTU0 -HT0 #U #HTU #HU0
+elim (IHU01 … HU0 … HL12) -IHU01 -U0 -HL12 /3 width=4/
+qed-.
+
+lemma sstas_tpss_conf: ∀h,g,L,T1,U1. ⦃h, L⦄ ⊢ T1 •*[g] U1 →
+                       ∀T2. L ⊢ T1 ▶* T2 →
+                       ∃∃U2. ⦃h, L⦄ ⊢ T2 •*[g] U2 & L ⊢ U1 ▶* U2.
+/2 width=3 by sstas_tpss_lpss_conf/ qed-.
+
+lemma sstas_lpss_conf: ∀h,g,L1,T,U1. ⦃h, L1⦄ ⊢ T •*[g] U1 →
+                       ∀L2. L1 ⊢ ▶* L2 →
+                       ∃∃U2. ⦃h, L2⦄ ⊢ T •*[g] U2 & L1 ⊢ U1 ▶* U2.
+/2 width=3 by sstas_tpss_lpss_conf/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/sstas_sstas.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/sstas_sstas.ma
new file mode 100644
index 000000000..0b0dcca42
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/sstas_sstas.ma
@@ -0,0 +1,54 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/static/ssta_ssta.ma".
+include "basic_2/unfold/sstas.ma".
+
+(* ITERATED STRATIFIED STATIC TYPE ASSIGNMENT FOR TERMS *********************)
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma sstas_inv_O: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U →
+                   ∀T0. ⦃h, L⦄ ⊢ T •[g] ⦃0, T0⦄ → U = T.
+#h #g #L #T #U #H @(sstas_ind_dx … H) -T //
+#T0 #U0 #l0 #HTU0 #_ #_ #T1 #HT01
+elim (ssta_mono … HTU0 … HT01) <plus_n_Sm #H destruct
+qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma sstas_strip: ∀h,g,L,T,U1. ⦃h, L⦄ ⊢ T •*[g] U1 →
+                   ∀U2,l. ⦃h, L⦄ ⊢ T •[g] ⦃l, U2⦄ →
+                   T = U1 ∨ ⦃h, L⦄ ⊢ U2 •*[g] U1.
+#h #g #L #T #U1 #H1 @(sstas_ind_dx … H1) -T /2 width=1/
+#T #U #l0 #HTU #HU1 #_ #U2 #l #H2
+elim (ssta_mono … H2 … HTU) -H2 -HTU #H1 #H2 destruct /2 width=1/
+qed-.
+
+(* Main properties **********************************************************)
+
+theorem sstas_trans: ∀h,g,L,T1,U. ⦃h, L⦄ ⊢ T1 •*[g] U →
+                     ∀T2. ⦃h, L⦄ ⊢ U •*[g] T2 → ⦃h, L⦄ ⊢ T1 •*[g] T2.
+/2 width=3/ qed-.
+
+theorem sstas_conf: ∀h,g,L,T,U1. ⦃h, L⦄ ⊢ T •*[g] U1 →
+                    ∀U2. ⦃h, L⦄ ⊢ T •*[g] U2 →
+                   ⦃h, L⦄ ⊢ U1 •*[g] U2 ∨ ⦃h, L⦄ ⊢ U2 •*[g] U1.
+#h #g #L #T #U1 #H1 @(sstas_ind_dx … H1) -T /2 width=1/
+#T #U #l #HTU #HU1 #IHU1 #U2 #H2
+elim (sstas_strip … H2 … HTU) #H destruct
+[ -H2 -IHU1 /3 width=4/
+| -T /2 width=1/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/unfold.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/unfold.ma
new file mode 100644
index 000000000..4235f281e
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/unfold.ma
@@ -0,0 +1,31 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/relocation/ldrop.ma".
+
+(* CONTEXT-SENSITIVE UNFOLD FOR TERMS ***************************************)
+
+inductive unfold: lenv → relation2 term lenv ≝
+| unfold_sort: ∀L,k. unfold L (⋆k) L
+| unfold_lref: ∀I,L1,L2,K1,K2,V,i. ⇩[0, i] L1 ≡ K1. ⓑ{I}V →
+               unfold K1 V K2 → ⇩[|L2|, i] L2 ≡ K2 →
+               unfold L1 (#i) (L1@@L2)
+| unfold_bind: ∀a,I,L1,L2,V,T.
+               unfold (L1.ⓑ{I}V) T L2 → unfold L1 (ⓑ{a,I}V.T) L2
+| unfold_flat: ∀I,L1,L2,V,T.
+               unfold L1 T L2 → unfold L1 (ⓕ{I}V.T) L2
+.
+
+interpretation "context-sensitive unfold (term)"
+   'Unwind L1 T L2 = (unfold L1 T L2).
diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
index 8ed310e1e..70fad245b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
@@ -10,7 +10,7 @@ table {
      }
    ]
 (*
-   class "wine"
+   class "magenta"
    [ { "higher order dynamic typing" * } {
         [ { "higher order native type assignment" * } {
              [ "ntas ( ⦃?,?⦄ ⊢ ? :* ? )" "nta_lift" * ]
@@ -19,7 +19,7 @@ table {
      }
    ]
 *)
-   class "magenta"
+   class "prune"
    [ { "dynamic typing" * } {
 (*
         [ { "local env. ref. for native type assignment" * } {
@@ -49,7 +49,7 @@ table {
         ]
      }
    ]
-   class "prune"
+   class "blue"
    [ { "equivalence" * } {
         [ { "focalized equivalence" * } {
              [ "lfpcs ( ⦃?⦄ ⬌* ⦃?⦄ )" "lfpcs_aaa" + "lfpcs_fpcs" + "lfpcs_lfprs" + "lfpcs_lfpcs" * ]
@@ -66,7 +66,7 @@ table {
         ]
      }
    ]
-   class "blue"
+   class "sky"
    [ { "conversion" * } {
         [ { "focalized conversion" * } {
              [ "lfpc ( ⦃?⦄ ⬌ ⦃?⦄ )" "lfpc_lfpc" * ]
@@ -79,7 +79,7 @@ table {
         ]
      }
    ]
-   class "sky"
+   class "cyan"
    [ { "computation" * } {
         [ { "focalized computation" * } {
              [ "lfprs ( ⦃?⦄ ➡* ⦃?⦄ )" "lfprs_aaa" + "lfprs_ltprs" + "lfprs_cprs" + "lfprs_fprs" + "lfprs_lfprs" * ]
@@ -118,7 +118,7 @@ table {
         ]
      }
    ]
-   class "cyan"
+   class "water"
    [ { "reducibility" * } {
         [ { "context-sensitive focalized reduction" * } {
              [ "cfpr ( ? ⊢ ⦃?,?⦄ ➡ ⦃?,?⦄ )" "cnfpr_ltpss" + "cfpr_aaa" + "cfpr_cpr" + "cfpr_cfpr" * ]
@@ -157,17 +157,17 @@ table {
         ]
      }
    ]
-   class "water"
-   [ { "restricted computation" * } {
+   class "green"
+   [ { "unfold" * } {
         [ { "restricted parallel computation" * } {
              [ "lpqs ( ? ⊢ ➤* ? )" "lpqs_ldrop" + "lpqs_cpqs" + "lpqs_lpqs" * ]
              [ "cpqs ( ? ⊢ ? ➤* ? )" "cpqs_lift" * ]
           }
         ]
-     }
-   ]   
-   class "green"
-   [ { "unwind" * } {
+        [ { "unfold" * } {
+             [ "unfold ( ? ⊢ ? ⧫* ? )" * ]
+          }
+        ]
         [ { "iterated stratified static type assignment" * } {
              [ "sstas ( ⦃?,?⦄ ⊢ ? •*[?] ? )" "sstas_lift" + "sstas_lpss" + "sstas_aaa" + "sstas_sstas" * ]
           }
@@ -195,7 +195,7 @@ table {
      }
    ]
    class "yellow"
-   [ { "unfold" * } {
+   [ { "substitution" * } {
 (*        
 	[ { "basic local env. thinning" * } {
              [ "thin ( ? ▼*[?,?] ≡ ? )" "thin_ldrop" + "thin_delift" * ]
@@ -232,7 +232,7 @@ table {
      }
    ]
    class "orange"
-   [ { "substitution" * } {
+   [ { "relocation" * } {
         [ { "structural successor for closures" * } {
              [ "fsup ( ⦃?,?⦄ ⊃ ⦃?,?⦄ )" * ]
           }
-- 
2.39.2