From eb4b3b1b307fc392c36f0be253e6a111553259bc Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 5 Apr 2013 11:56:45 +0000
Subject: [PATCH] - parallel substitution reaxiomatized - supclosure
 reaxiomatixed (now commutes with parallel substitution) - some refactoring

---
 .../basic_2/computation/ltprs_ltprs.ma        |   2 +-
 .../basic_2/computation/tprs_tprs.ma          |   2 +-
 .../lambdadelta/basic_2/etc/csup/csup.etc     | 109 ++---------
 .../basic_2/etc/csup/csup_csup.etc            |  16 --
 .../lambdadelta/basic_2/etc/csup/csupp.etc    |  64 ------
 .../lambdadelta/basic_2/etc/csup/csups.etc    | 107 ----------
 .../basic_2/etc/csup/csups_csups.etc          |   5 -
 .../frsup.ma => etc/frsup/frsup.etc}          |   4 +
 .../frsupp.ma => etc/frsup/frsupp.etc}        |   4 +
 .../frsup/frsupp_frsupp.etc}                  |   0
 .../frsups.ma => etc/frsup/frsups.etc}        |   4 +
 .../frsup/frsups_frsups.etc}                  |   0
 .../basic_2/etc/frsup/ssta_frsups.etc         |  70 +++++++
 .../lambdadelta/basic_2/etc/fsup/fsup.etc     |  73 +++++++
 .../lambdadelta/basic_2/etc/fsup/fsups.etc    |  92 +++++++++
 .../etc/{xpr/xpr.etc => fsup/fsups_fsups.etc} |  24 +--
 .../basic_2/etc/fsup/ldrop_fsup.etc           |  62 ++++++
 .../basic_2/etc/fsup/ldrop_fsups.etc          |  30 +++
 .../lambdadelta/basic_2/grammar/cl_weight.ma  |   8 +-
 .../contribs/lambdadelta/basic_2/notation.ma  |  36 +---
 .../basic_2/reducibility/cpr_cpr.ma           |   4 +-
 .../basic_2/reducibility/cpr_lift.ma          |   4 +-
 .../basic_2/reducibility/cpr_ltpr.ma          |  10 +-
 .../basic_2/reducibility/cpr_ltpss_sn.ma      |   2 +-
 .../basic_2/reducibility/cpr_tpss.ma          |   4 +-
 .../basic_2/reducibility/fpr_cpr.ma           |   2 +-
 .../basic_2/reducibility/lfpr_cpr.ma          |  23 +++
 .../basic_2/reducibility/ltpr_ldrop.ma        |  15 ++
 .../basic_2/reducibility/ltpr_ltpss_dx.ma     |   6 +-
 .../basic_2/reducibility/ltpr_tps.ma          |  40 ++--
 .../{tpr_tpss.ma => ltpr_tpss.ma}             |  40 ++--
 .../basic_2/reducibility/tpr_delift.ma        |   4 +-
 .../basic_2/reducibility/tpr_tpr.ma           |  12 +-
 .../basic_2/reducibility/tpr_tps.ma           |  57 ------
 .../lambdadelta/basic_2/reducibility/xpr.ma   |  66 +++++++
 .../lambdadelta/basic_2/static/ssta.ma        |  53 -----
 .../lambdadelta/basic_2/static/ssta_ssta.ma   |  12 +-
 .../lambdadelta/basic_2/substitution/fsup.ma  |  70 +++++++
 .../lambdadelta/basic_2/substitution/ldrop.ma |  19 +-
 .../basic_2/substitution/ldrop_lpx.ma         |   6 +-
 .../lambdadelta/basic_2/substitution/lift.ma  |   2 +-
 .../lambdadelta/basic_2/substitution/tps.ma   |   8 +-
 .../lambdadelta/basic_2/unfold/cpss.ma        | 183 ++++++++++++++++++
 .../lambdadelta/basic_2/unfold/cpss_lift.ma   |  69 +++++++
 .../lambdadelta/basic_2/unfold/delift.ma      |   2 +-
 .../lambdadelta/basic_2/unfold/fsupp.ma       |  60 ++++++
 .../csupp_csupp.etc => unfold/fsupp_fsupp.ma} |   4 +-
 .../lambdadelta/basic_2/unfold/lcpss.ma       |  89 +++++++++
 .../lambdadelta/basic_2/unfold/lcpss_cpss.ma  | 145 ++++++++++++++
 .../lambdadelta/basic_2/unfold/lcpss_lcpss.ma |  55 ++++++
 .../lambdadelta/basic_2/unfold/lcpss_ldrop.ma |  69 +++++++
 .../lambdadelta/basic_2/unfold/ltpss_dx.ma    |   6 +-
 .../basic_2/unfold/ltpss_dx_ldrop.ma          |  99 ++++++++++
 .../basic_2/unfold/ltpss_dx_tpss.ma           |   1 -
 .../lambdadelta/basic_2/unfold/ltpss_sn.ma    |   6 +-
 .../basic_2/unfold/ltpss_sn_alt.ma            |   4 +
 .../basic_2/unfold/ltpss_sn_ldrop.ma          |  42 ++++
 .../lambdadelta/basic_2/unfold/tpss.ma        |   8 +-
 .../lambdadelta/basic_2/unfold/tpss_alt.ma    |   4 +
 .../lambdadelta/basic_2/web/basic_2_src.tbl   |  28 +--
 60 files changed, 1513 insertions(+), 532 deletions(-)
 delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/csup/csupp.etc
 delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/csup/csups.etc
 rename matita/matita/contribs/lambdadelta/basic_2/{substitution/frsup.ma => etc/frsup/frsup.etc} (96%)
 rename matita/matita/contribs/lambdadelta/basic_2/{unfold/frsupp.ma => etc/frsup/frsupp.etc} (96%)
 rename matita/matita/contribs/lambdadelta/basic_2/{unfold/frsupp_frsupp.ma => etc/frsup/frsupp_frsupp.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{unfold/frsups.ma => etc/frsup/frsups.etc} (96%)
 rename matita/matita/contribs/lambdadelta/basic_2/{unfold/frsups_frsups.ma => etc/frsup/frsups_frsups.etc} (100%)
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/frsup/ssta_frsups.etc
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/fsup/fsup.etc
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/fsup/fsups.etc
 rename matita/matita/contribs/lambdadelta/basic_2/etc/{xpr/xpr.etc => fsup/fsups_fsups.etc} (58%)
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/fsup/ldrop_fsup.etc
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/fsup/ldrop_fsups.etc
 rename matita/matita/contribs/lambdadelta/basic_2/reducibility/{tpr_tpss.ma => ltpr_tpss.ma} (78%)
 delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tps.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/reducibility/xpr.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/substitution/fsup.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/unfold/cpss.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/unfold/cpss_lift.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/unfold/fsupp.ma
 rename matita/matita/contribs/lambdadelta/basic_2/{etc/csup/csupp_csupp.etc => unfold/fsupp_fsupp.ma} (93%)
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/unfold/lcpss.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/unfold/lcpss_cpss.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/unfold/lcpss_lcpss.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/unfold/lcpss_ldrop.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs_ltprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs_ltprs.ma
index aec82cd5a..7ededf2af 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs_ltprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs_ltprs.ma
@@ -19,7 +19,7 @@ include "basic_2/computation/ltprs.ma".
 
 (* Advanced properties ******************************************************)
 
-lemma ltprs_strip: ∀L1. ∀L:term. L ➡* L1 → ∀L2. L ➡ L2 →
+lemma ltprs_strip: ∀L1. ∀L:lenv. L ➡* L1 → ∀L2. L ➡ L2 →
                    ∃∃L0. L1 ➡ L0 & L2 ➡* L0.
 /3 width=3/ qed.
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/tprs_tprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/tprs_tprs.ma
index ec3c9cc57..87a4a71ab 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/tprs_tprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/tprs_tprs.ma
@@ -22,7 +22,7 @@ include "basic_2/computation/tprs.ma".
 (* Basic_1: was: pr1_strip *)
 lemma tprs_strip: ∀T1,T. T ➡* T1 → ∀T2. T ➡ T2 →
                   ∃∃T0. T1 ➡ T0 & T2 ➡* T0.
-/3 width=3/ qed.
+/3 width=3 by TC_strip1, tpr_conf/ qed.
 
 (* Main propertis ***********************************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csup.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csup.etc
index dcfe086e9..0a980f6a7 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csup.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csup.etc
@@ -1,94 +1,5 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-notation "hvbox( ⦃ L1, break T1 ⦄ > break ⦃ L2 , break T2 ⦄ )"
-   non associative with precedence 45
-   for @{ 'SupTerm $L1 $T1 $L2 $T2 }.
-
-include "basic_2/substitution/ldrop.ma".
-
-(* SUPCLOSURE ***************************************************************)
-
-inductive csup: bi_relation lenv term ≝
-| csup_lref   : ∀I,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → csup L (#i) K V
-| csup_bind_sn: ∀a,I,L,V,T. csup L (ⓑ{a,I}V.T) L V
-| csup_bind_dx: ∀a,I,L,V,T. csup L (ⓑ{a,I}V.T) (L.ⓑ{I}V) T
-| csup_flat_sn: ∀I,L,V,T.   csup L (ⓕ{I}V.T) L V
-| csup_flat_dx: ∀I,L,V,T.   csup L (ⓕ{I}V.T) L T
-.
-
-interpretation
-   "structural predecessor (closure)"
-   'SupTerm L1 T1 L2 T2 = (csup L1 T1 L2 T2).
-
-(* Basic inversion lemmas ***************************************************)
-
-fact csup_inv_atom1_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ → ∀J. T1 = ⓪{J} →
-                         ∃∃I,i. ⇩[0, i] L1 ≡ L2.ⓑ{I}T2 & J = LRef i.
-#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2
-[ #I #L #K #V #i #HLK #J #H destruct /2 width=4/
-| #a #I #L #V #T #J #H destruct
-| #a #I #L #V #T #J #H destruct
-| #I #L #V #T #J #H destruct
-| #I #L #V #T #J #H destruct
-]
-qed-.
-
-lemma csup_inv_atom1: ∀J,L1,L2,T2. ⦃L1, ⓪{J}⦄ > ⦃L2, T2⦄ →
-                      ∃∃I,i. ⇩[0, i] L1 ≡ L2.ⓑ{I}T2 & J = LRef i.
-/2 width=3 by csup_inv_atom1_aux/ qed-.
-
-fact csup_inv_bind1_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ →
-                         ∀b,J,W,U. T1 = ⓑ{b,J}W.U →
-                         (L2 = L1 ∧ T2 = W) ∨
-                         (L2 = L1.ⓑ{J}W ∧ T2 = U).
-#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2
-[ #I #L #K #V #i #_ #b #J #W #U #H destruct
-| #a #I #L #V #T #b #J #W #U #H destruct /3 width=1/
-| #a #I #L #V #T #b #J #W #U #H destruct /3 width=1/
-| #I #L #V #T #b #J #W #U #H destruct
-| #I #L #V #T #b #J #W #U #H destruct
-]
-qed-.
-
-lemma csup_inv_bind1: ∀b,J,L1,L2,W,U,T2. ⦃L1, ⓑ{b,J}W.U⦄ > ⦃L2, T2⦄ →
-                      (L2 = L1 ∧ T2 = W) ∨
-                      (L2 = L1.ⓑ{J}W ∧ T2 = U).
-/2 width=4 by csup_inv_bind1_aux/ qed-.
-
-fact csup_inv_flat1_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ →
-                         ∀J,W,U. T1 = ⓕ{J}W.U →
-                         L2 = L1 ∧ (T2 = W ∨ T2 = U).
-#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2
-[ #I #L #K #V #i #_ #J #W #U #H destruct
-| #a #I #L #V #T #J #W #U #H destruct
-| #a #I #L #V #T #J #W #U #H destruct
-| #I #L #V #T #J #W #U #H destruct /3 width=1/
-| #I #L #V #T #J #W #U #H destruct /3 width=1/
-]
-qed-.
-
-lemma csup_inv_flat1: ∀J,L1,L2,W,U,T2. ⦃L1, ⓕ{J}W.U⦄ > ⦃L2, T2⦄ →
-                      L2 = L1 ∧ (T2 = W ∨ T2 = U).
-/2 width=4 by csup_inv_flat1_aux/ qed-.
-
 (* Basic forward lemmas *****************************************************)
 
-lemma csup_fwd_cw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ → #{L2, T2} < #{L1, T1}.
-#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2 /width=1/ /2 width=4 by ldrop_pair2_fwd_cw/
-qed-.
-
 lemma csup_fwd_ldrop: ∀L1,L2,T1,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ →
                       ∃i. ⇩[0, i] L1 ≡ L2 ∨ ⇩[0, i] L2 ≡ L1.
 #L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2 /3 width=2/ /4 width=2/
@@ -155,3 +66,23 @@ lemma csup_inv_lref2_be: ∀L,U,i. ⦃L, U⦄ > ⦃L, #i⦄ →
 elim (lift_csup_trans_eq … HTU … H) -H -T #T #H
 elim (lift_inv_lref2_be … H ? ?) //
 qed-.
+
+
+fact csup_inv_all4_refl_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ → L1 = L2 →
+                             ∨∨ ∃∃a,I,U. T1 = ⓑ{a,I}T2.U
+                              | ∃∃I,W. T1 = ⓕ{I}W.T2
+                              | ∃∃I,U. T1 = ⓕ{I}T2.U.
+#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2 /3 width=3/ /3 width=4/
+[ #I #L #K #V #i #HLK #H destruct
+  lapply (ldrop_pair2_fwd_cw … HLK V) -HLK #H
+  elim (lt_refl_false … H)
+| #a #I #L #V #T #H
+  elim (discr_lpair_x_xy … H)
+]
+qed-.
+
+lemma csup_inv_all4_refl: ∀L,T1,T2. ⦃L, T1⦄ > ⦃L, T2⦄ →
+                          ∨∨ ∃∃a,I,U. T1 = ⓑ{a,I}T2.U
+                           | ∃∃I,W. T1 = ⓕ{I}W.T2
+                           | ∃∃I,U. T1 = ⓕ{I}T2.U.
+/2 width=4 by csup_inv_all4_refl_aux/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csup_csup.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csup_csup.etc
index 813cb969d..661d89697 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csup_csup.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csup_csup.etc
@@ -17,22 +17,6 @@ include "basic_2/substitution/csup.ma".
 
 (* SUPCLOSURE ***************************************************************)
 
-(* Advanced inversion lemmas ************************************************)
-
-lemma csup_inv_ldrop: ∀L1,L2,T1,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ →
-                      ∀J,W,j. ⇩[0, j] L1 ≡ L2.ⓑ{J}W → T1 = #j ∧ T2 = W.
-#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2
-[ #I #L #K #V #i #HLKV #J #W #j #HLKW
-  elim (ldrop_conf_div … HLKV … HLKW) -L /2 width=1/
-| #a
-| #a
-]
-#I #L #V #T #J #W #j #H
-lapply (ldrop_pair2_fwd_cw … H W) -H #H
-[2: lapply (transitive_lt (#{L,W}) … H) /2 width=1/ -H #H ]
-elim (lt_refl_false … H)
-qed-.
-
 (* Main forward lemmas ******************************************************)
 
 theorem csup_trans_fwd_refl: ∀L,L0,T1,T2. ⦃L, T1⦄ > ⦃L0, T2⦄ →
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csupp.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csupp.etc
deleted file mode 100644
index c28eaea73..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csupp.etc
+++ /dev/null
@@ -1,64 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-notation "hvbox( ⦃ L1, break T1 ⦄ > + break ⦃ L2 , break T2 ⦄ )"
-   non associative with precedence 45
-   for @{ 'SupTermPlus $L1 $T1 $L2 $T2 }.
-
-include "basic_2/substitution/csup.ma".
-
-(* PLUS-ITERATED SUPCLOSURE *************************************************)
-
-definition csupp: bi_relation lenv term ≝ bi_TC … csup.
-
-interpretation "plus-iterated structural predecessor (closure)"
-   'SupTermPlus L1 T1 L2 T2 = (csupp L1 T1 L2 T2).
-
-(* Basic eliminators ********************************************************)
-
-lemma csupp_ind: ∀L1,T1. ∀R:relation2 lenv term.
-                 (∀L2,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ → R L2 T2) →
-                 (∀L,T,L2,T2. ⦃L1, T1⦄ >+ ⦃L, T⦄ → ⦃L, T⦄ > ⦃L2, T2⦄ → R L T → R L2 T2) →
-                 ∀L2,T2. ⦃L1, T1⦄ >+ ⦃L2, T2⦄ → R L2 T2.
-#L1 #T1 #R #IH1 #IH2 #L2 #T2 #H
-@(bi_TC_ind … IH1 IH2 ? ? H)
-qed-.
-
-lemma csupp_ind_dx: ∀L2,T2. ∀R:relation2 lenv term.
-                    (∀L1,T1. ⦃L1, T1⦄ > ⦃L2, T2⦄ → R L1 T1) →
-                    (∀L1,L,T1,T. ⦃L1, T1⦄ > ⦃L, T⦄ → ⦃L, T⦄ >+ ⦃L2, T2⦄ → R L T → R L1 T1) →
-                    ∀L1,T1. ⦃L1, T1⦄ >+ ⦃L2, T2⦄ → R L1 T1.
-#L2 #T2 #R #IH1 #IH2 #L1 #T1 #H
-@(bi_TC_ind_dx … IH1 IH2 ? ? H)
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma csup_csupp: ∀L1,L2,T1,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ → ⦃L1, T1⦄ >+ ⦃L2, T2⦄.
-/2 width=1/ qed.
-
-lemma csupp_strap1: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ >+ ⦃L, T⦄ → ⦃L, T⦄ > ⦃L2, T2⦄ →
-                    ⦃L1, T1⦄ >+ ⦃L2, T2⦄.
-/2 width=4/ qed.
-
-lemma csupp_strap2: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ > ⦃L, T⦄ → ⦃L, T⦄ >+ ⦃L2, T2⦄ →
-                    ⦃L1, T1⦄ >+ ⦃L2, T2⦄.
-/2 width=4/ qed.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma csupp_fwd_cw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ >+ ⦃L2, T2⦄ → #{L2, T2} < #{L1, T1}.
-#L1 #L2 #T1 #T2 #H @(csupp_ind … H) -L2 -T2
-/3 width=3 by csup_fwd_cw, transitive_lt/
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csups.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csups.etc
deleted file mode 100644
index 7f5879426..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csups.etc
+++ /dev/null
@@ -1,107 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-notation "hvbox( ⦃ L1, break T1 ⦄ > * break ⦃ L2 , break T2 ⦄ )"
-   non associative with precedence 45
-   for @{ 'SupTermStar $L1 $T1 $L2 $T2 }.
-
-include "basic_2/substitution/csup.ma".
-include "basic_2/unfold/csupp.ma".
-
-(* STAR-ITERATED SUPCLOSURE *************************************************)
-
-definition csups: bi_relation lenv term ≝ bi_star … csup.
-
-interpretation "star-iterated structural predecessor (closure)"
-   'SupTermStar L1 T1 L2 T2 = (csups L1 T1 L2 T2).
-
-(* Basic eliminators ********************************************************)
-
-lemma csups_ind: ∀L1,T1. ∀R:relation2 lenv term. R L1 T1 →
-                 (∀L,L2,T,T2. ⦃L1, T1⦄ >* ⦃L, T⦄ → ⦃L, T⦄ > ⦃L2, T2⦄ → R L T → R L2 T2) →
-                 ∀L2,T2. ⦃L1, T1⦄ >* ⦃L2, T2⦄ → R L2 T2.
-#L1 #T1 #R #IH1 #IH2 #L2 #T2 #H
-@(bi_star_ind … IH1 IH2 ? ? H)
-qed-.
-
-lemma csups_ind_dx: ∀L2,T2. ∀R:relation2 lenv term. R L2 T2 →
-                    (∀L1,L,T1,T. ⦃L1, T1⦄ > ⦃L, T⦄ → ⦃L, T⦄ >* ⦃L2, T2⦄ → R L T → R L1 T1) →
-                    ∀L1,T1. ⦃L1, T1⦄ >* ⦃L2, T2⦄ → R L1 T1.
-#L2 #T2 #R #IH1 #IH2 #L1 #T1 #H
-@(bi_star_ind_dx … IH1 IH2 ? ? H)
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma csups_refl: bi_reflexive … csups.
-/2 width=1/ qed.
-
-lemma csupp_csups: ∀L1,L2,T1,T2. ⦃L1, T1⦄ >+ ⦃L2, T2⦄ → ⦃L1, T1⦄ >* ⦃L2, T2⦄.
-/2 width=1/ qed.
-
-lemma csup_csups: ∀L1,L2,T1,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ → ⦃L1, T1⦄ >* ⦃L2, T2⦄.
-/2 width=1/ qed.
-
-lemma csups_strap1: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ >* ⦃L, T⦄ → ⦃L, T⦄ > ⦃L2, T2⦄ →
-                    ⦃L1, T1⦄ >* ⦃L2, T2⦄.
-/2 width=4/ qed.
-
-lemma csups_strap2: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ > ⦃L, T⦄ → ⦃L, T⦄ >* ⦃L2, T2⦄ →
-                    ⦃L1, T1⦄ >* ⦃L2, T2⦄.
-/2 width=4/ qed.
-
-lemma csups_csupp_csupp: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ >* ⦃L, T⦄ →
-                         ⦃L, T⦄ >+ ⦃L2, T2⦄ → ⦃L1, T1⦄ >+ ⦃L2, T2⦄.
-/2 width=4/ qed.
-
-lemma csupp_csups_csupp: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ >+ ⦃L, T⦄ →
-                          ⦃L, T⦄ >* ⦃L2, T2⦄ → ⦃L1, T1⦄ >+ ⦃L2, T2⦄.
-/2 width=4/ qed.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma csups_fwd_cw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ >* ⦃L2, T2⦄ → #{L2, T2} ≤ #{L1, T1}.
-#L1 #L2 #T1 #T2 #H @(csups_ind … H) -L2 -T2 //
-/4 width=3 by csup_fwd_cw, lt_to_le_to_lt, lt_to_le/ (**) (* slow even with trace *)
-qed-.
-
-(* Advanced inversion lemmas for csupp **************************************)
-
-lemma csupp_inv_atom1_csups: ∀J,L1,L2,T2. ⦃L1, ⓪{J}⦄ >+ ⦃L2, T2⦄ →
-                             ∃∃I,K,V,i. ⇩[0, i] L1 ≡ K.ⓑ{I}V &
-                             ⦃K, V⦄ >* ⦃L2, T2⦄ & J = LRef i.
-#J #L1 #L2 #T2 #H @(csupp_ind … H) -L2 -T2
-[ #L2 #T2 #H
-  elim (csup_inv_atom1 … H) -H * #i #HL12 #H destruct /2 width=7/
-| #L #T #L2 #T2 #_ #HT2 * #I #K #V #i #HLK #HVT #H destruct /3 width=8/
-]
-qed-.
-
-lemma csupp_inv_bind1_csups: ∀b,J,L1,L2,W,U,T2. ⦃L1, ⓑ{b,J}W.U⦄ >+ ⦃L2, T2⦄ →
-                             ⦃L1, W⦄ >* ⦃L2, T2⦄ ∨ ⦃L1.ⓑ{J}W, U⦄ >* ⦃L2, T2⦄.
-#b #J #L1 #L2 #W #U #T2 #H @(csupp_ind … H) -L2 -T2
-[ #L2 #T2 #H
-  elim (csup_inv_bind1 … H) -H * #H1 #H2 destruct /2 width=1/
-| #L #T #L2 #T2 #_ #HT2 * /3 width=4/
-]
-qed-.
-
-lemma csupp_inv_flat1_csups: ∀J,L1,L2,W,U,T2. ⦃L1, ⓕ{J}W.U⦄ >+ ⦃L2, T2⦄ →
-                             ⦃L1, W⦄ >* ⦃L2, T2⦄ ∨ ⦃L1, U⦄ >* ⦃L2, T2⦄.
-#J #L1 #L2 #W #U #T2 #H @(csupp_ind … H) -L2 -T2
-[ #L2 #T2 #H
-  elim (csup_inv_flat1 … H) -H #H1 * #H2 destruct /2 width=1/
-| #L #T #L2 #T2 #_ #HT2 * /3 width=4/
-]
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csups_csups.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csups_csups.etc
index aa54d9bef..9978429d7 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csups_csups.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csups_csups.etc
@@ -55,8 +55,3 @@ lemma lift_csups_trans_aux: ∀T1,U1,d,e. ⇧[d, e] T1 ≡ U1 →
 #L #L2 #U #U2 #HL1 #HL2 #IHL1 #H destruct
 
 * -T1 -U1 -d -e
-
-(* Main propertis ***********************************************************)
-
-theorem csups_trans: bi_transitive … csups.
-/2 width=4/ qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/frsup.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/frsup/frsup.etc
similarity index 96%
rename from matita/matita/contribs/lambdadelta/basic_2/substitution/frsup.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/frsup/frsup.etc
index a561410d8..077fd7422 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/frsup.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/frsup/frsup.etc
@@ -12,6 +12,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
+notation "hvbox( ⦃ term 46 L1, break term 46 T1 ⦄ ⧁ break ⦃ term 46 L2 , break term 46 T2 ⦄ )"
+   non associative with precedence 45
+   for @{ 'RestSupTerm $L1 $T1 $L2 $T2 }.
+
 include "basic_2/grammar/cl_weight.ma".
 include "basic_2/substitution/lift.ma".
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/frsupp.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/frsup/frsupp.etc
similarity index 96%
rename from matita/matita/contribs/lambdadelta/basic_2/unfold/frsupp.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/frsup/frsupp.etc
index add56ba3d..9f7a8dc9d 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/frsupp.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/frsup/frsupp.etc
@@ -12,6 +12,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
+notation "hvbox( ⦃ term 46 L1, break term 46 T1 ⦄ ⧁ + break ⦃ term 46 L2 , break term 46 T2 ⦄ )"
+   non associative with precedence 45
+   for @{ 'RestSupTermPlus $L1 $T1 $L2 $T2 }.
+
 include "basic_2/substitution/frsup.ma".
 
 (* PLUS-ITERATED RESTRICTED SUPCLOSURE **************************************)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/frsupp_frsupp.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/frsup/frsupp_frsupp.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/unfold/frsupp_frsupp.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/frsup/frsupp_frsupp.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/frsups.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/frsup/frsups.etc
similarity index 96%
rename from matita/matita/contribs/lambdadelta/basic_2/unfold/frsups.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/frsup/frsups.etc
index 373454cf9..6e70e76a9 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/frsups.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/frsup/frsups.etc
@@ -12,6 +12,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
+notation "hvbox( ⦃ term 46 L1, break term 46 T1 ⦄ ⧁ * break ⦃ term 46 L2 , break term 46 T2 ⦄ )"
+   non associative with precedence 45
+   for @{ 'RestSupTermStar $L1 $T1 $L2 $T2 }.
+
 include "basic_2/unfold/frsupp.ma".
 
 (* STAR-ITERATED RESTRICTED SUPCLOSURE **************************************)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/frsups_frsups.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/frsup/frsups_frsups.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/unfold/frsups_frsups.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/frsup/frsups_frsups.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/frsup/ssta_frsups.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/frsup/ssta_frsups.etc
new file mode 100644
index 000000000..9eb1fbd8b
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/frsup/ssta_frsups.etc
@@ -0,0 +1,70 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/frsups.ma".
+include "basic_2/static/ssta.ma".
+
+(* STRATIFIED STATIC TYPE ASSIGNMENT ON TERMS *******************************)
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma ssta_inv_frsupp: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g] ⦃l, U⦄ → ⦃L, U⦄ ⧁+ ⦃L, T⦄ → ⊥.
+#h #g #L #T #U #l #H elim H -L -T -U -l
+[ #L #k #l #_ #H
+  elim (frsupp_inv_atom1_frsups … H)
+| #L #K #V #W #U #i #l #_ #_ #HWU #_ #H
+  elim (lift_frsupp_trans … (⋆) … H … HWU) -U #X #H
+  elim (lift_inv_lref2_be … H ? ?) -H //
+| #L #K #W #V #U #i #l #_ #_ #HWU #_ #H
+  elim (lift_frsupp_trans … (⋆) … H … HWU) -U #X #H
+  elim (lift_inv_lref2_be … H ? ?) -H //
+| #a #I #L #V #T #U #l #_ #IHTU #H
+  elim (frsupp_inv_bind1_frsups … H) -H #H [2: /4 width=4/ ] -IHTU
+  lapply (frsups_fwd_fw … H) -H normalize
+  <associative_plus <associative_plus #H
+  elim (le_plus_xySz_x_false … H)
+| #L #V #T #U #l #_ #IHTU #H
+  elim (frsupp_inv_flat1_frsups … H) -H #H [2: /4 width=4/ ] -IHTU
+  lapply (frsups_fwd_fw … H) -H normalize
+  <associative_plus <associative_plus #H
+  elim (le_plus_xySz_x_false … H)
+| /3 width=4/
+]
+qed-.
+
+fact ssta_inv_refl_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g] ⦃l, U⦄ → T = U → ⊥.
+#h #g #L #T #U #l #H elim H -L -T -U -l
+[ #L #k #l #_ #H
+  lapply (next_lt h k) destruct -H -e0 (**) (* destruct: these premises are not erased *)
+  <e1 -e1 #H elim (lt_refl_false … H)
+| #L #K #V #W #U #i #l #_ #_ #HWU #_ #H destruct
+  elim (lift_inv_lref2_be … HWU ? ?) -HWU //
+| #L #K #W #V #U #i #l #_ #_ #HWU #_ #H destruct
+  elim (lift_inv_lref2_be … HWU ? ?) -HWU //
+| #a #I #L #V #T #U #l #_ #IHTU #H destruct /2 width=1/
+| #L #V #T #U #l #_ #IHTU #H destruct /2 width=1/
+| #L #W #T #U #l #HTU #_ #H destruct
+  elim (ssta_inv_frsupp … HTU ?) -HTU /2 width=1/
+]
+qed-.
+
+lemma ssta_inv_refl: ∀h,g,T,L,l. ⦃h, L⦄ ⊢ T •[g] ⦃l, T⦄ → ⊥.
+/2 width=8 by ssta_inv_refl_aux/ qed-.
+
+lemma ssta_inv_frsups: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g] ⦃l, U⦄ → ⦃L, U⦄ ⧁* ⦃L, T⦄ → ⊥.
+#h #g #L #T #U #L #HTU #H elim (frsups_inv_all … H) -H
+[ * #_ #H destruct /2 width=6 by ssta_inv_refl/
+| /2 width=8 by ssta_inv_frsupp/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fsup/fsup.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fsup/fsup.etc
new file mode 100644
index 000000000..b3970be51
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fsup/fsup.etc
@@ -0,0 +1,73 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/substitution/ldrop.ma".
+
+(* SUPCLOSURE ***************************************************************)
+
+(* Basic inversion lemmas ***************************************************)
+
+fact fsup_inv_atom1_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ∀J. T1 = ⓪{J} →
+                         (∃∃I,K,V. L1 = K.ⓑ{I}V & J = LRef 0 & L2 = K & T2 = V) ∨
+                         ∃∃I,K,V,i. ⦃K, #i⦄ ⊃ ⦃L2, T2⦄ & L1 = K.ⓑ{I}V & J = LRef (i+1).
+#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2
+[ #I #L #V #J #H destruct /3 width=6/
+| #I #L #K #V #T #i #HLK #J #H destruct /3 width=7/
+| #a #I #L #V #T #J #H destruct
+| #a #I #L #V #T #J #H destruct
+| #I #L #V #T #J #H destruct
+| #I #L #V #T #J #H destruct
+]
+qed-.
+
+lemma fsup_inv_atom1: ∀J,L1,L2,T2. ⦃L1, ⓪{J}⦄ ⊃ ⦃L2, T2⦄ →
+                      (∃∃I,K,V. L1 = K.ⓑ{I}V & J = LRef 0 & L2 = K & T2 = V) ∨
+                      ∃∃I,K,V,i. ⦃K, #i⦄ ⊃ ⦃L2, T2⦄ & L1 = K.ⓑ{I}V & J = LRef (i+1).
+/2 width=3 by fsup_inv_atom1_aux/ qed-.
+
+fact fsup_inv_bind1_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ →
+                         ∀b,J,W,U. T1 = ⓑ{b,J}W.U →
+                         (L2 = L1 ∧ T2 = W) ∨
+                         (L2 = L1.ⓑ{J}W ∧ T2 = U).
+#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2
+[ #I #L #V #b #J #W #U #H destruct
+| #I #L #K #V #T #i #_ #b #J #W #U #H destruct
+| #a #I #L #V #T #b #J #W #U #H destruct /3 width=1/
+| #a #I #L #V #T #b #J #W #U #H destruct /3 width=1/
+| #I #L #V #T #b #J #W #U #H destruct
+| #I #L #V #T #b #J #W #U #H destruct
+]
+qed-.
+
+lemma fsup_inv_bind1: ∀b,J,L1,L2,W,U,T2. ⦃L1, ⓑ{b,J}W.U⦄ ⊃ ⦃L2, T2⦄ →
+                      (L2 = L1 ∧ T2 = W) ∨
+                      (L2 = L1.ⓑ{J}W ∧ T2 = U).
+/2 width=4 by fsup_inv_bind1_aux/ qed-.
+
+fact fsup_inv_flat1_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ →
+                         ∀J,W,U. T1 = ⓕ{J}W.U →
+                         L2 = L1 ∧ (T2 = W ∨ T2 = U).
+#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2
+[ #I #L #K #J #W #U #H destruct
+| #I #L #K #V #T #i #_ #J #W #U #H destruct
+| #a #I #L #V #T #J #W #U #H destruct
+| #a #I #L #V #T #J #W #U #H destruct
+| #I #L #V #T #J #W #U #H destruct /3 width=1/
+| #I #L #V #T #J #W #U #H destruct /3 width=1/
+]
+qed-.
+
+lemma fsup_inv_flat1: ∀J,L1,L2,W,U,T2. ⦃L1, ⓕ{J}W.U⦄ ⊃ ⦃L2, T2⦄ →
+                      L2 = L1 ∧ (T2 = W ∨ T2 = U).
+/2 width=4 by fsup_inv_flat1_aux/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fsup/fsups.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fsup/fsups.etc
new file mode 100644
index 000000000..c7867e1f8
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fsup/fsups.etc
@@ -0,0 +1,92 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/grammar/fsupp.ma".
+
+(* STAR-ITERATED SUPCLOSURE *************************************************)
+
+definition fsups: bi_relation lenv term ≝ bi_star … fsup.
+
+interpretation "star-iterated structural successor (closure)"
+   'SupTermStar L1 T1 L2 T2 = (fsups L1 T1 L2 T2).
+
+(* Basic eliminators ********************************************************)
+
+lemma fsups_ind: ∀L1,T1. ∀R:relation2 lenv term. R L1 T1 →
+                 (∀L,L2,T,T2. ⦃L1, T1⦄ ⊃* ⦃L, T⦄ → ⦃L, T⦄ ⊃ ⦃L2, T2⦄ → R L T → R L2 T2) →
+                 ∀L2,T2. ⦃L1, T1⦄ ⊃* ⦃L2, T2⦄ → R L2 T2.
+#L1 #T1 #R #IH1 #IH2 #L2 #T2 #H
+@(bi_star_ind … IH1 IH2 ? ? H)
+qed-.
+
+lemma fsups_ind_dx: ∀L2,T2. ∀R:relation2 lenv term. R L2 T2 →
+                    (∀L1,L,T1,T. ⦃L1, T1⦄ ⊃ ⦃L, T⦄ → ⦃L, T⦄ ⊃* ⦃L2, T2⦄ → R L T → R L1 T1) →
+                    ∀L1,T1. ⦃L1, T1⦄ ⊃* ⦃L2, T2⦄ → R L1 T1.
+#L2 #T2 #R #IH1 #IH2 #L1 #T1 #H
+@(bi_star_ind_dx … IH1 IH2 ? ? H)
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma fsups_refl: bi_reflexive … fsups.
+/2 width=1/ qed.
+
+lemma fsupp_fsups: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⊃* ⦃L2, T2⦄.
+/2 width=1/ qed.
+
+lemma fsup_fsups: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⊃* ⦃L2, T2⦄.
+/2 width=1/ qed.
+
+lemma fsups_strap1: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⊃* ⦃L, T⦄ → ⦃L, T⦄ ⊃ ⦃L2, T2⦄ →
+                    ⦃L1, T1⦄ ⊃* ⦃L2, T2⦄.
+/2 width=4/ qed.
+
+lemma fsups_strap2: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⊃ ⦃L, T⦄ → ⦃L, T⦄ ⊃* ⦃L2, T2⦄ →
+                    ⦃L1, T1⦄ ⊃* ⦃L2, T2⦄.
+/2 width=4/ qed.
+
+lemma fsups_fsupp_fsupp: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⊃* ⦃L, T⦄ →
+                         ⦃L, T⦄ ⊃+ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄.
+/2 width=4/ qed.
+
+lemma fsupp_fsups_fsupp: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⊃+ ⦃L, T⦄ →
+                         ⦃L, T⦄ ⊃* ⦃L2, T2⦄ → ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄.
+/2 width=4/ qed.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma fsups_fwd_cw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃* ⦃L2, T2⦄ → ♯{L2, T2} ≤ ♯{L1, T1}.
+#L1 #L2 #T1 #T2 #H @(fsups_ind … H) -L2 -T2 //
+/4 width=3 by fsup_fwd_cw, lt_to_le_to_lt, lt_to_le/ (**) (* slow even with trace *)
+qed-.
+
+(* Advanced inversion lemmas on plus-iterated supclosure ********************)
+
+lemma fsupp_inv_bind1_fsups: ∀b,J,L1,L2,W,U,T2. ⦃L1, ⓑ{b,J}W.U⦄ ⊃+ ⦃L2, T2⦄ →
+                             ⦃L1, W⦄ ⊃* ⦃L2, T2⦄ ∨ ⦃L1.ⓑ{J}W, U⦄ ⊃* ⦃L2, T2⦄.
+#b #J #L1 #L2 #W #U #T2 #H @(fsupp_ind … H) -L2 -T2
+[ #L2 #T2 #H
+  elim (fsup_inv_bind1 … H) -H * #H1 #H2 destruct /2 width=1/
+| #L #T #L2 #T2 #_ #HT2 * /3 width=4/
+]
+qed-.
+
+lemma fsupp_inv_flat1_fsups: ∀J,L1,L2,W,U,T2. ⦃L1, ⓕ{J}W.U⦄ ⊃+ ⦃L2, T2⦄ →
+                             ⦃L1, W⦄ ⊃* ⦃L2, T2⦄ ∨ ⦃L1, U⦄ ⊃* ⦃L2, T2⦄.
+#J #L1 #L2 #W #U #T2 #H @(fsupp_ind … H) -L2 -T2
+[ #L2 #T2 #H
+  elim (fsup_inv_flat1 … H) -H #H1 * #H2 destruct /2 width=1/
+| #L #T #L2 #T2 #_ #HT2 * /3 width=4/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xpr.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fsup/fsups_fsups.etc
similarity index 58%
rename from matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xpr.etc
rename to matita/matita/contribs/lambdadelta/basic_2/etc/fsup/fsups_fsups.etc
index 1e17654ca..e2f893f24 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xpr.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fsup/fsups_fsups.etc
@@ -12,25 +12,11 @@
 (*                                                                        *)
 (**************************************************************************)
 
-notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 • ➡ break [ term 46 g ] break term 46 T2 )"
-   non associative with precedence 45
-   for @{ 'XPRed $h $g $L $T1 $T2 }.
+include "basic_2/grammar/fsups.ma".
 
-include "basic_2/static/ssta.ma".
-include "basic_2/reducibility/cpr.ma".
+(* STAR-ITERATED SUPCLOSURE *************************************************)
 
-(* EXTENDED PARALLEL REDUCTION ON TERMS *************************************)
+(* Main properties **********************************************************)
 
-inductive xpr (h) (g) (L) (T1) (T2): Prop ≝
-| xpr_cpr : L ⊢ T1 ➡ T2 → xpr h g L T1 T2
-| xpr_ssta: ∀l. ⦃h, L⦄ ⊢ T1 •[g, l + 1] T2 → xpr h g L T1 T2
-.
-
-interpretation
-   "extended parallel reduction (term)"
-   'XPRed h g L T1 T2 = (xpr h g L T1 T2).
-
-(* Basic properties *********************************************************)
-
-lemma xpr_refl: ∀h,g,L. reflexive … (xpr h g L).
-/2 width=1/ qed.
+theorem fsups_trans: bi_transitive … fsups.
+/2 width=4/ qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fsup/ldrop_fsup.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fsup/ldrop_fsup.etc
new file mode 100644
index 000000000..75ea3e531
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fsup/ldrop_fsup.etc
@@ -0,0 +1,62 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/substitution/fsup.ma".
+include "basic_2/substitution/ldrop_ldrop.ma".
+
+(* LOCAL ENVIRONMENT SLICING ************************************************)
+
+(* Inversion lemmas on supclosure *******************************************)
+
+lemma fsup_inv_atom1_ldrop: ∀K,V,L,I. ⦃L, ⓪{I}⦄ ⊃ ⦃K, V⦄ →
+                            ∃∃J,i. ⇩[0, i] L ≡ K.ⓑ{J}V & I = LRef i.
+#K #V #L @(f_ind … length … L) -L #n #IH #L #Hn #I #H
+elim (fsup_inv_atom1 … H) -H *
+[ #J #L0 #V0 #H1 #H2 #H3 #H4 destruct /2 width=4/
+| #J #L0 #V0 #i #HLK #H1 #H2 destruct
+  elim (IH … HLK) -IH -HLK [2: normalize // ] #I #j #HLK #H destruct /3 width=4/
+]
+qed-.
+
+(* Advanced eliminators on supclosure ***************************************)
+
+lemma fsup_ind_ldrop: ∀R:bi_relation lenv term.
+                      (∀I,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → R L (#i) K V) →
+                      (∀a,I,L,V,T. R L (ⓑ{a,I}V.T) L V) →
+                      (∀a,I,L,V,T. R L (ⓑ{a,I}V.T) (L.ⓑ{I}V) T) →
+                      (∀I,L,V,T. R L (ⓕ{I}V.T) L V) →
+                      (∀I,L,V,T. R L (ⓕ{I}V.T) L T) →
+                      ∀L1,T1,L2,T2. ⦃L1,T1⦄⊃⦃L2,T2⦄ → R L1 T1 L2 T2.
+#R #H1 #H2 #H3 #H4 #H5 #L1 #T1 #L2 #T2 #H elim H -L1 -T1 -L2 -T2 //
+[ /3 width=2/
+| #I #L #K #V #T #i #H #H1LK
+  elim (fsup_inv_atom1_ldrop … H) -H #J #j #H2LK #H destruct /3 width=2/
+]
+qed-.
+
+(* Advanced inversion lemmas on supclosure **********************************)
+
+lemma fsup_inv_ldrop: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ →
+                      ∀J,W,j. ⇩[0, j] L1 ≡ L2.ⓑ{J}W → T1 = #j ∧ T2 = W.
+#L1 #L2 #T1 #T2 #H @(fsup_ind_ldrop … H) -L1 -L2 -T1 -T2
+[ #I #L #K #V #i #HLKV #J #W #j #HLKW
+  elim (ldrop_conf_div … HLKV … HLKW) -L /2 width=1/
+| #a
+| #a
+]
+#I #L #V #T #J #W #j #H
+lapply (ldrop_pair2_fwd_fw … H W) -H #H
+[2: lapply (transitive_lt (♯{L,W}) … H) /2 width=1/ -H #H ]
+elim (lt_refl_false … H)
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fsup/ldrop_fsups.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fsup/ldrop_fsups.etc
new file mode 100644
index 000000000..dc4d7e9f4
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fsup/ldrop_fsups.etc
@@ -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/grammar/fsups.ma".
+include "basic_2/substitution/ldrop_fsup.ma".
+
+(* LOCAL ENVIRONMENT SLICING ************************************************)
+
+(* Inversion lemmas on plus-iterated supclosure  ****************************)
+
+lemma fsupp_inv_atom1_fsups: ∀J,L1,L2,T2. ⦃L1, ⓪{J}⦄ ⊃+ ⦃L2, T2⦄ →
+                             ∃∃I,K,V,i. ⇩[0, i] L1 ≡ K.ⓑ{I}V &
+                             ⦃K, V⦄ ⊃* ⦃L2, T2⦄ & J = LRef i.
+#J #L1 #L2 #T2 #H @(fsupp_ind … H) -L2 -T2
+[ #L2 #T2 #H
+  elim (fsup_inv_atom1_ldrop … H) -H * #i #HL12 #H destruct /2 width=7/
+| #L #T #L2 #T2 #_ #HT2 * #I #K #V #i #HLK #HVT #H destruct /3 width=8/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma
index 35796b6ba..2a9802626 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma
@@ -43,7 +43,7 @@ normalize in ⊢ (?→?→?→?→?%%); //
 qed.
 
 lemma fw_tpair_dx_sn: ∀I1,I2,L,V1,V2,T. ♯{L, V2} < ♯{L, ②{I1}V1.②{I2}V2.T}.
-normalize in ⊢ (?→?→?→?→?→?→?%%); /2 width=1/
+normalize in ⊢ (?→?→?→?→?→?→?%%); /2 width=1 by monotonic_le_plus_r/ (**) (* auto too slow without trace *)
 qed.
 
 lemma fw_tpair_sn_sn_shift: ∀I,I1,I2,L,V1,V2,T.
@@ -53,7 +53,11 @@ qed.
 
 lemma fw_tpair_sn_dx_shift: ∀I,I1,I2,L,V1,V2,T.
                             ♯{L.ⓑ{I}V2, T} < ♯{L, ②{I1}V1.②{I2}V2.T}.
-normalize in ⊢ (?→?→?→?→?→?→?→?%%); /2 width=1/
+normalize in ⊢ (?→?→?→?→?→?→?→?%%); /2 width=1 by monotonic_le_plus_r/ (**) (* auto too slow without trace *)
+qed.
+
+lemma fw_lpair_sn: ∀I,L,V,T. ♯{L, V} < ♯{L.ⓑ{I}V, T}.
+normalize /3 width=1 by monotonic_lt_plus_l, monotonic_le_plus_r/ (**) (* auto too slow without trace *)
 qed.
 
 (* Basic_1: removed theorems 7:
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation.ma b/matita/matita/contribs/lambdadelta/basic_2/notation.ma
index 4aa5cd88a..9c9c19209 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation.ma
@@ -162,18 +162,14 @@ notation "hvbox( ⇩ [ term 46 d , break term 46 e ] break term 46 L1 ≡ break
    non associative with precedence 45
    for @{ 'RDrop $d $e $L1 $L2 }.
 
-notation "hvbox( ⦃ term 46 L1, break term 46 T1 ⦄ ⧁ break ⦃ term 46 L2 , break term 46 T2 ⦄ )"
+notation "hvbox( ⦃ term 46 L1, break term 46 T1 ⦄ ⊃ break ⦃ term 46 L2 , break term 46 T2 ⦄ )"
    non associative with precedence 45
-   for @{ 'RestSupTerm $L1 $T1 $L2 $T2 }.
+   for @{ 'SupTerm $L1 $T1 $L2 $T2 }.
 
 notation "hvbox( L ⊢ break ⌘ ⦃ term 46 T ⦄ ≡ break term 46 k )"
    non associative with precedence 45
    for @{ 'ICM $L $T $k }.
 
-notation "hvbox( L ⊢ break term 46 T1 break ▶ [ term 46 d , break term 46 e ] break term 46 T2 )"
-   non associative with precedence 45
-   for @{ 'PSubst $L $T1 $d $e $T2 }.
-
 (* Unfold *******************************************************************)
 
 notation "hvbox( @ ⦃ term 46 T1 , break term 46 f ⦄ ≡ break term 46 T2 )"
@@ -192,33 +188,21 @@ notation "hvbox( ⇩ * [ term 46 e ] break term 46 L1 ≡ break term 46 L2 )"
    non associative with precedence 45
    for @{ 'RDropStar $e $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 @{ 'RestSupTermPlus $L1 $T1 $L2 $T2 }.
-
-notation "hvbox( ⦃ term 46 L1, break term 46 T1 ⦄ ⧁ * break ⦃ term 46 L2 , break term 46 T2 ⦄ )"
-   non associative with precedence 45
-   for @{ 'RestSupTermStar $L1 $T1 $L2 $T2 }.
-
-notation "hvbox( T1 break ▶ * [ term 46 d , break term 46 e ] break term 46 T2 )"
-   non associative with precedence 45
-   for @{ 'PSubstStar $T1 $d $e $T2 }.
-
-notation "hvbox( L ⊢ break term 46 T1 break ▶ * [ term 46 d , break term 46 e ] break term 46 T2 )"
+notation "hvbox( ⦃ term 46 L1, break term 46 T1 ⦄ ⊃ + break ⦃ term 46 L2 , break term 46 T2 ⦄ )"
    non associative with precedence 45
-   for @{ 'PSubstStar $L $T1 $d $e $T2 }.
+   for @{ 'SupTermPlus $L1 $T1 $L2 $T2 }.
 
-notation "hvbox( L ⊢ break term 46 T1 break ▶ ▶ * [ term 46 d , break term 46 e ] break term 46 T2 )"
+notation "hvbox( ⦃ term 46 L1, break term 46 T1 ⦄ ⊃ * break ⦃ term 46 L2 , break term 46 T2 ⦄ )"
    non associative with precedence 45
-   for @{ 'PSubstStarAlt $L $T1 $d $e $T2 }.
+   for @{ 'SupTermStar $L1 $T1 $L2 $T2 }.
 
-notation "hvbox( T1 break ⊢ ▶ * [ term 46 d , break term 46 e ] break term 46 T2 )"
+notation "hvbox( L ⊢ break term 46 T1 ▶* break term 46 T2 )"
    non associative with precedence 45
-   for @{ 'PSubstStarSn $T1 $d $e $T2 }.
+   for @{ 'PSubstStar $L $T1 $T2 }.
 
-notation "hvbox( T1 break ⊢ ▶ ▶ * [ term 46 d , break term 46 e ] break term 46 T2 )"
+notation "hvbox( T1 ⊢ ▶ * break term 46 T2 )"
    non associative with precedence 45
-   for @{ 'PSubstStarSnAlt $T1 $d $e $T2 }.
+   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
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_cpr.ma
index 039dc29e0..d231c849f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_cpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_cpr.ma
@@ -57,7 +57,7 @@ theorem cpr_conf: ∀L,U0,T1,T2. L ⊢ U0 ➡ T1 → L ⊢ U0 ➡ T2 →
                   ∃∃T. L ⊢ T1 ➡ T & L ⊢ T2 ➡ T.
 #L #U0 #T1 #T2 * #U1 #HU01 #HUT1 * #U2 #HU02 #HUT2
 elim (tpr_conf … HU01 HU02) -U0 #U #HU1 #HU2
-elim (tpr_tpss_ltpr ? L … HU1 … HUT1) -U1 // #U1 #HTU1 #HU1
-elim (tpr_tpss_ltpr ? L … HU2 … HUT2) -U2 // #U2 #HTU2 #HU2
+elim (ltpr_tpr_tpss_conf ? L … HU1 … HUT1) -U1 // #U1 #HTU1 #HU1
+elim (ltpr_tpr_tpss_conf ? L … HU2 … HUT2) -U2 // #U2 #HTU2 #HU2
 elim (tpss_conf_eq … HU1 … HU2) -U /3 width=5/
 qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_lift.ma
index 5206f43ce..0a7afddab 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_lift.ma
@@ -75,9 +75,9 @@ elim (tpr_inv_abbr1 … H1) -H1 *
 [ #V #T #T0 #HV1 #HT1 #HT0 #H destruct
   elim (tpss_inv_bind1 … H2) -H2 #V2 #T2 #HV2 #HT02 #H destruct
   lapply (tps_lsubr_trans … HT0 (L. ⓓV) ?) -HT0 /2 width=1/ #HT0
-  lapply (tps_weak_all … HT0) -HT0 #HT0
+  lapply (tps_weak_full … HT0) -HT0 #HT0
   lapply (tpss_lsubr_trans … HT02 (L. ⓓV) ?) -HT02 /2 width=1/ #HT02
-  lapply (tpss_weak_all … HT02) -HT02 #HT02
+  lapply (tpss_weak_full … HT02) -HT02 #HT02
   lapply (tpss_strap2 … HT0 HT02) -T0 /4 width=7/
 | #T2 #HT12 #HXT2 #H destruct
   elim (lift_total Y 0 1) #Z #HYZ
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_ltpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_ltpr.ma
index d3e75f8c0..ab10e3fc6 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_ltpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_ltpr.ma
@@ -12,20 +12,20 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/reducibility/tpr_tpss.ma".
+include "basic_2/reducibility/ltpr_tpss.ma".
 include "basic_2/reducibility/cpr.ma".
 
 (* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************)
 
 (* Properties concerning parallel unfold on terms ***************************)
 
-(* Note: we could invoke tpss_weak_all instead of ltpr_fwd_length *)
+(* Note: we could invoke tpss_weak_full instead of ltpr_fwd_length *)
 (* Basic_1: was only: pr2_subst1 *)
 lemma cpr_tpss_ltpr: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. L2 ⊢ T1 ➡ T2 →
                      ∀d,e,U1. L1 ⊢ T1 ▶* [d, e] U1 →
                      ∃∃U2. L2 ⊢ U1 ➡ U2 & L2 ⊢ T2 ▶* [d, e] U2.
 #L1 #L2 #HL12 #T1 #T2 * #T #HT1 #HT2 #d #e #U1 #HTU1
-elim (tpr_tpss_ltpr … HL12 … HT1 … HTU1) -L1 -HT1 #U #HU1 #HTU
+elim (ltpr_tpr_tpss_conf … HL12 … HT1 … HTU1) -L1 -HT1 #U #HU1 #HTU
 elim (tpss_conf_eq … HT2 … HTU) -T /3 width=3/
 qed.
 
@@ -33,7 +33,7 @@ lemma cpr_ltpr_conf_eq: ∀L1,T1,T2. L1 ⊢ T1 ➡ T2 → ∀L2. L1 ➡ L2 →
                         ∃∃T. L2 ⊢ T1 ➡ T & T2 ➡ T.
 #L1 #T1 #T2 * #T #HT1 #HT2 #L2 #HL12
 >(ltpr_fwd_length … HL12) in HT2; #HT2
-elim (tpr_tpss_ltpr … HL12 … HT2) -L1 /3 width=3/
+elim (ltpr_tpr_tpss_conf … HL12 … HT2) -L1 /3 width=3/
 qed.
 
 lemma cpr_ltpr_conf_tpss: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. L1 ⊢ T1 ➡ T2 →
@@ -42,5 +42,5 @@ lemma cpr_ltpr_conf_tpss: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. L1 ⊢ T1 ➡ T2 →
 #L1 #L2 #HL12 #T1 #T2 #HT12 #d #e #U1 #HTU1
 elim (cpr_ltpr_conf_eq … HT12 … HL12) -HT12 #T #HT1 #HT2
 elim (cpr_tpss_ltpr … HL12 … HT1 … HTU1) -L1 -HT1 #U2 #HU12 #HTU2
-lapply (tpss_weak_all … HTU2) -HTU2 #HTU2 /3 width=5/ (**) (* /4 width=5/ is too slow *)
+lapply (tpss_weak_full … HTU2) -HTU2 #HTU2 /3 width=5/ (**) (* /4 width=5/ is too slow *)
 qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_ltpss_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_ltpss_sn.ma
index 49ec47f77..f946e4cfb 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_ltpss_sn.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_ltpss_sn.ma
@@ -22,7 +22,7 @@ include "basic_2/reducibility/cpr.ma".
 lemma ltpss_sn_cpr_trans: ∀L1,L2,d,e. L1 ⊢ ▶* [d, e] L2 →
                           ∀T1,T2. L2 ⊢ T1 ➡ T2 → L1 ⊢ T1 ➡ T2.
 #L1 #L2 #d #e #HL12 #T1 #T2 *
-lapply (ltpss_sn_weak_all … HL12)
+lapply (ltpss_sn_weak_full … HL12)
 <(ltpss_sn_fwd_length … HL12) -HL12 /3 width=5/
 qed.
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_tpss.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_tpss.ma
index fc4f2b8c5..d8c7225d9 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_tpss.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_tpss.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/reducibility/tpr_tpss.ma".
+include "basic_2/reducibility/ltpr_tpss.ma".
 include "basic_2/reducibility/cpr.ma".
 
 (* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************)
@@ -22,7 +22,7 @@ include "basic_2/reducibility/cpr.ma".
 lemma cpr_tpss_trans: ∀L,T1,T. L ⊢ T1 ➡ T →
                       ∀T2,d,e. L ⊢ T ▶* [d, e] T2 → L ⊢ T1 ➡ T2.
 #L #T1 #T * #T0 #HT10 #HT0 #T2 #d #e #HT2
-lapply (tpss_weak_all … HT2) -HT2 #HT2
+lapply (tpss_weak_full … HT2) -HT2 #HT2
 lapply (tpss_trans_eq … HT0 HT2) -T /2 width=3/
 qed.
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/fpr_cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/fpr_cpr.ma
index 007681d0b..baa630f5b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/fpr_cpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/fpr_cpr.ma
@@ -36,7 +36,7 @@ elim (le_or_ge (|K|) d) #Hd
 [ elim (ldrop_ltpss_sn_trans_ge … HLK … HK2 …)
 | elim (ldrop_ltpss_sn_trans_be … HLK … HK2 …)
 ] // -Hd #L2 #HL2 #HLK2
-lapply (ltpss_sn_weak_all … HL2) -K /3 width=4/
+lapply (ltpss_sn_weak_full … HL2) -K /3 width=4/
 qed-.
 
 (* Advanced properties ******************************************************)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_cpr.ma
index 04686f960..8a01f263a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_cpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_cpr.ma
@@ -13,6 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/unfold/ltpss_sn_ltpss_sn.ma".
+include "basic_2/reducibility/ltpr_ldrop.ma".
 include "basic_2/reducibility/cpr.ma".
 include "basic_2/reducibility/lfpr.ma".
 
@@ -27,3 +28,25 @@ lemma lfpr_pair_cpr: ∀L1,L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀V1,V2. L2 ⊢ V1 ➡
 lapply (ltpss_sn_tpss_trans_eq … HV2 … HL2) -HV2 #V2
 @(ex2_intro … (L.ⓑ{I}V)) /2 width=1/ (**) (* explicit constructor *)
 qed.
+
+(* Properties on supclosure *************************************************)
+(*
+lamma fsub_cpr_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 #HT12 #U2 * #T #H1 #H2
+elim (fsub_tpr_trans … HT12 … H1) -T2 #L #U #HL1 #HT1U #HUT
+elim (fsup_tpss_trans_full … HUT … H2) -T  -HUT -H2 #L #U #HL1 #HT1U #HUT
+
+
+
+
+
+
+ #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 #HK2
+elim (lift_total T d e) #U #HTU
+elim (ldrop_ltpr_trans … HLK1 … HK1) -HLK1 -HK1 #L #HL1 #HLK
+lapply (tpr_lift … HT1 … HTU1 … HTU) -HT1 -HTU1 /3 width=11/
+qed-.
+*)
\ No newline at end of file
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_ldrop.ma
index 945279795..02404a11d 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_ldrop.ma
@@ -13,11 +13,14 @@
 (**************************************************************************)
 
 include "basic_2/substitution/ldrop_lpx.ma".
+include "basic_2/substitution/fsup.ma".
 include "basic_2/reducibility/tpr_lift.ma".
 include "basic_2/reducibility/ltpr.ma".
 
 (* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************)
 
+(* Properies on local environment slicing ***********************************)
+
 (* Basic_1: was: wcpr0_drop *)
 lemma ltpr_ldrop_conf: dropable_sn ltpr.
 /3 width=3 by lpx_deliftable_dropable, tpr_inv_lift1/ qed.
@@ -28,3 +31,15 @@ lemma ldrop_ltpr_trans: dedropable_sn ltpr.
 
 lemma ltpr_ldrop_trans_O1: dropable_dx ltpr.
 /2 width=3/ qed.
+
+(* Properties on supclosure *************************************************)
+
+lemma fsub_tpr_trans: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ∀U2. T2 ➡ U2 →
+                      ∃∃L,U1. L1 ➡ 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 #HK2
+elim (lift_total T d e) #U #HTU
+elim (ldrop_ltpr_trans … HLK1 … HK1) -HLK1 -HK1 #L #HL1 #HLK
+lapply (tpr_lift … HT1 … HTU1 … HTU) -HT1 -HTU1 /3 width=11/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_ltpss_dx.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_ltpss_dx.ma
index cee1cb49e..00730b732 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_ltpss_dx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_ltpss_dx.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/reducibility/tpr_tpss.ma".
+include "basic_2/reducibility/ltpr_tpss.ma".
 
 (* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************)
 
@@ -27,10 +27,10 @@ lemma ltpr_ltpss_dx_conf: ∀L1,K1,d,e. L1 ▶* [d, e] K1 → ∀L2. L1 ➡ L2 
 | #L1 #K1 #I #V1 #W1 #e #_ #HVW1 #IHLK1 #X #H
   elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct
   elim (IHLK1 … HL12) -L1 #K2 #HLK2 #HK12
-  elim (tpr_tpss_ltpr … HK12 … HV12 … HVW1) -V1 /3 width=5/
+  elim (ltpr_tpr_tpss_conf … HK12 … HV12 … HVW1) -V1 /3 width=5/
 | #L1 #K1 #I #V1 #W1 #d #e #_ #HVW1 #IHLK1 #X #H
   elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct
   elim (IHLK1 … HL12) -L1 #K2 #HLK2 #HK12
-  elim (tpr_tpss_ltpr … HK12 … HV12 … HVW1) -V1 /3 width=5/
+  elim (ltpr_tpr_tpss_conf … HK12 … HV12 … HVW1) -V1 /3 width=5/
 ]
 qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_tps.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_tps.ma
index 75792eef0..7f08be62b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_tps.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_tps.ma
@@ -18,24 +18,7 @@ include "basic_2/reducibility/ltpr_ldrop.ma".
 
 (* Properties concerning parallel substitution on terms *********************)
 
-lemma ltpr_tps_trans: ∀L2,T1,T2,d,e. L2 ⊢ T1 ▶ [d, e] T2 → ∀L1. L1 ➡ L2 →
-                      ∃∃T. L1 ⊢ T1 ▶ [d, e] T & T ➡ T2.
-#L2 #T1 #T2 #d #e #H elim H -L2 -T1 -T2 -d -e
-[ /2 width=3/
-| #L2 #K2 #V2 #W2 #i #d #e #Hdi #Hide #HLK2 #HVW2 #L1 #HL12
-  elim (ltpr_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H
-  elim (ltpr_inv_pair2 … H) -H #K1 #V1 #HK12 #HV12 #H destruct -K2
-  elim (lift_total V1 0 (i+1)) #W1 #HVW1
-  lapply (tpr_lift … HV12 … HVW1 … HVW2) -V2 /3 width=4/
-| #L2 #a #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #L1 #HL12
-  elim (IHV12 … HL12) -IHV12 #V #HV1 #HV2
-  elim (IHT12 (L1.ⓑ{I}V) ?) /2 width=1/ -L2 /3 width=5/
-| #L2 #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #L1 #HL12
-  elim (IHV12 … HL12) -IHV12
-  elim (IHT12 … HL12) -L2 /3 width=5/
-]
-qed.
-
+(* Basic_1: was: pr0_subst1_fwd *)
 lemma ltpr_tps_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶ [d, e] T2 → ∀L2. L1 ➡ L2 →
                      ∃∃T. L2 ⊢ T1 ▶ [d, e] T & T2 ➡ T.
 #L1 #T1 #T2 #d #e #H elim H -L1 -T1 -T2 -d -e
@@ -52,4 +35,23 @@ lemma ltpr_tps_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶ [d, e] T2 → ∀L2. L1 ➡
   elim (IHV12 … HL12) -IHV12
   elim (IHT12 … HL12) -L1 /3 width=5/
 ]
-qed.
+qed-.
+
+(* Basic_1: was: pr0_subst1_back *)
+lemma ltpr_tps_trans: ∀L2,T1,T2,d,e. L2 ⊢ T1 ▶ [d, e] T2 → ∀L1. L1 ➡ L2 →
+                      ∃∃T. L1 ⊢ T1 ▶ [d, e] T & T ➡ T2.
+#L2 #T1 #T2 #d #e #H elim H -L2 -T1 -T2 -d -e
+[ /2 width=3/
+| #L2 #K2 #V2 #W2 #i #d #e #Hdi #Hide #HLK2 #HVW2 #L1 #HL12
+  elim (ltpr_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H
+  elim (ltpr_inv_pair2 … H) -H #K1 #V1 #HK12 #HV12 #H destruct -K2
+  elim (lift_total V1 0 (i+1)) #W1 #HVW1
+  lapply (tpr_lift … HV12 … HVW1 … HVW2) -V2 /3 width=4/
+| #L2 #a #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #L1 #HL12
+  elim (IHV12 … HL12) -IHV12 #V #HV1 #HV2
+  elim (IHT12 (L1.ⓑ{I}V) ?) /2 width=1/ -L2 /3 width=5/
+| #L2 #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #L1 #HL12
+  elim (IHV12 … HL12) -IHV12
+  elim (IHT12 … HL12) -L2 /3 width=5/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpss.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_tpss.ma
similarity index 78%
rename from matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpss.ma
rename to matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_tpss.ma
index 597fe64eb..71586fa36 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpss.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_tpss.ma
@@ -13,20 +13,20 @@
 (**************************************************************************)
 
 include "basic_2/unfold/ltpss_dx_ltpss_dx.ma".
-include "basic_2/reducibility/tpr_tps.ma".
+include "basic_2/reducibility/ltpr_tps.ma".
 
-(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
+(* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************)
 
-(* Unfold properties ********************************************************)
+(* Properties on partial unfold for terms ***********************************)
 
 (* Basic_1: was: pr0_subst1 *)
-lemma tpr_tps_ltpr: ∀T1,T2. T1 ➡ T2 →
-                    ∀L1,d,e,U1. L1 ⊢ T1 ▶ [d, e] U1 →
-                    ∀L2. L1 ➡ L2 →
-                    ∃∃U2. U1 ➡ U2 & L2 ⊢ T2 ▶* [d, e] U2.
+lemma ltpr_tpr_tps_conf: ∀T1,T2. T1 ➡ T2 →
+                         ∀L1,d,e,U1. L1 ⊢ T1 ▶ [d, e] U1 →
+                         ∀L2. L1 ➡ L2 →
+                         ∃∃U2. U1 ➡ U2 & L2 ⊢ T2 ▶* [d, e] U2.
 #T1 #T2 #H elim H -T1 -T2
 [ #I #L1 #d #e #U1 #H #L2 #HL12
-  elim (ltpr_tpr_conf … H … HL12) -L1 /3 width=3/
+  elim (ltpr_tps_conf … H … HL12) -L1 /3 width=3/
 | #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12
   elim (tps_inv_flat1 … H) -H #W1 #U1 #HVW1 #HTU1 #H destruct
   elim (IHV12 … HVW1 … HL12) -V1
@@ -64,28 +64,28 @@ lemma tpr_tps_ltpr: ∀T1,T2. T1 ➡ T2 →
   elim (tps_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct
   elim (IHT12 … HTT1 … HL12) -T1 -HL12 /3 width=3/
 ]
-qed.
+qed-.
 
-lemma tpr_tps_bind: ∀I,V1,V2,T1,T2,U1. V1 ➡ V2 → T1 ➡ T2 →
-                    ⋆. ⓑ{I} V1 ⊢ T1 ▶ [0, 1] U1 →
-                    ∃∃U2. U1 ➡ U2 & ⋆. ⓑ{I} V2 ⊢ T2 ▶ [0, 1] U2.
+lemma tpr_tps_conf_bind: ∀I,V1,V2,T1,T2,U1. V1 ➡ V2 → T1 ➡ T2 →
+                         ⋆. ⓑ{I} V1 ⊢ T1 ▶ [0, 1] U1 →
+                         ∃∃U2. U1 ➡ U2 & ⋆. ⓑ{I} V2 ⊢ T2 ▶ [0, 1] U2.
 #I #V1 #V2 #T1 #T2 #U1 #HV12 #HT12 #HTU1
-elim (tpr_tps_ltpr … HT12 … HTU1 (⋆. ⓑ{I} V2) ?) -T1 /2 width=1/ -V1 #U2 #HU12 #HTU2
+elim (ltpr_tpr_tps_conf … HT12 … HTU1 (⋆. ⓑ{I} V2) ?) -T1 /2 width=1/ -V1 #U2 #HU12 #HTU2
 lapply (tpss_inv_SO2 … HTU2) -HTU2 /2 width=3/
-qed.
+qed-.
 
-lemma tpr_tpss_ltpr: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. T1 ➡ T2 →
-                     ∀d,e,U1. L1 ⊢ T1 ▶* [d, e] U1 →
-                     ∃∃U2. U1 ➡ U2 & L2 ⊢ T2 ▶* [d, e] U2.
+lemma ltpr_tpr_tpss_conf: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. T1 ➡ T2 →
+                          ∀d,e,U1. L1 ⊢ T1 ▶* [d, e] U1 →
+                          ∃∃U2. U1 ➡ U2 & L2 ⊢ T2 ▶* [d, e] U2.
 #L1 #L2 #HL12 #T1 #T2 #HT12 #d #e #U1 #HTU1 @(tpss_ind … HTU1) -U1
 [ /2 width=3/
 | -HT12 #U #U1 #_ #HU1 * #T #HUT #HT2
-  elim (tpr_tps_ltpr … HUT … HU1 … HL12) -U -HL12 #U2 #HU12 #HTU2
+  elim (ltpr_tpr_tps_conf … HUT … HU1 … HL12) -U -HL12 #U2 #HU12 #HTU2
   lapply (tpss_trans_eq … HT2 … HTU2) -T /2 width=3/
 ]
-qed.
+qed-.
 
 lemma tpr_tpss_conf: ∀T1,T2. T1 ➡ T2 →
                      ∀L,U1,d,e. L ⊢ T1 ▶* [d, e] U1 →
                      ∃∃U2. U1 ➡ U2 & L ⊢ T2 ▶* [d, e] U2.
-/2 width=5/ qed.
+/2 width=5 by ltpr_tpr_tpss_conf/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_delift.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_delift.ma
index 8e91abc6a..3fff8f25f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_delift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_delift.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/unfold/delift.ma".
-include "basic_2/reducibility/tpr_tpss.ma".
+include "basic_2/reducibility/ltpr_tpss.ma".
 
 (* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
 
@@ -24,4 +24,4 @@ lemma tpr_delift_conf: ∀U1,U2. U1 ➡ U2 → ∀L,T1,d,e. L ⊢ ▼*[d, e] U1
 #U1 #U2 #HU12 #L #T1 #d #e * #W1 #HUW1 #HTW1
 elim (tpr_tpss_conf … HU12 … HUW1) -U1 #U1 #HWU1 #HU21
 elim (tpr_inv_lift1 … HWU1 … HTW1) -W1 /3 width=5/
-qed.
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpr.ma
index c12f38cf4..a733345bf 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpr.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/reducibility/tpr_tpss.ma".
+include "basic_2/reducibility/ltpr_tpss.ma".
 
 (* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
 
@@ -71,7 +71,7 @@ elim (tpr_inv_abbr1 … H) -H *
 [ -HV2 -HVV2 #WW2 #UU2 #UU #HWW2 #HUU02 #HUU2 #H destruct
   elim (IH … HW02 … HWW2) -HW02 -HWW2 /2 width=1/ #W #HW02 #HWW2
   elim (IH … HU02 … HUU02) -HU02 -HUU02 -IH /2 width=1/ #U #HU2 #HUUU2
-  elim (tpr_tps_bind … HWW2 HUUU2 … HUU2) -UU2 #UUU #HUUU2 #HUUU1
+  elim (tpr_tps_conf_bind … HWW2 HUUU2 … HUU2) -UU2 #UUU #HUUU2 #HUUU1
   @ex2_intro
   [2: @tpr_theta [6: @HVV |7: @HWW2 |8: @HUUU2 |1,2,3,4: skip | // ]
   |1:skip
@@ -124,8 +124,8 @@ fact tpr_conf_delta_delta:
 #a #I1 #V0 #V1 #T0 #T1 #TT1 #V2 #T2 #TT2 #IH #HV01 #HV02 #HT01 #HT02 #HTT1 #HTT2
 elim (IH … HV01 … HV02) -HV01 -HV02 // #V #HV1 #HV2
 elim (IH … HT01 … HT02) -HT01 -HT02 -IH // #T #HT1 #HT2
-elim (tpr_tps_bind … HV1 HT1 … HTT1) -T1 #U1 #TTU1 #HTU1
-elim (tpr_tps_bind … HV2 HT2 … HTT2) -T2 #U2 #TTU2 #HTU2
+elim (tpr_tps_conf_bind … HV1 HT1 … HTT1) -T1 #U1 #TTU1 #HTU1
+elim (tpr_tps_conf_bind … HV2 HT2 … HTT2) -T2 #U2 #TTU2 #HTU2
 elim (tps_conf_eq … HTU1 … HTU2) -T #U #HU1 #HU2
 @ex2_intro [2,3: @tpr_delta |1: skip ] /width=10/ (**) (* /3 width=10/ is too slow *)
 qed.
@@ -141,7 +141,7 @@ fact tpr_conf_delta_zeta:
    ∃∃X. +ⓓV1. TT1 ➡ X & X2 ➡ X.
 #X2 #V0 #V1 #T0 #T1 #TT1 #T2 #IH #_ #HT01 #HTT1 #HT02 #HXT2
 elim (IH … HT01 … HT02) -IH -HT01 -HT02 // -V0 -T0 #T #HT1 #HT2
-elim (tpr_tps_bind ? ? V1 … HT1 HTT1) -T1 // #TT #HTT1 #HTT
+elim (tpr_tps_conf_bind ? ? V1 … HT1 HTT1) -T1 // #TT #HTT1 #HTT
 elim (tpr_inv_lift1 … HT2 … HXT2) -T2 #X #HXT #HX2
 lapply (tps_inv_lift1_eq … HTT … HXT) -HTT #H destruct /3 width=3/
 qed.
@@ -258,4 +258,4 @@ theorem tpr_conf: ∀T0:term. ∀T1,T2. T0 ➡ T1 → T0 ➡ T2 →
     ]
   ]
 ]
-qed.
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tps.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tps.ma
deleted file mode 100644
index 12cf13c0f..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tps.ma
+++ /dev/null
@@ -1,57 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/reducibility/ltpr_ldrop.ma".
-
-(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
-
-(* Properties on parallel substitution for terms ****************************)
-
-(* Basic_1: was: pr0_subst1_fwd *)
-lemma ltpr_tpr_conf: ∀L1,T,U1,d,e. L1 ⊢ T ▶ [d, e] U1 → ∀L2. L1 ➡ L2 →
-                     ∃∃U2. U1 ➡ U2 & L2 ⊢ T ▶ [d, e] U2.
-#L1 #T #U1 #d #e #H elim H -L1 -T -U1 -d -e
-[ /2 width=3/
-| #L1 #K1 #V1 #W1 #i #d #e #Hdi #Hide #HLK1 #HVW1 #L2 #HL12
-  elim (ltpr_ldrop_conf … HLK1 … HL12) -L1 #X #H #HLK2
-  elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct -K1
-  elim (lift_total V2 0 (i+1)) #W2 #HVW2
-  lapply (tpr_lift … HV12 … HVW1 … HVW2) -V1 /3 width=6/
-| #L1 #a #I #V #W1 #T #U1 #d #e #_ #_ #IHV #IHT #L2 #HL12
-  elim (IHV … HL12) -IHV #W2 #HW12
-  elim (IHT (L2.ⓑ{I}W2) ?) -IHT /2 width=1/ -L1 /3 width=5/
-| #L1 #I #V #W1 #T #U1 #d #e #_ #_ #IHV #IHT #L2 #HL12
-  elim (IHV … HL12) -IHV
-  elim (IHT … HL12) -IHT -HL12 /3 width=5/
-]
-qed.
-
-(* Basic_1: was: pr0_subst1_back *)
-lemma ltpr_tps_trans: ∀L2,T,U2,d,e. L2 ⊢ T ▶ [d, e] U2 → ∀L1. L1 ➡ L2 →
-                      ∃∃U1. U1 ➡ U2 & L1 ⊢ T ▶ [d, e] U1.
-#L2 #T #U2 #d #e #H elim H -L2 -T -U2 -d -e
-[ /2 width=3/
-| #L2 #K2 #V2 #W2 #i #d #e #Hdi #Hide #HLK2 #HVW2 #L1 #HL12
-  elim (ltpr_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H
-  elim (ltpr_inv_pair2 … H) -H #K1 #V1 #HK12 #HV12 #H destruct -K2
-  elim (lift_total V1 0 (i+1)) #W1 #HVW1
-  lapply (tpr_lift … HV12 … HVW1 … HVW2) -V2 /3 width=6/
-| #L2 #a #I #V #W2 #T #U2 #d #e #_ #_ #IHV #IHT #L1 #HL12
-  elim (IHV … HL12) -IHV #W1 #HW12
-  elim (IHT (L1.ⓑ{I}W1) ?) -IHT /2 width=1/ -L2 /3 width=5/
-| #L2 #I #V #W2 #T #U2 #d #e #_ #_ #IHV #IHT #L1 #HL12
-  elim (IHV … HL12) -IHV
-  elim (IHT … HL12) -IHT -HL12 /3 width=5/
-]
-qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/xpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/xpr.ma
new file mode 100644
index 000000000..4efbd3545
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/xpr.ma
@@ -0,0 +1,66 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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".
+include "basic_2/reducibility/cpr.ma".
+
+lemma arith1: ∀x,y,z,w. z < y → x + (y + w) - z = x + y - z + w.
+#x #y #z #w #H <le_plus_minus_comm // /3 width=1 by lt_to_le, le_plus_a/
+qed-.
+
+(* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************)
+
+notation "hvbox( ⦃term 46 h, break term 46 L⦄ ⊢ break term 46 T1 ➡ break [ term 46 g ] break term 46 T2 )"
+   non associative with precedence 45
+   for @{ 'XPRed $h $g $L $T1 $T2 }.
+
+inductive xpr (h) (g): lenv → relation term ≝
+| xpr_cpr : ∀I,L,U2. L ⊢ ⓪{I} ➡ U2 → xpr h g L (⓪{I}) U2
+| xpr_ssta: ∀I,L,U2,l. ⦃h, L⦄ ⊢ ⓪{I} •[g] ⦃l+1, U2⦄ → xpr h g L (⓪{I}) U2
+| xpr_bind: ∀a,I,L,V1,V2,T1,T2,U2. xpr h g L V1 V2 → xpr h g (L.ⓑ{I}V2) T1 T2 →
+            L ⊢ ⓑ{a,I}V2.T2 ➡ U2 → xpr h g L (ⓑ{a,I}V1.T1) U2
+| xpr_flat: ∀I,L,V1,V2,T1,T2,U2. xpr h g L V1 V2 → xpr h g L T1 T2 →
+            L ⊢ ⓕ{I}V2.T2 ➡ U2 → xpr h g L (ⓕ{I}V1.T1) U2
+.
+
+interpretation
+   "context-sensitive extended parallel reduction (term)"
+   'XPRed h g L T1 T2 = (xpr h g L T1 T2).
+
+(* Basic properties *********************************************************)
+
+(* Note: this is "∀h,g,L. reflexive … (xpr h g L)" *)
+lemma xpr_refl: ∀h,g,T,L. ⦃h, L⦄ ⊢ T ➡[g] T.
+#h #g #T elim T -T /2 width=1/ * /2 width=5/
+qed.
+
+lemma cpr_xpr: ∀h,g,T1,L,T2. L ⊢ T1 ➡ T2 → ⦃h, L⦄ ⊢ T1 ➡[g] T2.
+#h #g #T1 elim T1 -T1 /2 width=1/ * /2 width=5/
+qed.
+
+lemma ssta_xpr: ∀h,g,T1,L,T2,l. ⦃h, L⦄ ⊢ T1 •[g] ⦃l+1, T2⦄ → ⦃h, L⦄ ⊢ T1 ➡[g] T2.
+#h #g #T1 elim T1 -T1 /2 width=2/ * [|*]
+[ #a #I #V1 #T1 #_ #IHT1 #L #X #l #H
+  elim (ssta_inv_bind1 … H) -H #T2 #HT12 #H destruct /3 width=5/
+| #V1 #T1 #_ #IHT1 #L #X #l #H
+  elim (ssta_inv_appl1 … H) -H #T2 #HT12 #H destruct /3 width=5/
+| #V1 #T1 #_ #IHT1 #L #X #l #H
+  lapply (ssta_inv_cast1 … H) -H /3 width=5/
+]
+qed.
+
+include "basic_2/substitution/lift_lift.ma".
+include "basic_2/substitution/fsup.ma".
+include "basic_2/unfold/ltpss_dx_ldrop.ma".
+
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ssta.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ssta.ma
index d7a32e928..4f0300f00 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/ssta.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/ssta.ma
@@ -13,7 +13,6 @@
 (**************************************************************************)
 
 include "basic_2/substitution/ldrop.ma".
-include "basic_2/unfold/frsups.ma".
 include "basic_2/static/sd.ma".
 
 (* STRATIFIED STATIC TYPE ASSIGNMENT ON TERMS *******************************)
@@ -146,55 +145,3 @@ qed.
 lemma ssta_inv_cast1: ∀h,g,L,X,Y,U,l. ⦃h, L⦄ ⊢ ⓝY.X •[g] ⦃l, U⦄ →
                       ⦃h, L⦄ ⊢ X •[g] ⦃l, U⦄.
 /2 width=4/ qed-.
-
-(* Advanced inversion lemmas ************************************************)
-
-lemma ssta_inv_frsupp: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g] ⦃l, U⦄ → ⦃L, U⦄ ⧁+ ⦃L, T⦄ → ⊥.
-#h #g #L #T #U #l #H elim H -L -T -U -l
-[ #L #k #l #_ #H
-  elim (frsupp_inv_atom1_frsups … H)
-| #L #K #V #W #U #i #l #_ #_ #HWU #_ #H
-  elim (lift_frsupp_trans … (⋆) … H … HWU) -U #X #H
-  elim (lift_inv_lref2_be … H ? ?) -H //
-| #L #K #W #V #U #i #l #_ #_ #HWU #_ #H
-  elim (lift_frsupp_trans … (⋆) … H … HWU) -U #X #H
-  elim (lift_inv_lref2_be … H ? ?) -H //
-| #a #I #L #V #T #U #l #_ #IHTU #H
-  elim (frsupp_inv_bind1_frsups … H) -H #H [2: /4 width=4/ ] -IHTU
-  lapply (frsups_fwd_fw … H) -H normalize
-  <associative_plus <associative_plus #H
-  elim (le_plus_xySz_x_false … H)
-| #L #V #T #U #l #_ #IHTU #H
-  elim (frsupp_inv_flat1_frsups … H) -H #H [2: /4 width=4/ ] -IHTU
-  lapply (frsups_fwd_fw … H) -H normalize
-  <associative_plus <associative_plus #H
-  elim (le_plus_xySz_x_false … H)
-| /3 width=4/
-]
-qed-.
-
-fact ssta_inv_refl_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g] ⦃l, U⦄ → T = U → ⊥.
-#h #g #L #T #U #l #H elim H -L -T -U -l
-[ #L #k #l #_ #H
-  lapply (next_lt h k) destruct -H -e0 (**) (* destruct: these premises are not erased *)
-  <e1 -e1 #H elim (lt_refl_false … H)
-| #L #K #V #W #U #i #l #_ #_ #HWU #_ #H destruct
-  elim (lift_inv_lref2_be … HWU ? ?) -HWU //
-| #L #K #W #V #U #i #l #_ #_ #HWU #_ #H destruct
-  elim (lift_inv_lref2_be … HWU ? ?) -HWU //
-| #a #I #L #V #T #U #l #_ #IHTU #H destruct /2 width=1/
-| #L #V #T #U #l #_ #IHTU #H destruct /2 width=1/
-| #L #W #T #U #l #HTU #_ #H destruct
-  elim (ssta_inv_frsupp … HTU ?) -HTU /2 width=1/
-]
-qed-.
-
-lemma ssta_inv_refl: ∀h,g,T,L,l. ⦃h, L⦄ ⊢ T •[g] ⦃l, T⦄ → ⊥.
-/2 width=8 by ssta_inv_refl_aux/ qed-.
-
-lemma ssta_inv_frsups: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g] ⦃l, U⦄ → ⦃L, U⦄ ⧁* ⦃L, T⦄ → ⊥.
-#h #g #L #T #U #L #HTU #H elim (frsups_inv_all … H) -H
-[ * #_ #H destruct /2 width=6 by ssta_inv_refl/
-| /2 width=8 by ssta_inv_frsupp/
-]
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_ssta.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_ssta.ma
index adaf999ee..617ef508f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_ssta.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_ssta.ma
@@ -12,8 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/substitution/ldrop_ldrop.ma".
-include "basic_2/static/ssta.ma".
+include "basic_2/static/ssta_lift.ma".
 
 (* STRATIFIED STATIC TYPE ASSIGNMENT ON TERMS *******************************)
 
@@ -47,3 +46,12 @@ theorem ssta_mono: ∀h,g,L,T,U1,l1. ⦃h, L⦄ ⊢ T •[g] ⦃l1, U1⦄ →
   elim (IHTU1 … HTU2) -T /2 width=1/
 ]
 qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma ssta_inv_refl_pos: ∀h,g,L,T,l. ⦃h, L⦄ ⊢ T •[g] ⦃l+1, T⦄ → ⊥.
+#h #g #L #T #l #HTT
+elim (ssta_fwd_correct … HTT) <minus_plus_m_m #U #HTU
+elim (ssta_mono … HTU … HTT) -h -L #H #_ -T -U
+elim (plus_xySz_x_false 0 l 0 ?) //
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fsup.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fsup.ma
new file mode 100644
index 000000000..c8e78d9a9
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fsup.ma
@@ -0,0 +1,70 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/substitution/ldrop.ma".
+
+(* SUPCLOSURE ***************************************************************)
+
+inductive fsup: bi_relation lenv term ≝
+| fsup_lref   : ∀I,L,V. fsup (L.ⓑ{I}V) (#0) L V
+| fsup_bind_sn: ∀a,I,L,V,T. fsup L (ⓑ{a,I}V.T) L V
+| fsup_bind_dx: ∀a,I,L,V,T. fsup L (ⓑ{a,I}V.T) (L.ⓑ{I}V) T
+| fsup_flat_sn: ∀I,L,V,T.   fsup L (ⓕ{I}V.T) L V
+| fsup_flat_dx: ∀I,L,V,T.   fsup L (ⓕ{I}V.T) L T
+| fsup_ldrop  : ∀L1,K1,K2,T1,T2,U1,d,e.
+                ⇩[d, e] L1 ≡ K1 → ⇧[d, e] T1 ≡ U1 →
+                fsup K1 T1 K2 T2 → fsup L1 U1 K2 T2
+.
+
+interpretation
+   "structural successor (closure)"
+   'SupTerm L1 T1 L2 T2 = (fsup L1 T1 L2 T2).
+
+(* Basic properties *********************************************************)
+
+lemma fsup_lref_S_lt: ∀I,L,K,V,T,i. 0 < i → ⦃L, #(i-1)⦄ ⊃ ⦃K, T⦄ → ⦃L.ⓑ{I}V, #i⦄ ⊃ ⦃K, T⦄.
+/3 width=7/ qed.
+
+lemma fsup_lref: ∀I,K,V,i,L. ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃L, #i⦄ ⊃ ⦃K, V⦄.
+#I #K #V #i @(nat_elim1 i) -i #i #IH #L #H
+elim (ldrop_inv_O1_pair2 … H) -H *
+[ #H1 #H2 destruct //
+| #I1 #K1 #V1 #HK1 #H #Hi destruct
+  lapply (IH … HK1) /2 width=1/
+]
+qed.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma fsup_fwd_cw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ♯{L2, T2} < ♯{L1, T1}.
+#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 //
+#L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12
+lapply (ldrop_fwd_lw … HLK1) -HLK1 #HLK1
+lapply (lift_fwd_tw … HTU1) -HTU1 #HTU1
+@(lt_to_le_to_lt … IHT12) -IHT12 /2 width=1/
+qed-.
+
+fact fsup_fwd_length_lref1_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ∀i. T1 = #i → |L2| < |L1|.
+#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2
+[ 6: #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #i #H destruct
+     lapply (ldrop_fwd_length … HLK1) -HLK1 #HLK1
+     elim (lift_inv_lref2 … HTU1) -HTU1 * #Hdei #H destruct
+     @(lt_to_le_to_lt … HLK1) /2 width=2/
+| normalize // |2,3: #a
+] #I #L #V #T #j #H destruct
+qed-.
+
+lemma fsup_fwd_length_lref1: ∀L1,L2,T2,i. ⦃L1, #i⦄ ⊃ ⦃L2, T2⦄ → |L2| < |L1|.
+/2 width=5 by fsup_fwd_length_lref1_aux/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop.ma
index f1bc18f7d..8782fa93d 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop.ma
@@ -131,6 +131,19 @@ lemma ldrop_inv_skip1: ∀d,e,I,K1,V1,L2. ⇩[d, e] K1. ⓑ{I} V1 ≡ L2 → 0 <
                                 L2 = K2. ⓑ{I} V2.
 /2 width=3/ qed-.
 
+lemma ldrop_inv_O1_pair2: ∀I,K,V,e,L1. ⇩[0, e] L1 ≡ K. ⓑ{I} V →
+                          (e = 0 ∧ L1 = K. ⓑ{I} V) ∨
+                          ∃∃I1,K1,V1. ⇩[0, e - 1] K1 ≡ K. ⓑ{I} V & L1 = K1.ⓑ{I1}V1 & 0 < e.
+#I #K #V #e *
+[ #H lapply (ldrop_inv_atom1 … H) -H #H destruct
+| #L1 #I1 #V1 #H
+  elim (ldrop_inv_O1 … H) -H *
+  [ #H1 #H2 destruct /3 width=1/
+  | /3 width=5/
+  ]
+]
+qed-.
+
 fact ldrop_inv_skip2_aux: ∀d,e,L1,L2. ⇩[d, e] L1 ≡ L2 → 0 < d →
                           ∀I,K2,V2. L2 = K2. ⓑ{I} V2 →
                           ∃∃K1,V1. ⇩[d - 1, e] K1 ≡ K2 &
@@ -258,11 +271,15 @@ lemma ldrop_fwd_ldrop2: ∀L1,I2,K2,V2,e. ⇩[O, e] L1 ≡ K2. ⓑ{I2} V2 →
 ]
 qed-.
 
+lemma ldrop_fwd_length: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → |L2| ≤ |L1|.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e // normalize /2 width=1/
+qed-.
+
 lemma ldrop_fwd_lw: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → ♯{L2} ≤ ♯{L1}.
 #L1 #L2 #d #e #H elim H -L1 -L2 -d -e // normalize
 [ /2 width=3/
 | #L1 #L2 #I #V1 #V2 #d #e #_ #HV21 #IHL12
-  >(tw_lift … HV21) -HV21 /2 width=1/
+  >(lift_fwd_tw … HV21) -HV21 /2 width=1/
 ]
 qed-.
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_lpx.ma
index 2605b921c..f972cb2b2 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_lpx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_lpx.ma
@@ -62,7 +62,7 @@ fact lpx_dropable_aux: ∀R,L2,K2,d,e. ⇩[d, e] L2 ≡ K2 → ∀L1. lpx R L1 L
 | #L2 #K2 #I #V2 #W2 #d #e #_ #_ #_ #L1 #_
   >commutative_plus normalize #H destruct
 ]
-qed.
+qed-.
 
-lemma ltpr_dropable: ∀R. dropable_dx (lpx R).
-/2 width=5/ qed.
+lemma ltpx_dropable: ∀R. dropable_dx (lpx R).
+/2 width=5 by lpx_dropable_aux/ qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lift.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lift.ma
index 84babbdc8..7e7961eab 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lift.ma
@@ -276,7 +276,7 @@ qed-.
 
 (* Basic forward lemmas *****************************************************)
 
-lemma tw_lift: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → ♯{T1} = ♯{T2}.
+lemma lift_fwd_tw: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → ♯{T1} = ♯{T2}.
 #d #e #T1 #T2 #H elim H -d -e -T1 -T2 normalize //
 qed-.
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma
index af450e34d..7d89243d5 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma
@@ -12,6 +12,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
+notation "hvbox( L ⊢ break term 46 T1 break ▶ [ term 46 d , break term 46 e ] break term 46 T2 )"
+   non associative with precedence 45
+   for @{ 'PSubst $L $T1 $d $e $T2 }.
+
 include "basic_2/substitution/ldrop_append.ma".
 
 (* PARALLEL SUBSTITUTION ON TERMS *******************************************)
@@ -91,8 +95,8 @@ lemma tps_weak_top: ∀L,T1,T2,d,e.
 ]
 qed.
 
-lemma tps_weak_all: ∀L,T1,T2,d,e.
-                    L ⊢ T1 ▶ [d, e] T2 → L ⊢ T1 ▶ [0, |L|] T2.
+lemma tps_weak_full: ∀L,T1,T2,d,e.
+                     L ⊢ T1 ▶ [d, e] T2 → L ⊢ T1 ▶ [0, |L|] T2.
 #L #T1 #T2 #d #e #HT12
 lapply (tps_weak … HT12 0 (d + e) ? ?) -HT12 // #HT12
 lapply (tps_weak_top … HT12) //
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/cpss.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/cpss.ma
new file mode 100644
index 000000000..fa8f4fb4e
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/cpss.ma
@@ -0,0 +1,183 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/substitution/ldrop_append.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL UNFOLD FOR TERMS ******************************)
+
+inductive cpss: lenv → relation term ≝
+| cpss_atom : ∀L,I. cpss L (⓪{I}) (⓪{I})
+| cpss_subst: ∀L,K,V,V2,W2,i.
+              ⇩[0, i] L ≡ K. ⓓV → cpss K V V2 →
+              ⇧[0, i + 1] V2 ≡ W2 → cpss L (#i) W2
+| cpss_bind : ∀L,a,I,V1,V2,T1,T2.
+              cpss L V1 V2 → cpss (L. ⓑ{I} V1) T1 T2 →
+              cpss L (ⓑ{a,I} V1. T1) (ⓑ{a,I} V2. T2)
+| cpss_flat : ∀L,I,V1,V2,T1,T2.
+              cpss L V1 V2 → cpss L T1 T2 →
+              cpss L (ⓕ{I} V1. T1) (ⓕ{I} V2. T2)
+.
+
+interpretation "context-sensitive parallel unfold (term)"
+   'PSubstStar L T1 T2 = (cpss L T1 T2).
+
+(* Basic properties *********************************************************)
+
+(* Note: it does not hold replacing |L1| with |L2| *)
+lemma cpss_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/
+| /3 width=1/
+]
+qed-.
+
+lemma cpss_refl: ∀T,L. L ⊢ T ▶* T.
+#T elim T -T //
+#I elim I -I /2 width=1/
+qed.
+
+lemma cpss_delift: ∀K,V,T1,L,d. ⇩[0, d] L ≡ (K. ⓓV) →
+                   ∃∃T2,T. L ⊢ T1 ▶* T2 & ⇧[d, 1] T ≡ T2.
+#K #V #T1 elim T1 -T1
+[ * #i #L #d #HLK /2 width=4/
+  elim (lt_or_eq_or_gt i d) #Hid /3 width=4/
+  destruct
+  elim (lift_total V 0 (i+1)) #W #HVW
+  elim (lift_split … HVW i i ? ? ?) // /3 width=6/
+| * [ #a ] #I #W1 #U1 #IHW1 #IHU1 #L #d #HLK
+  elim (IHW1 … HLK) -IHW1 #W2 #W #HW12 #HW2
+  [ elim (IHU1 (L. ⓑ{I} W1) (d+1) ?) -IHU1 /2 width=1/ -HLK /3 width=9/
+  | elim (IHU1 … HLK) -IHU1 -HLK /3 width=8/
+  ]
+]
+qed-.
+
+lemma cpss_append: ∀K,T1,T2. K ⊢ T1 ▶* T2 → ∀L. L @@ K ⊢ T1 ▶* T2.
+#K #T1 #T2 #H elim H -K -T1 -T2 // /2 width=1/
+#K #K0 #V1 #V2 #W2 #i #HK0 #_ #HVW2 #IHV12 #L
+lapply (ldrop_fwd_ldrop2_length … HK0) #H
+@(cpss_subst … (L@@K0) V1 … HVW2) //
+@(ldrop_O1_append_sn_le … HK0) /2 width=2/ (**) (* /3/ does not work *)
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact cpss_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
+[ #L #I #J #H destruct /2 width=1/
+| #L #K #V #V2 #T2 #i #HLK #HV2 #HVT2 #I #H destruct /3 width=8/
+| #L #a #I #V1 #V2 #T1 #T2 #_ #_ #J #H destruct
+| #L #I #V1 #V2 #T1 #T2 #_ #_ #J #H destruct
+]
+qed-.
+
+lemma cpss_inv_atom1: ∀L,T2,I. 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 cpss_inv_atom1_aux/ qed-.
+
+lemma cpss_inv_sort1: ∀L,T2,k. L ⊢ ⋆k ▶* T2 → T2 = ⋆k.
+#L #T2 #k #H
+elim (cpss_inv_atom1 … H) -H //
+* #K #V #V2 #i #_ #_ #_ #H destruct
+qed-.
+
+lemma cpss_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 (cpss_inv_atom1 … H) -H /2 width=1/
+* #K #V #V2 #j #HLK #HV2 #HVT2 #H destruct /3 width=6/
+qed-.
+
+lemma cpss_inv_gref1: ∀L,T2,p. L ⊢ §p ▶* T2 → T2 = §p.
+#L #T2 #p #H
+elim (cpss_inv_atom1 … H) -H //
+* #K #V #V2 #i #_ #_ #_ #H destruct
+qed-.
+
+fact cpss_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.
+#L #U1 #U2 * -L -U1 -U2
+[ #L #k #a #I #V1 #T1 #H destruct
+| #L #K #V #V2 #W2 #i #_ #_ #_ #a #I #V1 #T1 #H destruct
+| #L #b #J #V1 #V2 #T1 #T2 #HV12 #HT12 #a #I #V #T #H destruct /2 width=5/
+| #L #J #V1 #V2 #T1 #T2 #_ #_ #a #I #V #T #H destruct
+]
+qed-.
+
+lemma cpss_inv_bind1: ∀L,a,I,V1,T1,U2. L ⊢ ⓑ{a,I} V1. T1 ▶* U2 →
+                      ∃∃V2,T2. L ⊢ V1 ▶* V2 &
+                               L. ⓑ{I} V1 ⊢ T1 ▶* T2 &
+                               U2 = ⓑ{a,I} V2. T2.
+/2 width=3 by cpss_inv_bind1_aux/ qed-.
+
+fact cpss_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 #U1 #U2 * -L -U1 -U2
+[ #L #k #I #V1 #T1 #H destruct
+| #L #K #V #V2 #W2 #i #_ #_ #_ #I #V1 #T1 #H destruct
+| #L #a #J #V1 #V2 #T1 #T2 #_ #_ #I #V #T #H destruct
+| #L #J #V1 #V2 #T1 #T2 #HV12 #HT12 #I #V #T #H destruct /2 width=5/
+]
+qed-.
+
+lemma cpss_inv_flat1: ∀L,I,V1,T1,U2. L ⊢ ⓕ{I} V1. T1 ▶* U2 →
+                      ∃∃V2,T2. L ⊢ V1 ▶* V2 & L ⊢ T1 ▶* T2 &
+                               U2 =  ⓕ{I} V2. T2.
+/2 width=3 by cpss_inv_flat1_aux/ qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma cpss_fwd_tw: ∀L,T1,T2. L ⊢ T1 ▶* T2 → ♯{T1} ≤ ♯{T2}.
+#L #T1 #T2 #H elim H -L -T1 -T2 normalize
+/3 by monotonic_le_plus_l, le_plus/ (**) (* just /3 width=1/ is too slow *)
+qed-.
+
+lemma cpss_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 (cpss_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 *)
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/cpss_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/cpss_lift.ma
new file mode 100644
index 000000000..616ea63c7
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/cpss_lift.ma
@@ -0,0 +1,69 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/substitution/ldrop_ldrop.ma".
+include "basic_2/unfold/cpss.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL UNFOLD FOR TERMS ******************************)
+
+(* Relocation properties ****************************************************)
+
+lemma cpss_lift: l_liftable cpss.
+#K #T1 #T2 #H elim H -K -T1 -T2
+[ #K #I #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/
+  ]
+| #K #a #I #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/
+| #K #I #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/
+]
+qed.
+
+lemma cpss_inv_lift1: l_deliftable_sn cpss.
+#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/
+  ]
+| #L #a #I #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/
+| #L #I #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/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/delift.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/delift.ma
index 95284abc7..3cd3241bc 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/delift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/delift.ma
@@ -104,5 +104,5 @@ qed-.
 
 lemma delift_fwd_tw: ∀L,T1,T2,d,e. L ⊢ ▼*[d, e] T1 ≡ T2 → ♯{T1} ≤ ♯{T2}.
 #L #T1 #T2 #d #e * #T #HT1 #HT2
->(tw_lift … HT2) -T2 /2 width=4 by tpss_fwd_tw/
+>(lift_fwd_tw … HT2) -T2 /2 width=4 by tpss_fwd_tw/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/fsupp.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/fsupp.ma
new file mode 100644
index 000000000..f0fde0f1f
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/fsupp.ma
@@ -0,0 +1,60 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/fsup.ma".
+
+(* PLUS-ITERATED SUPCLOSURE *************************************************)
+
+definition fsupp: bi_relation lenv term ≝ bi_TC … fsup.
+
+interpretation "plus-iterated structural successor (closure)"
+   'SupTermPlus L1 T1 L2 T2 = (fsupp L1 T1 L2 T2).
+
+(* Basic eliminators ********************************************************)
+
+lemma fsupp_ind: ∀L1,T1. ∀R:relation2 lenv term.
+                 (∀L2,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → R L2 T2) →
+                 (∀L,T,L2,T2. ⦃L1, T1⦄ ⊃+ ⦃L, T⦄ → ⦃L, T⦄ ⊃ ⦃L2, T2⦄ → R L T → R L2 T2) →
+                 ∀L2,T2. ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄ → R L2 T2.
+#L1 #T1 #R #IH1 #IH2 #L2 #T2 #H
+@(bi_TC_ind … IH1 IH2 ? ? H)
+qed-.
+
+lemma fsupp_ind_dx: ∀L2,T2. ∀R:relation2 lenv term.
+                    (∀L1,T1. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → R L1 T1) →
+                    (∀L1,L,T1,T. ⦃L1, T1⦄ ⊃ ⦃L, T⦄ → ⦃L, T⦄ ⊃+ ⦃L2, T2⦄ → R L T → R L1 T1) →
+                    ∀L1,T1. ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄ → R L1 T1.
+#L2 #T2 #R #IH1 #IH2 #L1 #T1 #H
+@(bi_TC_ind_dx … IH1 IH2 ? ? H)
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma fsup_fsupp: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄.
+/2 width=1/ qed.
+
+lemma fsupp_strap1: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⊃+ ⦃L, T⦄ → ⦃L, T⦄ ⊃ ⦃L2, T2⦄ →
+                    ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄.
+/2 width=4/ qed.
+
+lemma fsupp_strap2: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⊃ ⦃L, T⦄ → ⦃L, T⦄ ⊃+ ⦃L2, T2⦄ →
+                    ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄.
+/2 width=4/ qed.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma fsupp_fwd_cw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄ → ♯{L2, T2} < ♯{L1, T1}.
+#L1 #L2 #T1 #T2 #H @(fsupp_ind … H) -L2 -T2
+/3 width=3 by fsup_fwd_cw, transitive_lt/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csupp_csupp.etc b/matita/matita/contribs/lambdadelta/basic_2/unfold/fsupp_fsupp.ma
similarity index 93%
rename from matita/matita/contribs/lambdadelta/basic_2/etc/csup/csupp_csupp.etc
rename to matita/matita/contribs/lambdadelta/basic_2/unfold/fsupp_fsupp.ma
index 5afdb68d4..a546fc265 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csupp_csupp.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/fsupp_fsupp.ma
@@ -12,11 +12,11 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/unfold/csupp.ma".
+include "basic_2/unfold/fsupp.ma".
 
 (* PLUS-ITERATED SUPCLOSURE *************************************************)
 
 (* Main propertis ***********************************************************)
 
-theorem csupp_trans: bi_transitive … csupp.
+theorem fsupp_trans: bi_transitive … fsupp.
 /2 width=4/ qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lcpss.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lcpss.ma
new file mode 100644
index 000000000..3570a2d80
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/lcpss.ma
@@ -0,0 +1,89 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/cpss.ma".
+
+(* SN PARALLEL UNFOLD FOR LOCAL ENVIRONMENTS ********************************)
+
+inductive lcpss: relation lenv ≝
+| lcpss_atom: lcpss (⋆) (⋆)
+| lcpss_pair: ∀I,L1,L2,V1,V2. lcpss L1 L2 → L1 ⊢ V1 ▶* V2 →
+              lcpss (L1. ⓑ{I} V1) (L2. ⓑ{I} V2)
+.
+
+interpretation "parallel unfold (local environment, sn variant)"
+   'PSubstStarSn L1 L2 = (lcpss L1 L2).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact lcpss_inv_atom1_aux: ∀L1,L2. L1 ⊢ ▶* L2 → L1 = ⋆ → L2 = ⋆.
+#L1 #L2 * -L1 -L2
+[ //
+| #I #L1 #L2 #V1 #V2 #_ #_ #H destruct
+]
+qed-.
+
+lemma lcpss_inv_atom1: ∀L2. ⋆ ⊢ ▶* L2 → L2 = ⋆.
+/2 width=5 by lcpss_inv_atom1_aux/ qed-.
+
+fact lcpss_inv_pair1_aux: ∀L1,L2. L1 ⊢ ▶* L2 → ∀I,K1,V1. L1 = K1. ⓑ{I} V1 →
+                          ∃∃K2,V2. K1 ⊢ ▶* K2 & K1 ⊢ V1 ▶* V2 & L2 = K2. ⓑ{I} V2.
+#L1 #L2 * -L1 -L2
+[ #I #K1 #V1 #H destruct
+| #I #L1 #L2 #V1 #V2 #HL12 #HV12 #J #K1 #W1 #H destruct /2 width=5/
+]
+qed-.
+
+lemma lcpss_inv_pair1: ∀I,K1,V1,L2. K1. ⓑ{I} V1 ⊢ ▶* L2 →
+                       ∃∃K2,V2. K1 ⊢ ▶* K2 & K1 ⊢ V1 ▶* V2 & L2 = K2. ⓑ{I} V2.
+/2 width=5 by lcpss_inv_pair1_aux/ qed-.
+
+fact lcpss_inv_atom2_aux: ∀L1,L2. L1 ⊢ ▶* L2 → L2 = ⋆ → L1 = ⋆.
+#L1 #L2 * -L1 -L2
+[ //
+| #I #L1 #L2 #V1 #V2 #_ #_ #H destruct
+]
+qed-.
+
+lemma lcpss_inv_atom2: ∀L1. L1 ⊢ ▶* ⋆ → L1 = ⋆.
+/2 width=5 by lcpss_inv_atom2_aux/ qed-.
+
+fact lcpss_inv_pair2_aux: ∀L1,L2. L1 ⊢ ▶* L2 → ∀I,K2,V2. L2 = K2. ⓑ{I} V2 →
+                          ∃∃K1,V1. K1 ⊢ ▶* K2 & K1 ⊢ V1 ▶* V2 & L1 = K1. ⓑ{I} V1.
+#L1 #L2 * -L1 -L2
+[ #I #K1 #V1 #H destruct
+| #I #L1 #L2 #V1 #V2 #HL12 #HV12 #J #K2 #W2 #H destruct /2 width=5/
+]
+qed-.
+
+lemma lcpss_inv_pair2: ∀I,L1,K2,V2. L1 ⊢ ▶* K2. ⓑ{I} V2 →
+                       ∃∃K1,V1. K1 ⊢ ▶* K2 & K1 ⊢ V1 ▶* V2 & L1 = K1. ⓑ{I} V1.
+/2 width=5 by lcpss_inv_pair2_aux/ qed-.
+
+(* Basic properties *********************************************************)
+
+lemma lcpss_refl: ∀L. L ⊢ ▶* L.
+#L elim L -L // /2 width=1/
+qed.
+
+lemma lcpss_append: ∀K1,K2. K1 ⊢ ▶* K2 → ∀L1,L2. L1 ⊢ ▶* L2 →
+                    L1 @@ K1 ⊢ ▶* L2 @@ K2.
+#K1 #K2 #H elim H -K1 -K2 // /3 width=1/
+qed.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lcpss_fwd_length: ∀L1,L2. L1 ⊢ ▶* L2 → |L1| = |L2|.
+#L1 #L2 #H elim H -L1 -L2 normalize //
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lcpss_cpss.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lcpss_cpss.ma
new file mode 100644
index 000000000..aee1d7fcb
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/lcpss_cpss.ma
@@ -0,0 +1,145 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/fsup.ma".
+include "basic_2/unfold/lcpss_ldrop.ma".
+
+(* SN PARALLEL UNFOLD FOR LOCAL ENVIRONMENTS ********************************)
+
+(* Main properties on context-sensitive parallel unfold for terms ***********)
+
+fact cpss_conf_lcpss_aux: ∀L0,i. (
+                             ∀L,T0.♯{L, T0} < ♯{L0, #i} →
+                             ∀T1. L ⊢ T0 ▶* T1 → ∀T2. L ⊢ T0 ▶* T2 →
+                             ∀L1. L ⊢ ▶* L1 → ∀L2. L ⊢ ▶* L2 →
+                             ∃∃T. L1 ⊢ T1 ▶* T & L2 ⊢ T2 ▶* T
+                          ) →
+                          ∀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 (lcpss_ldrop_conf … HLK0 … HL01) -HL01 #X1 #H1 #HLK1
+elim (lcpss_inv_pair1 … H1) -H1 #K1 #V1 #HK01 #HV01 #H destruct
+elim (lcpss_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2
+elim (lcpss_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 (cpss_lift … HV2 … HLK2 … HVT2 … HVT) -K2 -V2 /3 width=6/
+qed-.
+
+theorem cpss_conf_lcpss: ∀L0,T0,T1. L0 ⊢ T0 ▶* T1 → ∀T2. L0 ⊢ T0 ▶* T2 →
+                         ∀L1. L0 ⊢ ▶* L1 → ∀L2. L0 ⊢ ▶* L2 →
+                         ∃∃T. L1 ⊢ T1 ▶* T & L2 ⊢ T2 ▶* T.
+#L0 #T0 @(f2_ind … fw … L0 T0) -L0 -T0 #n #IH #L0 * [|*]
+[ #I0 #Hn #T1 #H1 #T2 #H2 #L1 #HL01 #L2 #HL02 destruct
+  elim (cpss_inv_atom1 … H1) -H1
+  elim (cpss_inv_atom1 … H2) -H2
+  [ #H2 #H1 destruct /2 width=3/
+  | * #K0 #V0 #V2 #i2 #HLK0 #HV02 #HVT2 #H2 #H1 destruct
+    /3 width=10 by cpss_conf_lcpss_aux/
+  | #H2 * #K0 #V0 #V1 #i1 #HLK0 #HV01 #HVT1 #H1 destruct
+    /4 width=10 by ex2_commute, cpss_conf_lcpss_aux/
+  | * #X #Y #V2 #z #H #HV02 #HVT2 #H2
+    * #K0 #V0 #V1 #i #HLK0 #HV01 #HVT1 #H1 destruct
+    lapply (ldrop_mono … H … HLK0) -H #H destruct
+    elim (lcpss_ldrop_conf … HLK0 … HL01) -HL01 #X1 #H1 #HLK1
+    elim (lcpss_inv_pair1 … H1) -H1 #K1 #W1 #HK01 #_ #H destruct
+    lapply (ldrop_fwd_ldrop2 … HLK1) -W1 #HLK1
+    elim (lcpss_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2
+    elim (lcpss_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 (cpss_lift … HV1 … HLK1 … HVT1 … HVT) -K1 -V1
+    lapply (cpss_lift … HV2 … HLK2 … HVT2 … HVT) -K2 -V2 -V /2 width=3/
+  ]
+| #a #I #V0 #T0 #Hn #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct
+  elim (cpss_inv_bind1 … H1) -H1 #V1 #T1 #HV01 #HT01 #H destruct
+  elim (cpss_inv_bind1 … H2) -H2 #V2 #T2 #HV02 #HT02 #H destruct
+  elim (IH … HV01 … HV02 … HL01 … HL02) //
+  elim (IH … HT01 … HT02 (L1.ⓑ{I}V1) … (L2.ⓑ{I}V2)) -IH // /2 width=1/ /3 width=5/
+| #I #V0 #T0 #Hn #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct
+  elim (cpss_inv_flat1 … H1) -H1 #V1 #T1 #HV01 #HT01 #H destruct
+  elim (cpss_inv_flat1 … H2) -H2 #V2 #T2 #HV02 #HT02 #H destruct
+  elim (IH … HV01 … HV02 … HL01 … HL02) //
+  elim (IH … HT01 … HT02 … HL01 … HL02) // /3 width=5/
+]
+qed-.
+
+theorem cpss_conf: ∀L. confluent … (cpss L).
+/2 width=6 by cpss_conf_lcpss/ qed-.
+
+theorem cpss_trans_lcpss: ∀L1,T1,T. L1 ⊢ T1 ▶* T → ∀L2. L1 ⊢ ▶* L2 →
+                          ∀T2. L2 ⊢ T ▶* T2 → L1 ⊢ T1 ▶* T2.
+#L1 #T1 @(f2_ind … fw … L1 T1) -L1 -T1 #n #IH #L1 * [|*]
+[ #I #Hn #T #H1 #L2 #HL12 #T2 #HT2 destruct
+  elim (cpss_inv_atom1 … H1) -H1
+  [ #H destruct
+    elim (cpss_inv_atom1 … HT2) -HT2
+    [ #H destruct //
+    | * #K2 #V #V2 #i #HLK2 #HV2 #HVT2 #H destruct
+      elim (lcpss_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H
+      elim (lcpss_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 (lcpss_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2
+    elim (lcpss_inv_pair1 … H) -H #K2 #W2 #HK12 #_ #H destruct
+    lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2
+    elim (cpss_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 (cpss_inv_bind1 … H1) -H1 #V #T #HV1 #HT1 #H destruct
+  elim (cpss_inv_bind1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H destruct /4 width=5/
+| #I #V1 #T1 #Hn #X1 #H1 #L2 #HL12 #X2 #H2
+  elim (cpss_inv_flat1 … H1) -H1 #V #T #HV1 #HT1 #H destruct
+  elim (cpss_inv_flat1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H destruct /3 width=5/
+]
+qed-.
+
+theorem cpss_trans: ∀L. Transitive … (cpss L).
+/2 width=5 by cpss_trans_lcpss/ qed-.
+
+(* Properties on context-sensitive parallel unfold for terms ****************)
+
+lemma lcpss_cpss_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 (cpss_conf_lcpss … HT01 T0 … HL01 … HL01) // -L0 /2 width=3/
+qed-.
+
+lemma lcpss_cpss_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 (cpss_conf_lcpss … HT01 T0 … L0 … HL01) // -HT01 -HL01 /2 width=3/
+qed-.
+
+lemma lcpss_cpss_trans: ∀L1,L2. L1 ⊢ ▶* L2 →
+                        ∀T1,T2. L2 ⊢ T1 ▶* T2 → L1 ⊢ T1 ▶* T2.
+/2 width=5 by cpss_trans_lcpss/ qed-.
+
+lemma fsup_cpss_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_lcpss_trans … HLK1 … HK1) -HLK1 -HK1 #L2 #HL12 #HL2K
+lapply (cpss_lift … HT1 … HL2K … HTU1 … HTU) -HT1 -HTU1 /3 width=11/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lcpss_lcpss.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lcpss_lcpss.ma
new file mode 100644
index 000000000..5397ca3a4
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/lcpss_lcpss.ma
@@ -0,0 +1,55 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/unfold/lcpss_cpss.ma".
+
+(* SN PARALLEL UNFOLD ON LOCAL ENVIRONMENTS *********************************)
+
+(* Main properties **********************************************************)
+
+theorem lcpss_conf: confluent … lcpss.
+#L0 @(f_ind … length … L0) -L0 #n #IH *
+[ #_ #X1 #H1 #X2 #H2 -n
+  >(lcpss_inv_atom1 … H1) -X1
+  >(lcpss_inv_atom1 … H2) -X2 /2 width=3/
+| #L0 #I #V0 #Hn #X1 #H1 #X2 #H2 destruct
+  elim (lcpss_inv_pair1 … H1) -H1 #L1 #V1 #HL01 #HV01 #H destruct
+  elim (lcpss_inv_pair1 … H2) -H2 #L2 #V2 #HL02 #HV02 #H destruct
+  elim (IH … HL01 … HL02) -IH normalize // #L #HL1 #HL2
+  elim (cpss_conf_lcpss … HV01 … HV02 … HL01 … HL02) -L0 -V0 /3 width=5/
+]
+qed-.
+
+theorem lcpss_trans: Transitive … lcpss.
+#L1 #L #H elim H -L1 -L //
+#I #L1 #L #V1 #V #HL1 #HV1 #IHL1 #X #H
+elim (lcpss_inv_pair1 … H) -H #L2 #V2 #HL2 #HV2 #H destruct
+lapply (cpss_trans_lcpss … HV1 … HL1 … HV2) -V -HL1 /3 width=1/
+qed-.
+
+(* Advanced forward lemmas **************************************************)
+
+lemma cpss_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 (cpss_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
+  elim (IH … HT12) -IH -HT12 #L2 #T #HL12 #HT1 #H destruct
+  lapply (lcpss_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 *)
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lcpss_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lcpss_ldrop.ma
new file mode 100644
index 000000000..0c3b8c48f
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/lcpss_ldrop.ma
@@ -0,0 +1,69 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/cpss_lift.ma".
+include "basic_2/unfold/lcpss.ma".
+
+(* SN PARALLEL UNFOLD FOR LOCAL ENVIRONMENTS ********************************)
+
+(* Properies on local environment slicing ***********************************)
+
+lemma lcpss_ldrop_conf: dropable_sn lcpss.
+#L1 #K1 #d #e #H elim H -L1 -K1 -d -e
+[ #d #e #X #H
+  lapply (lcpss_inv_atom1 … H) -H #H destruct /2 width=3/
+| #L1 #I #V1 #X #H
+  elim (lcpss_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct /3 width=3/
+| #L1 #K1 #I #V1 #e #_ #IHLK1 #X #H
+  elim (lcpss_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct
+  elim (IHLK1 … HL12) -IHLK1 -HL12 /3 width=3/
+| #L1 #K1 #I #V1 #W1 #d #e #HLK1 #HWV1 #IHLK1 #X #H
+  elim (lcpss_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct
+  elim (cpss_inv_lift1 … HV12 … HLK1 … HWV1) -HLK1 -V1
+  elim (IHLK1 … HL12) -IHLK1 -HL12 /3 width=5/
+]
+qed-.
+
+lemma ldrop_lcpss_trans: dedropable_sn lcpss.
+#L1 #K1 #d #e #H elim H -L1 -K1 -d -e
+[ #d #e #X #H
+  lapply (lcpss_inv_atom1 … H) -H #H destruct /2 width=3/
+| #L1 #I #V1 #X #H
+  elim (lcpss_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct /3 width=3/
+| #L1 #K1 #I #V1 #e #_ #IHLK1 #K2 #HK12
+  elim (IHLK1 … HK12) -IHLK1 -HK12 /3 width=5/
+| #L1 #K1 #I #V1 #W1 #d #e #HLK1 #HWV1 #IHLK1 #X #H
+  elim (lcpss_inv_pair1 … H) -H #L2 #W2 #HL12 #HW12 #H destruct
+  elim (lift_total W2 d e) #V2 #HWV2
+  lapply (cpss_lift … HW12 … HLK1 … HWV1 … HWV2) -W1 -HLK1
+  elim (IHLK1 … HL12) -IHLK1 -HL12 /3 width=5/
+]
+qed-.
+
+fact lcpss_ldrop_trans_O1_aux: ∀L2,K2,d,e. ⇩[d, e] L2 ≡ K2 → ∀L1. L1 ⊢ ▶* L2 →
+                               d = 0 → ∃∃K1. ⇩[0, e] L1 ≡ K1 & K1 ⊢ ▶* K2.
+#L2 #K2 #d #e #H elim H -L2 -K2 -d -e
+[ #d #e #X #H >(lcpss_inv_atom2 … H) -H /2 width=3/
+| #K2 #I #V2 #X #H
+  elim (lcpss_inv_pair2 … H) -H #K1 #V1 #HK12 #HV12 #H destruct /3 width=5/
+| #L2 #K2 #I #V2 #e #_ #IHLK2 #X #H #_
+  elim (lcpss_inv_pair2 … H) -H #L1 #V1 #HL12 #HV12 #H destruct
+  elim (IHLK2 … HL12 ?) -L2 // /3 width=3/
+| #L2 #K2 #I #V2 #W2 #d #e #_ #_ #_ #L1 #_
+  >commutative_plus normalize #H destruct
+]
+qed-.
+
+lemma lcpss_ldrop_trans_O1: dropable_dx lcpss.
+/2 width=5 by lcpss_ldrop_trans_O1_aux/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx.ma
index 1beef1bb7..753c948cc 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx.ma
@@ -12,6 +12,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
+notation "hvbox( T1 break ▶ * [ term 46 d , break term 46 e ] break term 46 T2 )"
+   non associative with precedence 45
+   for @{ 'PSubstStar $T1 $d $e $T2 }.
+
 include "basic_2/unfold/tpss.ma".
 
 (* DX PARALLEL UNFOLD ON LOCAL ENVIRONMENTS *********************************)
@@ -208,7 +212,7 @@ lemma ltpss_dx_weak: ∀L1,L2,d1,e1. L1 ▶* [d1, e1] L2 →
 ]
 qed.
 
-lemma ltpss_dx_weak_all: ∀L1,L2,d,e. L1 ▶* [d, e] L2 → L1 ▶* [0, |L2|] L2.
+lemma ltpss_dx_weak_full: ∀L1,L2,d,e. L1 ▶* [d, e] L2 → L1 ▶* [0, |L2|] L2.
 #L1 #L2 #d #e #H elim H -L1 -L2 -d -e
 // /3 width=2/ /3 width=3/
 qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_ldrop.ma
index 4aa2f573e..0b6c504c2 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_ldrop.ma
@@ -12,10 +12,14 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basic_2/substitution/fsup.ma".
+include "basic_2/unfold/tpss_lift.ma".
 include "basic_2/unfold/ltpss_dx.ma".
 
 (* DX PARALLEL UNFOLD ON LOCAL ENVIRONMENTS *********************************)
 
+(* Properies on local environment slicing ***********************************)
+
 lemma ltpss_dx_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 ▶* [d1, e1] L1 →
                               ∀L2,e2. ⇩[0, e2] L0 ≡ L2 →
                               d1 + e1 ≤ e2 → ⇩[0, e2] L1 ≡ L2.
@@ -129,3 +133,98 @@ lemma ltpss_dx_ldrop_trans_le: ∀L1,L0,d1,e1. L1 ▶* [d1, e1] L0 →
   ]
 ]
 qed.
+
+lemma ldrop_ltpss_dx_trans_le: ∀L1,K1,d1,e1. ⇩[d1, e1] L1 ≡ K1 →
+                               ∀K2,d2,e2. K1 ▶* [d2, e2] K2 → d1 ≤ d2 →
+                               ∃∃L2. L1 ▶* [d2 + e1, e2] L2 & ⇩[d1, e1] L2 ≡ K2.
+#L1 #K1 #d1 #e1 #H elim H -L1 -K1 -d1 -e1
+[ #d1 #e1 #K2 #d2 #e2 #H #_
+  >(ltpss_dx_inv_atom1 … H) -H /2 width=3/
+| /2 width=3/
+| #L1 #K1 #I #V #e1 #_ #IHLK1 #K2 #d2 #e2 #HK12 #Hd
+  elim (IHLK1 … HK12 Hd) -K1 -Hd /3 width=5/
+| #L1 #K1 #I #V1 #W1 #d1 #e1 #_ #HWV1 #IHLK1 #X #d2 #e2 #H #Hd12
+  elim (le_inv_plus_l … Hd12) -Hd12 #Hd12 #Hd2
+  elim (ltpss_dx_inv_tpss11 … H Hd2) -H #K2 #W2 #HK12 #HW12 #H destruct
+  elim (IHLK1 … HK12 … Hd12) -IHLK1 -HK12 <le_plus_minus_comm // #L2 #HL12 #HLK2
+  elim (lift_total W2 d1 e1) #V2 #HWV2
+  lapply (tpss_lift_ge … HW12 … HLK2 HWV1 … HWV2) -W1 // -Hd12
+  <le_plus_minus_comm // /4 width=5/
+]
+qed-.
+
+lemma ldrop_ltpss_dx_trans_be: ∀L1,K1,d1,e1. ⇩[d1, e1] L1 ≡ K1 →
+                               ∀K2,d2,e2. K1 ▶* [d2, e2] K2 →
+                               d2 ≤ d1 → d1 ≤ d2 + e2 →
+                               ∃∃L2. L1 ▶* [d2, e1 + e2] L2 &
+                                     ⇩[d1, e1] L2 ≡ K2.
+#L1 #K1 #d1 #e1 #H elim H -L1 -K1 -d1 -e1
+[ #d1 #e1 #K2 #d2 #e2 #H #_ #_
+  >(ltpss_dx_inv_atom1 … H) -H /2 width=3/
+| #K1 #I #V1 #K2 #d2 #e2 #HK12 #H #_
+  lapply (le_n_O_to_eq … H) -H #H destruct /2 width=3/
+| #L1 #K1 #I #V #e1 #_ #IHLK1 #K2 #d2 #e2 #HK12 #H1 #H2
+  elim (IHLK1 … HK12 H1 H2) -K1 -H2
+  lapply (le_n_O_to_eq … H1) -H1 #H destruct /3 width=5/
+| #L1 #K1 #I #V1 #W1 #d1 #e1 #_ #HWV1 #IHLK1 #X #d2 #e2 #H #Hd21 #Hd12
+  elim (eq_or_gt d2) #Hd2 [ -Hd21 elim (eq_or_gt e2) #He2 ] destruct
+  [ lapply (le_n_O_to_eq … Hd12) -Hd12 <plus_n_Sm #H destruct
+  | elim (ltpss_dx_inv_tpss21 … H He2) -H #K2 #W2 #HK12 #HW12 #H destruct
+    elim (IHLK1 … HK12 …) -IHLK1 // /2 width=1/ >plus_minus_commutative // #L2 #HL12 #HLK2
+    elim (lift_total W2 d1 e1) #V2 #HWV2
+    lapply (tpss_lift_be … HW12 … HLK2 HWV1 … HWV2) -W1 // /2 width=1/
+    >plus_minus // >commutative_plus /4 width=5/
+  | elim (ltpss_dx_inv_tpss11 … H Hd2) -H #K2 #W2 #HK12 #HW12 #H destruct
+    elim (IHLK1 … HK12 …) -IHLK1 [2: >plus_minus // ] /2 width=1/ #L2 #HL12 #HLK2
+    elim (lift_total W2 d1 e1) #V2 #HWV2
+    lapply (tpss_lift_be … HW12 … HLK2 HWV1 … HWV2) -W1 [ >plus_minus // ] /2 width=1/
+    >commutative_plus /3 width=5/
+  ]
+]
+qed-.
+
+lemma ldrop_ltpss_dx_trans_ge: ∀L1,K1,d1,e1. ⇩[d1, e1] L1 ≡ K1 →
+                               ∀K2,d2,e2. K1 ▶* [d2, e2] K2 → d2 + e2 ≤ d1 →
+                               ∃∃L2. L1 ▶* [d2, e2] L2 & ⇩[d1, e1] L2 ≡ K2.
+#L1 #K1 #d1 #e1 #H elim H -L1 -K1 -d1 -e1
+[ #d1 #e1 #K2 #d2 #e2 #H #_
+  >(ltpss_dx_inv_atom1 … H) -H /2 width=3/
+| #K1 #I #V1 #K2 #d2 #e2 #HK12 #H
+  elim (plus_le_0 … H) -H #H1 #H2 destruct /2 width=3/
+| #L1 #K1 #I #V #e1 #_ #IHLK1 #K2 #d2 #e2 #HK12 #H
+  elim (IHLK1 … HK12 H) -K1
+  elim (plus_le_0 … H) -H #H1 #H2 destruct #L2 #HL12
+  >(ltpss_dx_inv_refl_O2 … HL12) -L1 /3 width=5/
+| #L1 #K1 #I #V1 #W1 #d1 #e1 #HLK1 #HWV1 #IHLK1 #X #d2 #e2 #H #Hd21
+  elim (eq_or_gt d2) #Hd2 [ elim (eq_or_gt e2) #He2 ] destruct
+  [ -IHLK1 -Hd21 <(ltpss_dx_inv_refl_O2 … H) -X /3 width=5/
+  | elim (ltpss_dx_inv_tpss21 … H He2) -H #K2 #W2 #HK12 #HW12 #H destruct
+    elim (IHLK1 … HK12 …) -IHLK1 /2 width=1/ #L2 #HL12 #HLK2
+    elim (lift_total W2 d1 e1) #V2 #HWV2
+    lapply (tpss_lift_le … HW12 … HLK2 HWV1 … HWV2) -W1 /2 width=1/ /3 width=5/
+  | elim (ltpss_dx_inv_tpss11 … H Hd2) -H #K2 #W2 #HK12 #HW12 #H destruct
+    elim (IHLK1 … HK12 …) -IHLK1 [2: >plus_minus // /2 width=1/ ] #L2 #HL12 #HLK2
+    elim (lift_total W2 d1 e1) #V2 #HWV2
+    lapply (tpss_lift_le … HW12 … HLK2 HWV1 … HWV2) -W1 [ >plus_minus // /2 width=1/ ] /3 width=5/
+  ]
+]
+qed-.
+
+(* Properties on supclosure *************************************************)
+
+lemma fsup_tps_trans_full: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ∀U2. L2 ⊢ T2 ▶[0,|L2|] U2 →
+                           ∃∃L,U1. L1 ▶*[0,|L|] L & L ⊢ T1 ▶[0,|L|] U1 & ⦃L, U1⦄ ⊃ ⦃L2, T2⦄.
+#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 (le_or_ge d (|K|)) #Hd
+[ elim (ldrop_ltpss_dx_trans_be … HLK1 … HK1 … Hd) // -HLK1 -HK1 #L2 #HL12 #HL2K
+  lapply (tps_lift_be … HT1 … HL2K … HTU1 HTU … Hd) // -HT1 -HTU1 #HU1
+| elim (ldrop_ltpss_dx_trans_ge … HLK1 … HK1 Hd) -HLK1 -HK1 #L2 #HL12 #HL2K
+  lapply (tps_lift_le … HT1 … HL2K … HTU1 HTU Hd) -HT1 -HTU1 #HU1
+]
+lapply (ltpss_dx_weak_full … HL12) -HL12 #HL12
+lapply (tps_weak_full … HU1) -HU1 #HU1
+@(ex3_2_intro … L2 U) // /2 width=7/ (**) (* explicit constructor: auto /3 width=14/ too slow *)
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_tpss.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_tpss.ma
index 04af50c8c..9c7875927 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_tpss.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_tpss.ma
@@ -12,7 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/unfold/tpss_lift.ma".
 include "basic_2/unfold/ltpss_dx_tps.ma".
 
 (* DX PARALLEL UNFOLD ON LOCAL ENVIRONMENTS *********************************)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn.ma
index e09cf12c5..577c1506d 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn.ma
@@ -12,6 +12,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
+notation "hvbox( T1 break ⊢ ▶ * [ term 46 d , break term 46 e ] break term 46 T2 )"
+   non associative with precedence 45
+   for @{ 'PSubstStarSn $T1 $d $e $T2 }.
+
 include "basic_2/unfold/tpss.ma".
 
 (* SN PARALLEL UNFOLD ON LOCAL ENVIRONMENTS *********************************)
@@ -206,7 +210,7 @@ lemma ltpss_sn_weak: ∀L1,L2,d1,e1. L1 ⊢ ▶* [d1, e1] L2 →
 ]
 qed.
 
-lemma ltpss_sn_weak_all: ∀L1,L2,d,e. L1 ⊢ ▶* [d, e] L2 → L1 ⊢ ▶* [0, |L1|] L2.
+lemma ltpss_sn_weak_full: ∀L1,L2,d,e. L1 ⊢ ▶* [d, e] L2 → L1 ⊢ ▶* [0, |L1|] L2.
 #L1 #L2 #d #e #H elim H -L1 -L2 -d -e
 // /3 width=2/ /3 width=3/
 qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_alt.ma
index 8b414d203..d2cdba023 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_alt.ma
@@ -12,6 +12,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
+notation "hvbox( T1 break ⊢ ▶ ▶ * [ term 46 d , break term 46 e ] break term 46 T2 )"
+   non associative with precedence 45
+   for @{ 'PSubstStarSnAlt $T1 $d $e $T2 }.
+
 include "basic_2/unfold/ltpss_dx_ltpss_dx.ma".
 include "basic_2/unfold/ltpss_sn_ltpss_sn.ma".
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_ldrop.ma
index bc4d73f3e..70167dfdd 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_ldrop.ma
@@ -12,11 +12,14 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basic_2/substitution/fsup.ma".
 include "basic_2/unfold/tpss_lift.ma".
 include "basic_2/unfold/ltpss_sn.ma".
 
 (* SN PARALLEL UNFOLD ON LOCAL ENVIRONMENTS *********************************)
 
+(* Properies on local environment slicing ***********************************)
+
 lemma ltpss_sn_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 ⊢ ▶* [d1, e1] L1 →
                               ∀L2,e2. ⇩[0, e2] L0 ≡ L2 →
                               d1 + e1 ≤ e2 → ⇩[0, e2] L1 ≡ L2.
@@ -131,6 +134,25 @@ lemma ltpss_sn_ldrop_trans_le: ∀L1,L0,d1,e1. L1 ⊢ ▶* [d1, e1] L0 →
 ]
 qed.
 
+lemma ldrop_ltpss_sn_trans_le: ∀L1,K1,d1,e1. ⇩[d1, e1] L1 ≡ K1 →
+                               ∀K2,d2,e2. K1 ⊢ ▶* [d2, e2] K2 → d1 ≤ d2 →
+                               ∃∃L2. L1 ⊢ ▶* [d2 + e1, e2] L2 & ⇩[d1, e1] L2 ≡ K2.
+#L1 #K1 #d1 #e1 #H elim H -L1 -K1 -d1 -e1
+[ #d1 #e1 #K2 #d2 #e2 #H #_
+  >(ltpss_sn_inv_atom1 … H) -H /2 width=3/
+| /2 width=3/
+| #L1 #K1 #I #V #e1 #_ #IHLK1 #K2 #d2 #e2 #HK12 #Hd
+  elim (IHLK1 … HK12 Hd) -K1 -Hd /3 width=5/
+| #L1 #K1 #I #V1 #W1 #d1 #e1 #HLK1 #HWV1 #IHLK1 #X #d2 #e2 #H #Hd12
+  elim (le_inv_plus_l … Hd12) -Hd12 #Hd12 #Hd2
+  elim (ltpss_sn_inv_tpss11 … H Hd2) -H #K2 #W2 #HK12 #HW12 #H destruct
+  elim (IHLK1 … HK12 … Hd12) -IHLK1 -HK12 <le_plus_minus_comm // #L2 #HL12 #HLK2
+  elim (lift_total W2 d1 e1) #V2 #HWV2
+  lapply (tpss_lift_ge … HW12 … HLK1 HWV1 … HWV2) -HLK1 -W1 // -Hd12
+  <le_plus_minus_comm // /4 width=5/
+]
+qed-.
+
 lemma ldrop_ltpss_sn_trans_be: ∀L1,K1,d1,e1. ⇩[d1, e1] L1 ≡ K1 →
                                ∀K2,d2,e2. K1 ⊢ ▶* [d2, e2] K2 →
                                d2 ≤ d1 → d1 ≤ d2 + e2 →
@@ -187,3 +209,23 @@ lemma ldrop_ltpss_sn_trans_ge: ∀L1,K1,d1,e1. ⇩[d1, e1] L1 ≡ K1 →
   ]
 ]
 qed-.
+
+(* Properties on supclosure *************************************************)
+
+lemma fsup_tpss_trans_full: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ∀U2. L2 ⊢ T2 ▶*[0,|L2|] U2 →
+                            ∃∃L,U1. L1 ⊢ ▶*[0,|L1|] L & L ⊢ T1 ▶*[0,|L|] U1 & ⦃L, U1⦄ ⊃ ⦃L2, T2⦄.
+#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
+lapply (ltpss_sn_fwd_length … HK1) #H >H in HK1; -H #HK1
+elim (le_or_ge d (|K|)) #Hd
+[ elim (ldrop_ltpss_sn_trans_be … HLK1 … HK1 … Hd) // -HLK1 -HK1 #L2 #HL12 #HL2K
+  lapply (tpss_lift_be … HT1 … Hd HL2K HTU1 … HTU) // -HT1 -HTU1 #HU1
+| elim (ldrop_ltpss_sn_trans_ge … HLK1 … HK1 Hd) -HLK1 -HK1 #L2 #HL12 #HL2K
+  lapply (tpss_lift_le … HT1 … Hd HL2K HTU1 … HTU) -HT1 -HTU1 #HU1
+]
+lapply (ltpss_sn_weak_full … HL12) -HL12 #HL12
+lapply (tpss_weak_full … HU1) -HU1 #HU1
+@(ex3_2_intro … L2 U) // /2 width=7/ (**) (* explicit constructor: auto /3 width=14/ too slow *)
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma
index 1fdae13f4..433718803 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma
@@ -12,6 +12,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
+notation "hvbox( L ⊢ break term 46 T1 break ▶ * [ term 46 d , break term 46 e ] break term 46 T2 )"
+   non associative with precedence 45
+   for @{ 'PSubstStar $L $T1 $d $e $T2 }.
+
 include "basic_2/substitution/tps.ma".
 
 (* PARTIAL UNFOLD ON TERMS **************************************************)
@@ -104,8 +108,8 @@ lemma tpss_weak_top: ∀L,T1,T2,d,e.
 ]
 qed.
 
-lemma tpss_weak_all: ∀L,T1,T2,d,e.
-                     L ⊢ T1 ▶* [d, e] T2 → L ⊢ T1 ▶* [0, |L|] T2.
+lemma tpss_weak_full: ∀L,T1,T2,d,e.
+                      L ⊢ T1 ▶* [d, e] T2 → L ⊢ T1 ▶* [0, |L|] T2.
 #L #T1 #T2 #d #e #HT12
 lapply (tpss_weak … HT12 0 (d + e) ? ?) -HT12 // #HT12
 lapply (tpss_weak_top … HT12) //
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_alt.ma
index 6fe188a7c..f7670eaa8 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_alt.ma
@@ -12,6 +12,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
+notation "hvbox( L ⊢ break term 46 T1 break ▶ ▶ * [ term 46 d , break term 46 e ] break term 46 T2 )"
+   non associative with precedence 45
+   for @{ 'PSubstStarAlt $L $T1 $d $e $T2 }.
+
 include "basic_2/unfold/tpss_lift.ma".
 
 (* PARALLEL UNFOLD ON TERMS *************************************************)
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 2b88582a7..b1f440f2e 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
@@ -154,8 +154,8 @@ table {
           }
         ]
         [ { "context-free reduction" * } {
-             [ "ltpr ( ? ➡ ? )" "ltpr_ldrop" + "ltpr_tps" + "ltpr_ltpss_dx" + "ltpr_ltpss_sn" + "ltpr_aaa" + "ltpr_ltpr" * ]
-             [ "tpr ( ? ➡ ? )"  "tpr_lift" + "tpr_tps" + "tpr_tpss" + "tpr_delift" + "tpr_tpr" * ]
+             [ "ltpr ( ? ➡ ? )" "ltpr_ldrop" + "ltpr_tps" + "ltpr_tpss" + "ltpr_ltpss_dx" + "ltpr_ltpss_sn" + "ltpr_aaa" + "ltpr_ltpr" * ]
+             [ "tpr ( ? ➡ ? )"  "tpr_lift" + "tpr_delift" + "tpr_tpr" * ]
           }
         ]
      }
@@ -198,19 +198,23 @@ table {
              [ "delift ( ? ⊢ ? ▼*[?,?] ≡ ? )" "delift_alt ( ? ⊢ ? ▼▼*[?,?] ≡ ? )" "delift_lift" + "delift_tpss" + "delift_ltpss" + "delift_delift" * ]
           }
         ]
-        [ { "partial unfold" * } {
+	[ { "revised parallel substitution" * } {
+             [ "lcpss ( ? ⊢ ▶* ? )" "lcpss_ldrop" + "lcpss_cpss" + "lcpss_lcpss" * ]
+             [ "cpss ( ? ⊢ ? ▶* ? )" "cpss_lift" * ]
+          }
+        ]        
+	[ { "partial unfold" * } {
              [ "ltpss_sn ( ? ⊢ ▶*[?,?] ? )" "ltpss_sn_alt ( ? ⊢ ▶▶*[?,?] ? )" "ltpss_sn_ldrop" + "ltpss_sn_tps" + "ltpss_sn_tpss" + "ltpss_sn_ltpss_sn" * ]
              [ "ltpss_dx ( ? ▶*[?,?] ? )" "ltpss_dx_ldrop" + "ltpss_dx_tps" + "ltpss_dx_tpss" + "ltpss_dx_ltpss_dx" * ]
              [ "tpss ( ? ⊢ ? ▶*[?,?] ? )" "tpss_alt ( ? ⊢ ? ▶▶*[?,?] ? )" "tpss_lift" "tpss_tpss" * ]
           }
         ]
-        [ { "generic local env. slicing" * } {
-             [ "ldrops ( ⇩*[?] ? ≡ ? )" "ldrops_ldrop" + "ldrops_ldrops" * ]
+        [ { "iterated structural successor for closures" * } {
+             [ "fsupp ( ⦃?,?⦄ ⊃+ ⦃?,?⦄ )" "fsupp_fsupp" * ]
           }
         ]
-        [ { "iterated restricted structural predecessor for closures" * } {
-             [ "frsups ( ⦃?,?⦄ ⧁* ⦃?,?⦄ )" "frsups_frsups" * ]
-             [ "frsupp ( ⦃?,?⦄ ⧁+ ⦃?,?⦄ )" "frsupp_frsupp" * ]
+        [ { "generic local env. slicing" * } {
+             [ "ldrops ( ⇩*[?] ? ≡ ? )" "ldrops_ldrop" + "ldrops_ldrops" * ]
           }
         ]
         [ { "generic term relocation" * } {
@@ -230,6 +234,10 @@ table {
              [ "tps ( ? ⊢ ? ▶[?,?] ? )" "tps_lift" + "tps_tps" * ]
           }
         ]
+        [ { "structural successor for closures" * } {
+             [ "fsup ( ⦃?,?⦄ ⊃ ⦃?,?⦄ )" * ]
+          }
+        ]
         [ { "global env. slicing" * } {
              [ "gdrop ( ⇩[?] ? ≡ ? )" "gdrop_gdrop" * ]
           }
@@ -242,10 +250,6 @@ table {
              [ "lsubr ( ? ⊑[?,?] ? )" "(lsubr_lsubr)" "lsubr_lbotr ( ⊒[?,?] ? )" * ]
           }
         ]
-        [ { "restricted structural predecessor for closures" * } {
-             [ "frsup ( ⦃?,?⦄ ⧁ ⦃?,?⦄ )" * ]
-          }
-        ]
         [ { "basic term relocation" * } {
              [ "lift_vector ( ⇧[?,?] ? ≡ ? )" "lift_lift_vector" * ]
              [ "lift ( ⇧[?,?] ? ≡ ? )" "lift_lift" * ]
-- 
2.39.2