From 53f874fba5b9c39a788085515a4fefe5d29281da Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 7 Nov 2012 16:18:41 +0000
Subject: [PATCH] - predefined_virtuals: nwe characters - lib: some additions -
 lambda_delta: commit of the components gramma, substitution, unfold   - we
 parked the support for the "bt-reduction"   - some renaming ...

---
 .../lambda_delta/basic_2/etc/csup/csup.etc    | 157 ++++++++++++++++++
 .../basic_2/etc/csup/csup_csup.etc            |  49 ++++++
 .../{unfold/csups.ma => etc/csup/csupp.etc}   |  39 +++--
 .../csup/csupp_csupp.etc}                     |   6 +-
 .../lambda_delta/basic_2/etc/csup/csups.etc   | 107 ++++++++++++
 .../basic_2/etc/csup/csups_csups.etc          |  62 +++++++
 .../lambda_delta/basic_2/etc/csup/ypr.etc     |  41 +++++
 .../lambda_delta/basic_2/etc/csup/yprs.etc    |  52 ++++++
 .../basic_2/etc/csup/yprs_csups.etc           |  25 +++
 .../csup.ma => etc/csup/yprs_xprs.etc}        |  27 ++-
 .../basic_2/etc/csup/yprs_yprs.etc            |  20 +++
 .../lambda_delta/basic_2/etc/csup/ysteps.etc  |  47 ++++++
 .../basic_2/etc/csup/ysteps_csups.etc         |  28 ++++
 .../lambda_delta/basic_2/grammar/cl_weight.ma |  20 +--
 .../lambda_delta/basic_2/grammar/lenv.ma      |  15 ++
 .../basic_2/grammar/lenv_append.ma            |  24 ++-
 .../basic_2/grammar/lenv_weight.ma            |   6 +-
 .../basic_2/grammar/term_weight.ma            |   6 +-
 .../basic_2/substitution/frsup.ma             | 119 +++++++++++++
 .../basic_2/substitution/ldrop.ma             |   2 +-
 .../basic_2/substitution/ldrop_ldrop.ma       |  16 ++
 .../lambda_delta/basic_2/unfold/delift_alt.ma |   4 +-
 .../basic_2/unfold/delift_lift.ma             |   4 +-
 .../lambda_delta/basic_2/unfold/frsupp.ma     | 107 ++++++++++++
 .../basic_2/unfold/frsupp_frsupp.ma           |  22 +++
 .../lambda_delta/basic_2/unfold/frsups.ma     | 134 +++++++++++++++
 .../basic_2/unfold/frsups_frsups.ma           |  22 +++
 .../basic_2/unfold/ltpss_dx_ltpss_dx.ma       |   4 +-
 .../lambda_delta/basic_2/unfold/ltpss_sn.ma   |   3 +-
 .../basic_2/unfold/ltpss_sn_ltpss_sn.ma       |   2 +-
 .../contribs/lambda_delta/ground_2/arith.ma   |  12 +-
 matita/matita/lib/arithmetics/nat.ma          |  22 ++-
 matita/matita/lib/basics/star.ma              |  71 ++++++++
 matita/matita/predefined_virtuals.ml          |   2 +-
 34 files changed, 1200 insertions(+), 77 deletions(-)
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/etc/csup/csup.etc
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/etc/csup/csup_csup.etc
 rename matita/matita/contribs/lambda_delta/basic_2/{unfold/csups.ma => etc/csup/csupp.etc} (60%)
 rename matita/matita/contribs/lambda_delta/basic_2/{unfold/csups_csups.ma => etc/csup/csupp_csupp.etc} (88%)
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/etc/csup/csups.etc
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/etc/csup/csups_csups.etc
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/etc/csup/ypr.etc
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/etc/csup/yprs.etc
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/etc/csup/yprs_csups.etc
 rename matita/matita/contribs/lambda_delta/basic_2/{substitution/csup.ma => etc/csup/yprs_xprs.etc} (56%)
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/etc/csup/yprs_yprs.etc
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/etc/csup/ysteps.etc
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/etc/csup/ysteps_csups.etc
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/substitution/frsup.ma
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/unfold/frsupp.ma
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/unfold/frsupp_frsupp.ma
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/unfold/frsups.ma
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/unfold/frsups_frsups.ma

diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/csup/csup.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/csup.etc
new file mode 100644
index 000000000..dcfe086e9
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/csup.etc
@@ -0,0 +1,157 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/
+#I #L1 #K1 #V1 #i #HLK1
+lapply (ldrop_fwd_ldrop2 … HLK1) -HLK1 /3 width=2/
+qed-. 
+
+(* Advanced forward lemmas **************************************************)
+
+lemma lift_csup_trans_eq: ∀T1,U1,d,e. ⇧[d, e] T1 ≡ U1 →
+                          ∀L,U2. ⦃L, U1⦄ > ⦃L, U2⦄ → 
+                          ∃T2. ⇧[d, e] T2 ≡ U2.
+#T1 #U1 #d #e * -T1 -U1 -d -e
+[5: #a #I #V1 #W1 #T1 #U1 #d #e #HVW1 #_ #L #X #H
+    elim (csup_inv_bind1 … H) -H *
+    [ #_ #H destruct /2 width=2/
+    | #H elim (discr_lpair_x_xy … H)
+    ]
+|6: #I #V1 #W1 #T1 #U1 #d #e #HVW1 #HUT1 #L #X #H
+    elim (csup_inv_flat1 … H) -H #_ * #H destruct /2 width=2/
+]
+#i #d #e [2,3: #_ ] #L #X #H
+elim (csup_inv_atom1 … H) -H #I #j #HL #H destruct
+lapply (ldrop_pair2_fwd_cw … HL X) -HL #H
+elim (lt_refl_false … H)
+qed-.
+(*
+lemma lift_csup_trans_gt: ∀L1,L2,U1,U2. ⦃L1, U1⦄ > ⦃L2, U2⦄ →
+                          ⇩[0, 1] L2 ≡ L1 → ∀T1,d,e. ⇧[d, e] T1 ≡ U1 →
+                          ∃T2. ⇧[d + 1, e] T2 ≡ U2.
+#L1 #L2 #U1 #U2 * -L1 -L2 -U1 -U2
+[ #I #L1 #K1 #V #i #HLK1 #HKL1
+  lapply (ldrop_fwd_lw … HLK1) -HLK1 #HLK1
+  lapply (ldrop_fwd_lw … HKL1) -HKL1 #HKL1
+  lapply (transitive_le … HLK1 HKL1) -L1 normalize #H
+  
+  
+| #a
+| #a
+]
+#I #L1 #W1 #U1 #HL1
+  
+
+
+ #X #d #e #H
+  lapply (ldrop_inv_refl … HL1) -HL1
+| #a #I #L1 #W1 #U1 #j #HL1 #X #d #e #H
+  lapply (ldrop_inv_ldrop1 … HL1)
+
+  elim (lift_inv_bind2 … H) -H #W2 #U2 #HW21 #HU21 #H destruct 
+   
+
+ /3 width=2/ /4 width=2/
+
+*)
+
+
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma csup_inv_lref2_be: ∀L,U,i. ⦃L, U⦄ > ⦃L, #i⦄ →
+                         ∀T,d,e. ⇧[d, e] T ≡ U → d ≤ i → i < d + e → ⊥.
+#L #U #i #H #T #d #e #HTU #Hdi #Hide
+elim (lift_csup_trans_eq … HTU … H) -H -T #T #H
+elim (lift_inv_lref2_be … H ? ?) //
+qed-.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/csup/csup_csup.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/csup_csup.etc
new file mode 100644
index 000000000..813cb969d
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/csup_csup.etc
@@ -0,0 +1,49 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/substitution/ldrop_ldrop.ma".
+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⦄ →
+                             ∀T3. ⦃L0, T2⦄ > ⦃L, T3⦄ →
+                             L = L0 ∨ ⦃L, T1⦄ > ⦃L, T3⦄.
+#L #L0 #T1 #T2 * -L -L0 -T1 -T2 /2 width=1/
+[ #I #L0 #K0 #V0 #i #HLK0 #T3 #H
+  lapply (ldrop_pair2_fwd_cw … HLK0 T3) -HLK0 #H1
+  lapply (csup_fwd_cw … H) -H #H2
+  lapply (transitive_lt … H1 H2) -H1 -H2 #H
+  elim (lt_refl_false … H)
+| #a #I #L0 #V2 #T2 #T3 #HT23
+  elim (csup_inv_ldrop … HT23 I V2 0 ?) -HT23 // #H1 #H2 destruct /2 width=1/
+  qed-.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/csups.ma b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/csupp.etc
similarity index 60%
rename from matita/matita/contribs/lambda_delta/basic_2/unfold/csups.ma
rename to matita/matita/contribs/lambda_delta/basic_2/etc/csup/csupp.etc
index 56cfa9ee8..c28eaea73 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/csups.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/csupp.etc
@@ -12,46 +12,53 @@
 (*                                                                        *)
 (**************************************************************************)
 
+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".
 
-(* ITERATED SUPCLOSURE ******************************************************)
+(* PLUS-ITERATED SUPCLOSURE *************************************************)
 
-definition csups: bi_relation lenv term ≝ bi_TC … csup.
+definition csupp: bi_relation lenv term ≝ bi_TC … csup.
 
-interpretation "iterated structural predecessor (closure)"
-   'SupTermStar L1 T1 L2 T2 = (csups L1 T1 L2 T2).
+interpretation "plus-iterated structural predecessor (closure)"
+   'SupTermPlus L1 T1 L2 T2 = (csupp L1 T1 L2 T2).
 
 (* Basic eliminators ********************************************************)
 
-lemma csups_ind: ∀L1,T1. ∀R:relation2 lenv term.
+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.
+                 (∀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 csups_ind_dx: ∀L2,T2. ∀R:relation2 lenv term.
+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.
+                    (∀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 csups_strap1: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ >* ⦃L, T⦄ → ⦃L, T⦄ > ⦃L2, T2⦄ →
-                    ⦃L1, T1⦄ >* ⦃L2, T2⦄.
+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 csups_strap2: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ > ⦃L, T⦄ → ⦃L, T⦄ >* ⦃L2, T2⦄ →
-                    ⦃L1, T1⦄ >* ⦃L2, T2⦄.
+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 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
+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/lambda_delta/basic_2/unfold/csups_csups.ma b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/csupp_csupp.etc
similarity index 88%
rename from matita/matita/contribs/lambda_delta/basic_2/unfold/csups_csups.ma
rename to matita/matita/contribs/lambda_delta/basic_2/etc/csup/csupp_csupp.etc
index 1446246c3..5afdb68d4 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/csups_csups.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/csupp_csupp.etc
@@ -12,11 +12,11 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/unfold/csups.ma".
+include "basic_2/unfold/csupp.ma".
 
-(* ITERATED SUPCLOSURE ******************************************************)
+(* PLUS-ITERATED SUPCLOSURE *************************************************)
 
 (* Main propertis ***********************************************************)
 
-theorem csups_trans: bi_transitive … csups.
+theorem csupp_trans: bi_transitive … csupp.
 /2 width=4/ qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/csup/csups.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/csups.etc
new file mode 100644
index 000000000..7f5879426
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/csups.etc
@@ -0,0 +1,107 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/lambda_delta/basic_2/etc/csup/csups_csups.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/csups_csups.etc
new file mode 100644
index 000000000..aa54d9bef
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/csups_csups.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/csup_csup.ma".
+include "basic_2/unfold/csups.ma".
+
+(* STAR-ITERATED SUPCLOSURE *************************************************)
+
+(* Advanced forward lemmas **************************************************)
+
+(*
+lemma csupp_strap2_fwd_refl: ∀L,L0,T1,T2. ⦃L, T1⦄ > ⦃L0, T2⦄ →
+                             ∀T3. ⦃L0, T2⦄ >+ ⦃L, T3⦄ →
+                             L = L0 ∨ ⦃L, T1⦄ >+ ⦃L, T3⦄.
+#L #L0 #T1 #T2 * -L -L0 -T1 -T2 /2 width=1/
+[ #I #L0 #K0 #V0 #i #HLK0 #T3 #H
+  lapply (ldrop_pair2_fwd_cw … HLK0 T3) -HLK0 #H1
+  lapply (csupp_fwd_cw … H) -H #H2
+  lapply (transitive_lt … H1 H2) -H1 -H2 #H
+  elim (lt_refl_false … H)
+| #a #I #L0 #V2 #T2 #T3 #HT23
+  /3 width=5/
+
+  elim (csup_inv_ldrop … HT23 I V2 0 ?) -HT23 // #H1 #H2 destruct /2 width=1/
+  qed-.
+
+
+
+
+
+
+
+
+lemma csups_strap1_fwd_refl: ∀L,L0,T1,T2. ⦃L, T1⦄ >* ⦃L0, T2⦄ →
+                             ∀T3. ⦃L0, T2⦄ > ⦃L, T3⦄ → L = L0.
+#L #L0 #T1 #T2 #H @(csups_ind_dx … H) -L -T1 //
+#L1 #L #T1 #T #HL1 #_ #IHL0 #T3 #HL0
+lapply (csup_trans_fwd_refl … HL10) … HL0) -T2
+*) 
+lemma lift_csups_trans_aux: ∀T1,U1,d,e. ⇧[d, e] T1 ≡ U1 →
+                            ∀L1,L2,U2. ⦃L1, U1⦄ >* ⦃L2, U2⦄ → L1 = L2 →
+                            ∃T2. ⇧[d, e] T2 ≡ U2.
+#T1 #U1 #d #e #HTU1 #L1 #L2 #U2 #H @(csups_ind … H) -L2 -U2 /2 width=2/ -T1
+#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/lambda_delta/basic_2/etc/csup/ypr.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/ypr.etc
new file mode 100644
index 000000000..f1510ab7e
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/ypr.etc
@@ -0,0 +1,41 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+notation "hvbox( h ⊢ break ⦃ L1, break T1 ⦄ • ⥸ break [ g ] break ⦃ L2 , break T2 ⦄ )"
+   non associative with precedence 45
+   for @{ 'YPRed $h $g $L1 $T1 $L2 $T2 }.
+
+include "basic_2/substitution/csup.ma".
+include "basic_2/reducibility/xpr.ma".
+
+(* HYPER PARALLEL REDUCTION ON CLOSURES *************************************)
+
+inductive ypr (h) (g) (L1) (T1): relation2 lenv term ≝
+| ypr_cpr : ∀T2. L1 ⊢ T1 ➡ T2 → ypr h g L1 T1 L1 T2
+| ypr_ssta: ∀T2,l. ⦃h, L1⦄ ⊢ T1 •[g, l + 1] T2 → ypr h g L1 T1 L1 T2
+| ypr_csup: ∀L2,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ → ypr h g L1 T1 L2 T2
+. 
+
+interpretation
+   "hyper parallel reduction (closure)"
+   'YPRed h g L1 T1 L2 T2 = (ypr h g L1 T1 L2 T2).
+
+(* Basic properties *********************************************************)
+
+lemma ypr_refl: ∀h,g. bi_reflexive … (ypr h g).
+/2 width=1/ qed.
+
+lemma xpr_ypr: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 •➡[g] T2 → h ⊢ ⦃L, T1⦄ •⥸[g] ⦃L, T2⦄.
+#h #g #L #T1 #T2 * /2 width=1/ /2 width=2/
+qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/csup/yprs.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/yprs.etc
new file mode 100644
index 000000000..86dc0c135
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/yprs.etc
@@ -0,0 +1,52 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+notation "hvbox( h ⊢ break ⦃ L1, break T1 ⦄ • ⥸  * break [ g ] break ⦃ L2 , break T2 ⦄ )"
+   non associative with precedence 45
+   for @{ 'YPRedStar $h $g $L1 $T1 $L2 $T2 }.
+
+include "basic_2/reducibility/ypr.ma".
+
+(* HYPER PARALLEL COMPUTATION ON CLOSURES ***********************************)
+
+definition yprs: ∀h. sd h → bi_relation lenv term ≝
+                 λh,g. bi_TC … (ypr h g).
+
+interpretation "hyper parallel computation (closure)"
+   'YPRedStar h g L1 T1 L2 T2 = (yprs h g L1 T1 L2 T2).
+
+(* Basic eliminators ********************************************************)
+
+lemma yprs_ind: ∀h,g,L1,T1. ∀R:relation2 lenv term. R L1 T1 →
+                (∀L,L2,T,T2. h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L, T⦄ → h ⊢ ⦃L, T⦄ •⥸[g] ⦃L2, T2⦄ → R L T → R L2 T2) →
+                ∀L2,T2. h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L2, T2⦄ → R L2 T2.
+/3 width=7 by bi_TC_star_ind/ qed-.
+
+lemma yprs_ind_dx: ∀h,g,L2,T2. ∀R:relation2 lenv term. R L2 T2 →
+                   (∀L1,L,T1,T. h ⊢ ⦃L1, T1⦄ •⥸[g] ⦃L, T⦄ → h ⊢ ⦃L, T⦄ •⥸*[g] ⦃L2, T2⦄ → R L T → R L1 T1) →
+                   ∀L1,T1. h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L2, T2⦄ → R L1 T1.
+/3 width=7 by bi_TC_star_ind_dx/ qed-.
+
+(* Basic properties *********************************************************)
+
+lemma yprs_refl: ∀h,g. bi_reflexive … (yprs h g).
+/2 width=1/ qed.
+
+lemma yprs_strap1: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L, T⦄ →
+                   h ⊢ ⦃L, T⦄ •⥸[g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L2, T2⦄.
+/2 width=4/ qed.
+
+lemma yprs_strap2: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ •⥸[g] ⦃L, T⦄ →
+                   h ⊢ ⦃L, T⦄ •⥸*[g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L2, T2⦄.
+/2 width=4/ qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/csup/yprs_csups.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/yprs_csups.etc
new file mode 100644
index 000000000..08c939d8d
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/yprs_csups.etc
@@ -0,0 +1,25 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/unfold/csups.ma".
+include "basic_2/computation/yprs.ma".
+
+(* HYPER PARALLEL COMPUTATION ON CLOSURES ***********************************)
+
+(* Properties on iterated supclosure ****************************************)
+
+lemma csups_yprs: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ >* ⦃L2, T2⦄ →
+                  h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L2, T2⦄.
+#h #g #L1 #L2 #T1 #T2 #H @(csups_ind … H) -L2 -T2 /3 width=1/ /3 width=4/
+qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/csup.ma b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/yprs_xprs.etc
similarity index 56%
rename from matita/matita/contribs/lambda_delta/basic_2/substitution/csup.ma
rename to matita/matita/contribs/lambda_delta/basic_2/etc/csup/yprs_xprs.etc
index 01a676616..2feb88a2f 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/substitution/csup.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/yprs_xprs.etc
@@ -12,24 +12,17 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/substitution/ldrop.ma".
+include "basic_2/computation/xprs_cprs.ma".
+include "basic_2/computation/yprs.ma".
 
-(* SUPCLOSURE ***************************************************************)
+(* HYPER PARALLEL COMPUTATION ON CLOSURES ***********************************)
 
-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
-.
+(* Properties on extended parallel computation for terms ********************)
 
-interpretation
-   "structural predecessor (closure)"
-   'SupTerm L1 T1 L2 T2 = (csup L1 T1 L2 T2).
+lemma xprs_yprs: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 •➡*[g] T2 →
+                 h ⊢ ⦃L, T1⦄ •⥸*[g] ⦃L, T2⦄.
+#h #g #L #T1 #T2 #H @(xprs_ind … H) -T2 // /3 width=4/
+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 cprs_yprs: ∀h,g,L,T1,T2. L ⊢ T1 ➡* T2 → h ⊢ ⦃L, T1⦄ •⥸*[g] ⦃L, T2⦄.
+/3 width=1/ qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/csup/yprs_yprs.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/yprs_yprs.etc
new file mode 100644
index 000000000..d737dd817
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/yprs_yprs.etc
@@ -0,0 +1,20 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/computation/yprs.ma".
+
+(* HYPER PARALLEL COMPUTATION ON TERMS **************************************)
+
+theorem yprs_trans: ∀h,g. bi_transitive … (yprs h g).
+/2 width=4/ qed-.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/csup/ysteps.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/ysteps.etc
new file mode 100644
index 000000000..149e7895b
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/ysteps.etc
@@ -0,0 +1,47 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+notation "hvbox( h ⊢ break ⦃ L1, break T1 ⦄ • ⭃ * break [ g ] break ⦃ L2 , break T2 ⦄ )"
+   non associative with precedence 45
+   for @{ 'YPRedStepStar $h $g $L1 $T1 $L2 $T2 }.
+
+include "basic_2/substitution/csup.ma".
+include "basic_2/computation/yprs.ma".
+
+(* ITERATED STEP OF HYPER PARALLEL COMPUTATION ON CLOSURES ******************)
+
+inductive ysteps (h) (g) (L1) (T1) (L2) (T2): Prop ≝
+| ysteps_intro: h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L2, T2⦄ → (L1 = L2 → T1 = T2 → ⊥) →
+                ysteps h g L1 T1 L2 T2
+.
+
+interpretation "iterated step of hyper parallel computation (closure)"
+   'YPRedStepStar h g L1 T1 L2 T2 = (ysteps h g L1 T1 L2 T2).
+
+(* Basic properties *********************************************************)
+
+lemma ssta_ysteps: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l + 1] U →
+                   h ⊢ ⦃L, T⦄ •⭃*[g] ⦃L, U⦄.
+#h #g #L #T #U #l #HTU
+@ysteps_intro /3 width=2/ #_ #H destruct
+elim (ssta_inv_refl … HTU)
+qed.
+
+lemma csup_ysteps: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ →
+                   h ⊢ ⦃L1, T1⦄ •⭃*[g] ⦃L2, T2⦄.
+#h #g #L1 #L2 #T1 #T2 #H
+lapply (csup_fwd_cw … H) #H1
+@ysteps_intro /3 width=1/ -H #H2 #H3 destruct
+elim (lt_refl_false … H1)
+qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/csup/ysteps_csups.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/ysteps_csups.etc
new file mode 100644
index 000000000..2e48f396d
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/ysteps_csups.etc
@@ -0,0 +1,28 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/computation/yprs_csups.ma".
+include "basic_2/computation/ysteps.ma".
+
+(* ITERATED STEP OF HYPER PARALLEL COMPUTATION ON CLOSURES ******************)
+
+(* Properties on iterated supclosure ****************************************)
+
+lemma csups_ysteps: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ >* ⦃L2, T2⦄ →
+                    h ⊢ ⦃L1, T1⦄ •⭃*[g] ⦃L2, T2⦄.
+#h #g #L1 #L2 #T1 #T2 #H
+lapply (csups_fwd_cw … H) #H1
+@ysteps_intro /2 width=1/ -H #H2 #H3 destruct
+elim (lt_refl_false … H1)
+qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_weight.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_weight.ma
index 40a364a44..478911825 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_weight.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_weight.ma
@@ -17,21 +17,21 @@ include "basic_2/grammar/cl_shift.ma".
 
 (* WEIGHT OF A CLOSURE ******************************************************)
 
-definition cw: lenv → term → ? ≝ λL,T. #{L} + #{T}.
+definition fw: lenv → term → ? ≝ λL,T. #{L} + #{T}.
 
-interpretation "weight (closure)" 'Weight L T = (cw L T).
+interpretation "weight (closure)" 'Weight L T = (fw L T).
 
 (* Basic properties *********************************************************)
 
 (* Basic_1: was: flt_wf__q_ind *)
 
 (* Basic_1: was: flt_wf_ind *)
-axiom cw_wf_ind: ∀R:lenv→predicate term.
-                 (∀L2,T2. (∀L1,T1. #{L1,T1} < #{L2,T2} → R L1 T1) → R L2 T2) →
-                 ∀L,T. R L T.
+axiom fw_ind: ∀R:relation2 lenv term.
+              (∀L2,T2. (∀L1,T1. #{L1,T1} < #{L2,T2} → R L1 T1) → R L2 T2) →
+              ∀L,T. R L T.
 
 (* Basic_1: was: flt_shift *)
-lemma cw_shift: ∀a,K,I,V,T. #{K. ⓑ{I} V, T} < #{K, ⓑ{a,I} V. T}.
+lemma fw_shift: ∀a,K,I,V,T. #{K. ⓑ{I} V, T} < #{K, ⓑ{a,I} V. T}.
 normalize //
 qed.
 
@@ -41,19 +41,19 @@ lemma tw_shift: ∀L,T. #{L, T} ≤ #{L @@ T}.
 @transitive_le [3: @IHL |2: /2 width=2/ | skip ]
 qed.
 
-lemma cw_tpair_sn: ∀I,L,V,T. #{L, V} < #{L, ②{I}V.T}.
+lemma fw_tpair_sn: ∀I,L,V,T. #{L, V} < #{L, ②{I}V.T}.
 #I #L #V #T normalize in ⊢ (? % %); //
 qed.
 
-lemma cw_tpair_dx: ∀I,L,V,T. #{L, T} < #{L, ②{I}V.T}.
+lemma fw_tpair_dx: ∀I,L,V,T. #{L, T} < #{L, ②{I}V.T}.
 #I #L #V #T normalize in ⊢ (? % %); //
 qed.
 
-lemma cw_tpair_dx_sn: ∀I1,I2,L,V1,V2,T. #{L, V2} < #{L, ②{I1}V1.②{I2}V2.T}.
+lemma fw_tpair_dx_sn: ∀I1,I2,L,V1,V2,T. #{L, V2} < #{L, ②{I1}V1.②{I2}V2.T}.
 #I1 #I2 #L #V1 #V2 #T normalize in ⊢ (? % %); /2 width=1/
 qed.
 
-lemma cw_tpair_dx_sn_shift: ∀a2,I1,I2,L,V1,V2,T.
+lemma fw_tpair_dx_sn_shift: ∀a2,I1,I2,L,V1,V2,T.
                             #{L.ⓑ{I2}V2, T} < #{L, ②{I1}V1.ⓑ{a2,I2}V2.T}.
 #a2 #I1 #I2 #L #V1 #V2 #T normalize in ⊢ (? % %); /2 width=1/
 qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv.ma
index ba94738a8..9988b3d4c 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv.ma
@@ -37,4 +37,19 @@ interpretation "abbreviation (local environment)"
 interpretation "abstraction (local environment)"
    'DxAbst L T = (LPair L Abst T).
 
+(* Basic inversion lemmas ***************************************************)
+
+lemma destruct_lpair_lpair: ∀I1,I2,L1,L2,V1,V2. L1.ⓑ{I1}V1 = L2.ⓑ{I2}V2 →
+                            ∧∧L1 = L2 & I1 = I2 & V1 = V2.
+#I1 #I2 #L1 #L2 #V1 #V2 #H destruct /2 width=1/
+qed-.
+
+lemma discr_lpair_x_xy: ∀I,V,L. L = L.ⓑ{I}V → ⊥.
+#I #V #L elim L -L
+[ #H destruct
+| #L #J #W #IHL #H
+  elim (destruct_lpair_lpair … H) -H #H1 #H2 #H3 destruct /2 width=1/ (**) (* destruct lemma needed *)
+]
+qed-.
+
 (* Basic_1: removed theorems 2: chead_ctail c_tail_ind *)
diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_append.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_append.ma
index f58f96076..ab90ddf29 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_append.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_append.ma
@@ -46,9 +46,9 @@ lemma append_inj_sn: ∀K1,K2,L1,L2. L1 @@ K1 = L2 @@ K2 → |K1| = |K2| →
   #K2 #I2 #V2 #L1 #L2 #_ <plus_n_Sm #H destruct
 | #K1 #I1 #V1 #IH * normalize
   [ #L1 #L2 #_ <plus_n_Sm #H destruct
-  | #K2 #I2 #V2 #L1 #L2 #H1 #H2 destruct (**) (* destruct does not simplify well *)
-    -H1 (**) (* destruct: the destucted equality is not erased *)
-    elim (IH … e0 ?) -IH /2 width=1/ -H2 #H1 #H2 destruct /2 width=1/
+  | #K2 #I2 #V2 #L1 #L2 #H1 #H2
+    elim (destruct_lpair_lpair … H1) -H1 #H1 #H3 #H4 destruct (**) (* destruct lemma needed *)
+    elim (IH … H1 ?) -IH -H1 // -H2 /2 width=1/
   ]
 ]
 qed-.
@@ -65,20 +65,30 @@ lemma append_inj_dx: ∀K1,K2,L1,L2. L1 @@ K1 = L2 @@ K2 → |L1| = |L2| →
   [ #L1 #L2 #H1 #H2 destruct
     normalize in H2; >append_length in H2; #H
     elim (plus_xySz_x_false … (sym_eq … H))
-  | #K2 #I2 #V2 #L1 #L2 #H1 #H2 destruct (**) (* destruct does not simplify well *)
-    -H1 (**) (* destruct: the destucted equality is not erased *)
-    elim (IH … e0 ?) -IH // -H2 #H1 #H2 destruct /2 width=1/
+  | #K2 #I2 #V2 #L1 #L2 #H1 #H2
+    elim (destruct_lpair_lpair … H1) -H1 #H1 #H3 #H4 destruct (**) (* destruct lemma needed *)
+    elim (IH … H1 ?) -IH -H1 // -H2 /2 width=1/
   ]
 ]
 qed-.
 
+lemma append_inv_refl_dx: ∀L,K. L @@ K = L → K = ⋆.
+#L #K #H
+elim (append_inj_dx … (⋆) … H ?) //
+qed-.
+
+lemma append_inv_pair_dx: ∀I,L,K,V. L @@ K = L.ⓑ{I}V → K = ⋆.ⓑ{I}V.
+#I #L #K #V #H
+elim (append_inj_dx … (⋆.ⓑ{I}V) … H ?) //
+qed-.
+
 lemma length_inv_pos_dx_append: ∀d,L. |L| = d + 1 →
                                 ∃∃I,K,V. |K| = d & L = ⋆.ⓑ{I}V @@ K.
 #d @(nat_ind_plus … d) -d
 [ #L #H 
   elim (length_inv_pos_dx … H) -H #I #K #V #H
   >(length_inv_zero_dx … H) -H #H destruct
-  @ex2_3_intro [4: /2 width=2/ |5: // |1,2,3: skip ] (* /3/ does not work *)
+  @ex2_3_intro [4: /2 width=2/ |5: // |1,2,3: skip ] (**) (* /3/ does not work *)
 | #d #IHd #L #H
   elim (length_inv_pos_dx … H) -H #I #K #V #H
   elim (IHd … H) -IHd -H #I0 #K0 #V0 #H1 #H2 #H3 destruct
diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_weight.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_weight.ma
index d277ed00e..59e2e6172 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_weight.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_weight.ma
@@ -31,9 +31,9 @@ lemma lw_pair: ∀I,L,V. #{L} < #{(L.ⓑ{I}V)}.
 
 (* Basic eliminators ********************************************************)
 
-axiom lw_wf_ind: ∀R:predicate lenv.
-                 (∀L2. (∀L1. #{L1} < #{L2} → R L1) → R L2) →
-                 ∀L. R L.
+axiom lw_ind: ∀R:predicate lenv.
+              (∀L2. (∀L1. #{L1} < #{L2} → R L1) → R L2) →
+              ∀L. R L.
 
 (* Basic_1: removed theorems 2: clt_cong clt_head clt_thead *)
 (* Basic_1: note: clt_thead should be renamed clt_ctail *)
diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/term_weight.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/term_weight.ma
index ce05e436e..d8f39a3a1 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/grammar/term_weight.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/term_weight.ma
@@ -32,9 +32,9 @@ qed.
 
 (* Basic eliminators ********************************************************)
 
-axiom tw_wf_ind: ∀R:predicate term.
-                 (∀T2. (∀T1. #{T1} < #{T2} → R T1) → R T2) →
-                 ∀T. R T.
+axiom tw_ind: ∀R:predicate term.
+              (∀T2. (∀T1. #{T1} < #{T2} → R T1) → R T2) →
+              ∀T. R T.
 
 (* Basic_1: removed theorems 11:
             wadd_le wadd_lt wadd_O weight_le weight_eq weight_add_O
diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/frsup.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/frsup.ma
new file mode 100644
index 000000000..31d6c9fee
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/frsup.ma
@@ -0,0 +1,119 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/cl_weight.ma".
+include "basic_2/substitution/lift.ma".
+
+(* RESTRICTED SUPCLOSURE ****************************************************)
+
+inductive frsup: bi_relation lenv term ≝
+| frsup_bind_sn: ∀a,I,L,V,T. frsup L (ⓑ{a,I}V.T) L V
+| frsup_bind_dx: ∀a,I,L,V,T. frsup L (ⓑ{a,I}V.T) (L.ⓑ{I}V) T
+| frsup_flat_sn: ∀I,L,V,T.   frsup L (ⓕ{I}V.T) L V
+| frsup_flat_dx: ∀I,L,V,T.   frsup L (ⓕ{I}V.T) L T
+.
+
+interpretation
+   "restricted structural predecessor (closure)"
+   'RestSupTerm L1 T1 L2 T2 = (frsup L1 T1 L2 T2).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact frsup_inv_atom1_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ →
+                          ∀J. T1 = ⓪{J} → ⊥.
+#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2
+[ #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 frsup_inv_atom1: ∀J,L1,L2,T2. ⦃L1, ⓪{J}⦄ ⧁ ⦃L2, T2⦄ → ⊥.
+/2 width=7 by frsup_inv_atom1_aux/ qed-.
+
+fact frsup_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
+[ #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 frsup_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 frsup_inv_bind1_aux/ qed-.
+
+fact frsup_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
+[ #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 frsup_inv_flat1: ∀J,L1,L2,W,U,T2. ⦃L1, ⓕ{J}W.U⦄ ⧁ ⦃L2, T2⦄ →
+                       L2 = L1 ∧ (T2 = W ∨ T2 = U).
+/2 width=4 by frsup_inv_flat1_aux/ qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma frsup_fwd_fw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → #{L2, T2} < #{L1, T1}.
+#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2 /width=1/
+qed-.
+
+lemma frsup_fwd_lw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → #{L1} ≤ #{L2}.
+#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2 /width=1/
+qed-.
+
+lemma frsup_fwd_tw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → #{T2} < #{T1}.
+#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2 /width=1/ /2 width=1 by le_minus_to_plus/
+qed-.
+
+lemma frsup_fwd_append: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → ∃L. L2 = L1 @@ L.
+#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2
+[ #a
+| #a #I #L #V #_ @(ex_intro … (⋆.ⓑ{I}V)) //
+]
+#I #L #V #T @(ex_intro … (⋆)) //
+qed-.
+
+(* Advanced forward lemmas **************************************************)
+
+lemma lift_frsup_trans: ∀T1,U1,d,e. ⇧[d, e] T1 ≡ U1 →
+                        ∀L,K,U2. ⦃L, U1⦄ ⧁ ⦃L @@ K, U2⦄ →
+                        ∃T2. ⇧[d + |K|, e] T2 ≡ U2.
+#T1 #U1 #d #e * -T1 -U1 -d -e
+[5: #a #I #V1 #W1 #T1 #U1 #d #e #HVW1 #HTU1 #L #K #X #H
+    elim (frsup_inv_bind1 … H) -H *
+    [ -HTU1 #H1 #H2 destruct
+      >(append_inv_refl_dx … H1) -L -K normalize /2 width=2/
+    | -HVW1 #H1 #H2 destruct
+      >(append_inv_pair_dx … H1) -L -K normalize /2 width=2/
+    ]
+|6: #I #V1 #W1 #T1 #U1 #d #e #HVW1 #HUT1 #L #K #X #H
+    elim (frsup_inv_flat1 … H) -H #H1 * #H2 destruct
+    >(append_inv_refl_dx … H1) -L -K normalize /2 width=2/
+]
+#i #d #e [2,3: #_ ] #L #K #X #H
+elim (frsup_inv_atom1 … H)
+qed-.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma
index c93d3cd18..9511648aa 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma
@@ -266,7 +266,7 @@ lemma ldrop_fwd_lw: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → #{L2} ≤ #{L1}.
 ]
 qed-. 
 
-lemma ldrop_pair2_fwd_cw: ∀I,L,K,V,d,e. ⇩[d, e] L ≡ K. ⓑ{I} V →
+lemma ldrop_pair2_fwd_fw: ∀I,L,K,V,d,e. ⇩[d, e] L ≡ K. ⓑ{I} V →
                           ∀T. #{K, V} < #{L, T}.
 #I #L #K #V #d #e #H #T
 lapply (ldrop_fwd_lw … H) -H #H
diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_ldrop.ma
index b7862fcbf..07d9c53e4 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_ldrop.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_ldrop.ma
@@ -158,3 +158,19 @@ lemma ldrop_trans_ge_comm: ∀d1,e1,e2,L1,L2,L.
                            ⇩[0, e2 + e1] L1 ≡ L2.
 #e1 #e1 #e2 >commutative_plus /2 width=5/
 qed.
+
+lemma ldrop_conf_div: ∀I1,L,K,V1,e1. ⇩[0, e1] L ≡ K. ⓑ{I1} V1 →
+                      ∀I2,V2,e2. ⇩[0, e2] L ≡ K. ⓑ{I2} V2 →
+                      ∧∧ e1 = e2 & I1 = I2 & V1 = V2.
+#I1 #L #K #V1 #e1 #HLK1 #I2 #V2 #e2 #HLK2
+elim (le_or_ge e1 e2) #He
+[ lapply (ldrop_conf_ge … HLK1 … HLK2 ?)
+| lapply (ldrop_conf_ge … HLK2 … HLK1 ?)
+] -HLK1 -HLK2 // #HK
+lapply (ldrop_fwd_O1_length … HK) #H
+elim (discr_minus_x_xy … H) -H
+[1,3: normalize <plus_n_Sm #H destruct ]
+#H >H in HK; #HK
+lapply (ldrop_inv_refl … HK) -HK #H destruct
+lapply (inv_eq_minus_O … H) -H /3 width=1/
+qed-.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_alt.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_alt.ma
index 84c8bee70..9a3eb1b7c 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_alt.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_alt.ma
@@ -49,12 +49,12 @@ lemma delifta_lsubs_trans: ∀L1,T1,T2,d,e. L1 ⊢ ▼▼*[d, e] T1 ≡ T2 →
 qed.
 
 lemma delift_delifta: ∀L,T1,T2,d,e. L ⊢ ▼*[d, e] T1 ≡ T2 → L ⊢ ▼▼*[d, e] T1 ≡ T2.
-#L #T1 @(cw_wf_ind … L T1) -L -T1 #L #T1 elim T1 -T1
+#L #T1 @(fw_ind … L T1) -L -T1 #L #T1 elim T1 -T1
 [ * #i #IH #T2 #d #e #H
   [ >(delift_inv_sort1 … H) -H //
   | elim (delift_inv_lref1 … H) -H * /2 width=1/
     #K #V1 #V2 #Hdi #Hide #HLK #HV12 #HVT2
-    lapply (ldrop_pair2_fwd_cw … HLK) #H
+    lapply (ldrop_pair2_fwd_fw … HLK) #H
     lapply (IH … HV12) // -H /2 width=6/
   | >(delift_inv_gref1 … H) -H //
   ]
diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma
index a53033aa0..01ee6108e 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma
@@ -32,14 +32,14 @@ qed.
 
 fact sfr_delift_aux: ∀L,T,T1,d,e. d + e ≤ |L| → ≽ [d, e] L → T = T1 →
                      ∃T2. L ⊢ ▼*[d, e] T1 ≡ T2.
-#L #T @(cw_wf_ind … L T) -L -T #L #T #IH * * /2 width=2/
+#L #T @(fw_ind … L T) -L -T #L #T #IH * * /2 width=2/
 [ #i #d #e #Hde #HL #H destruct
   elim (lt_or_ge i d) #Hdi [ /3 width=2/ ]
   elim (lt_or_ge i (d+e)) #Hide [2: /3 width=2/ ]
   lapply (lt_to_le_to_lt … Hide Hde) #Hi
   elim (ldrop_O1_lt … Hi) -Hi #I #K #V1 #HLK
   lapply (sfr_inv_ldrop … HLK … HL ? ?) // #H destruct
-  lapply (ldrop_pair2_fwd_cw … HLK (#i)) #HKL
+  lapply (ldrop_pair2_fwd_fw … HLK (#i)) #HKL
   lapply (ldrop_fwd_ldrop2 … HLK) #HLK0
   lapply (ldrop_fwd_O1_length … HLK0) #H
   lapply (sfr_ldrop_trans_be_up … HLK0 … HL ? ?) -HLK0 -HL
diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/frsupp.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/frsupp.ma
new file mode 100644
index 000000000..9cfee7cfd
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/frsupp.ma
@@ -0,0 +1,107 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/frsup.ma".
+
+(* PLUS-ITERATED RESTRICTED SUPCLOSURE **************************************)
+
+definition frsupp: bi_relation lenv term ≝ bi_TC … frsup.
+
+interpretation "plus-iterated restricted structural predecessor (closure)"
+   'RestSupTermPlus L1 T1 L2 T2 = (frsupp L1 T1 L2 T2).
+
+(* Basic eliminators ********************************************************)
+
+lemma frsupp_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 frsupp_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 frsup_frsupp: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄.
+/2 width=1/ qed.
+
+lemma frsupp_strap1: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⧁+ ⦃L, T⦄ → ⦃L, T⦄ ⧁ ⦃L2, T2⦄ →
+                     ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄.
+/2 width=4/ qed.
+
+lemma frsupp_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 frsupp_fwd_fw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → #{L2, T2} < #{L1, T1}.
+#L1 #L2 #T1 #T2 #H @(frsupp_ind … H) -L2 -T2
+/3 width=3 by frsup_fwd_fw, transitive_lt/
+qed-.
+
+lemma frsupp_fwd_lw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → #{L1} ≤ #{L2}.
+#L1 #L2 #T1 #T2 #H @(frsupp_ind … H) -L2 -T2
+/2 width=3 by frsup_fwd_lw/ (**) (* /3 width=5 by frsup_fwd_lw, transitive_le/ is too slow *)
+#L #T #L2 #T2 #_ #HL2 #HL1
+lapply (frsup_fwd_lw … HL2) -HL2 /2 width=3 by transitive_le/
+qed-.
+
+lemma frsupp_fwd_tw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → #{T2} < #{T1}.
+#L1 #L2 #T1 #T2 #H @(frsupp_ind … H) -L2 -T2
+/3 width=3 by frsup_fwd_tw, transitive_lt/
+qed-.
+
+lemma frsupp_fwd_append: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → ∃L. L2 = L1 @@ L.
+#L1 #L2 #T1 #T2 #H @(frsupp_ind … H) -L2 -T2 /2 width=3 by frsup_fwd_append/
+#L #T #L2 #T2 #_ #HL2 * #K1 #H destruct
+elim (frsup_fwd_append … HL2) -HL2 #K2 #H destruct /2 width=2/
+qed-.
+
+(* Advanced forward lemmas **************************************************)
+
+fact lift_frsupp_trans_aux: ∀L2,U0. (
+                               ∀L,K,U1,U2. ⦃L, U1⦄ ⧁+ ⦃L @@ K, U2⦄ →
+                               ∀T1,d,e. ⇧[d, e] T1 ≡ U1 →
+                               #{L, U1} < #{L2, U0} → 
+                               ∃T2. ⇧[d + |K|, e] T2 ≡ U2
+                            ) →
+                            ∀L1,K,U1,U2. ⦃L1, U1⦄ ⧁+ ⦃L2 @@ K, U2⦄ →
+                            ∀T1,d,e. ⇧[d, e] T1 ≡ U1 →
+                            L2 = L1 → U0 = U1 →
+                            ∃T2. ⇧[d + |K|, e] T2 ≡ U2.
+#L2 #U0 #IH #L1 #X #U1 #U2 #H @(frsupp_ind_dx … H) -L1 -U1 /2 width=5 by lift_frsup_trans/
+#L1 #L #U1 #U #HL1 #HL2 #_ #T1 #d #e #HTU1 #H1 #H2 destruct
+elim (frsup_fwd_append … HL1) #K1 #H destruct
+elim (frsupp_fwd_append … HL2) #K >append_assoc #H
+elim (append_inj_dx … H ?) -H // #_ #H destruct
+<append_assoc in HL2; #HL2
+elim (lift_frsup_trans … HTU1 … HL1) -T1 #T #HTU
+lapply (frsup_fwd_fw … HL1) -HL1 #HL1
+elim (IH … HL2 … HTU ?) -IH -HL2 -T // -L1 -U1 -U /2 width=2/
+qed-.
+
+lemma lift_frsupp_trans: ∀L,U1,K,U2. ⦃L, U1⦄ ⧁+ ⦃L @@ K, U2⦄ →
+                         ∀T1,d,e. ⇧[d, e] T1 ≡ U1 →
+                         ∃T2. ⇧[d + |K|, e] T2 ≡ U2.
+#L #U1 @(fw_ind … L U1) -L -U1 /3 width=10 by lift_frsupp_trans_aux/
+qed-.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/frsupp_frsupp.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/frsupp_frsupp.ma
new file mode 100644
index 000000000..92efe26ce
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/frsupp_frsupp.ma
@@ -0,0 +1,22 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/frsupp.ma".
+
+(* PLUS-ITERATED RESTRICTED SUPCLOSURE **************************************)
+
+(* Main propertis ***********************************************************)
+
+theorem frsupp_trans: bi_transitive … frsupp.
+/2 width=4/ qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/frsups.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/frsups.ma
new file mode 100644
index 000000000..9d216beca
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/frsups.ma
@@ -0,0 +1,134 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/substitution/frsup.ma".
+include "basic_2/unfold/frsupp.ma".
+
+(* STAR-ITERATED RESTRICTED SUPCLOSURE **************************************)
+
+definition frsups: bi_relation lenv term ≝ bi_star … frsup.
+
+interpretation "star-iterated restricted structural predecessor (closure)"
+   'RestSupTermStar L1 T1 L2 T2 = (frsups L1 T1 L2 T2).
+
+(* Basic eliminators ********************************************************)
+
+lemma frsups_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 frsups_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 frsups_refl: bi_reflexive … frsups.
+/2 width=1/ qed.
+
+lemma frsupp_frsups: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⧁* ⦃L2, T2⦄.
+/2 width=1/ qed.
+
+lemma frsup_frsups: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⧁* ⦃L2, T2⦄.
+/2 width=1/ qed.
+
+lemma frsups_strap1: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⧁* ⦃L, T⦄ → ⦃L, T⦄ ⧁ ⦃L2, T2⦄ →
+                     ⦃L1, T1⦄ ⧁* ⦃L2, T2⦄.
+/2 width=4/ qed.
+
+lemma frsups_strap2: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⧁ ⦃L, T⦄ → ⦃L, T⦄ ⧁* ⦃L2, T2⦄ →
+                     ⦃L1, T1⦄ ⧁* ⦃L2, T2⦄.
+/2 width=4/ qed.
+
+lemma frsups_frsupp_frsupp: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⧁* ⦃L, T⦄ →
+                            ⦃L, T⦄ ⧁+ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄.
+/2 width=4/ qed.
+
+lemma frsupp_frsups_frsupp: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⧁+ ⦃L, T⦄ →
+                            ⦃L, T⦄ ⧁* ⦃L2, T2⦄ → ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄.
+/2 width=4/ qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma frsups_inv_all: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁* ⦃L2, T2⦄ →
+                      (L1 = L2 ∧ T1 = T2) ∨ ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄.
+#L1 #L2 #T1 #T2 * /2 width=1/
+qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma frsups_fwd_fw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁* ⦃L2, T2⦄ → #{L2, T2} ≤ #{L1, T1}.
+#L1 #L2 #T1 #T2 #H elim (frsups_inv_all … H) -H [ * // ]
+/3 width=1 by frsupp_fwd_fw, lt_to_le/
+qed-.
+
+lemma frsups_fwd_lw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁* ⦃L2, T2⦄ → #{L1} ≤ #{L2}.
+#L1 #L2 #T1 #T2 #H elim (frsups_inv_all … H) -H [ * // ]
+/2 width=3 by frsupp_fwd_lw/
+qed-.
+
+lemma frsups_fwd_tw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁* ⦃L2, T2⦄ → #{T2} ≤ #{T1}.
+#L1 #L2 #T1 #T2 #H elim (frsups_inv_all … H) -H [ * // ]
+/3 width=3 by frsupp_fwd_tw, lt_to_le/
+qed-.
+
+lemma frsups_fwd_append: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁* ⦃L2, T2⦄ → ∃L. L2 = L1 @@ L.
+#L1 #L2 #T1 #T2 #H elim (frsups_inv_all … H) -H
+[ * #H1 #H2 destruct
+  @(ex_intro … (⋆)) //
+| /2 width=3 by frsupp_fwd_append/
+qed-.
+
+(* Advanced forward lemmas ***************************************************)
+
+lemma lift_frsups_trans: ∀T1,U1,d,e. ⇧[d, e] T1 ≡ U1 →
+                         ∀L,K,U2. ⦃L, U1⦄ ⧁* ⦃L @@ K, U2⦄ →
+                         ∃T2. ⇧[d + |K|, e] T2 ≡ U2.
+#T1 #U1 #d #e #HTU1 #L #K #U2 #H elim (frsups_inv_all … H) -H
+[ * #H1 #H2 destruct
+  >(append_inv_refl_dx … (sym_eq … H1)) -H1 normalize /2 width=2/
+| /2 width=5 by lift_frsupp_trans/
+]
+qed-.
+
+(* Advanced inversion lemmas for frsupp **************************************)
+
+lemma frsupp_inv_atom1_frsups: ∀J,L1,L2,T2. ⦃L1, ⓪{J}⦄ ⧁+ ⦃L2, T2⦄ → ⊥.
+#J #L1 #L2 #T2 #H @(frsupp_ind … H) -L2 -T2 //
+#L2 #T2 #H elim (frsup_inv_atom1 … H)
+qed-.
+
+lemma frsupp_inv_bind1_frsups: ∀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 @(frsupp_ind … H) -L2 -T2
+[ #L2 #T2 #H
+  elim (frsup_inv_bind1 … H) -H * #H1 #H2 destruct /2 width=1/
+| #L #T #L2 #T2 #_ #HT2 * /3 width=4/
+]
+qed-.
+
+lemma frsupp_inv_flat1_frsups: ∀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 @(frsupp_ind … H) -L2 -T2
+[ #L2 #T2 #H
+  elim (frsup_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/lambda_delta/basic_2/unfold/frsups_frsups.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/frsups_frsups.ma
new file mode 100644
index 000000000..e7b7de26e
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/frsups_frsups.ma
@@ -0,0 +1,22 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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".
+
+(* STAR-ITERATED RESTRICTED SUPCLOSURE **************************************)
+
+(* Main propertis ***********************************************************)
+
+theorem frsups_trans: bi_transitive … frsups.
+/2 width=4/ qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_dx_ltpss_dx.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_dx_ltpss_dx.ma
index 22fa61ffc..5ea9f6bd6 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_dx_ltpss_dx.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_dx_ltpss_dx.ma
@@ -46,7 +46,7 @@ qed.
 fact ltpss_dx_tpss_trans_eq_aux: ∀Y1,X2,L1,T2,U2,d,e.
                                  L1 ⊢ T2 ▶* [d, e] U2 → ∀L0. L0 ▶* [d, e] L1 →
                                  Y1 = L1 → X2 = T2 → L0 ⊢ T2 ▶* [d, e] U2.
-#Y1 #X2 @(cw_wf_ind … Y1 X2) -Y1 -X2 #Y1 #X2 #IH
+#Y1 #X2 @(fw_ind … Y1 X2) -Y1 -X2 #Y1 #X2 #IH
 #L1 #T2 #U2 #d #e #H @(tpss_ind_alt … H) -L1 -T2 -U2 -d -e
 [ //
 | #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #HV12 #HVW2 #_ #L0 #HL01 #H1 #H2 destruct
@@ -82,7 +82,7 @@ lemma ltpss_dx_tps_trans_eq: ∀L0,L1,T2,U2,d,e. L0 ▶* [d, e] L1 →
 fact ltpss_dx_conf_aux: ∀K,K1,L1,d1,e1. K1 ▶* [d1, e1] L1 →
                         ∀K2,L2,d2,e2. K2 ▶* [d2, e2] L2 → K1 = K → K2 = K →
                         ∃∃L. L1 ▶* [d2, e2] L & L2 ▶* [d1, e1] L.
-#K @(lw_wf_ind … K) -K #K #IH #K1 #L1 #d1 #e1 * -K1 -L1 -d1 -e1
+#K @(lw_ind … K) -K #K #IH #K1 #L1 #d1 #e1 * -K1 -L1 -d1 -e1
 [ -IH /2 width=3/
 | -IH #K1 #I1 #V1 #K2 #L2 #d2 #e2 * -K2 -L2 -d2 -e2
   [ /2 width=3/
diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn.ma
index 95eb9efd9..0d13a5a3f 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn.ma
@@ -200,7 +200,8 @@ lemma ltpss_sn_weak: ∀L1,L2,d1,e1. L1 ⊢ ▶* [d1, e1] L2 →
     lapply (le_plus_to_minus … Hd21) -Hd21 #Hd21 /3 width=5/
   | -Hd21 normalize in Hde12;
     lapply (lt_to_le_to_lt 0 … Hde12) // #He2
-    lapply (le_plus_to_minus_r … Hde12) -Hde12 /3 width=5/
+    lapply (le_plus_to_minus_r … Hde12) -Hde12
+    /3 width=5 by ltpss_sn_tpss2_lt, tpss_weak/ (**) (* /3 width=5/ used to work *)
   ]
 ]
 qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn_ltpss_sn.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn_ltpss_sn.ma
index 7aa2c5df2..10a190143 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn_ltpss_sn.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn_ltpss_sn.ma
@@ -23,7 +23,7 @@ include "basic_2/unfold/ltpss_sn_tpss.ma".
 fact ltpss_sn_tpss_trans_eq_aux: ∀Y1,X2,L1,T2,U2,d,e.
                                  L1 ⊢ T2 ▶* [d, e] U2 → ∀L0. L0 ⊢ ▶* [d, e] L1 →
                                  Y1 = L1 → X2 = T2 → L0 ⊢ T2 ▶* [d, e] U2.
-#Y1 #X2 @(cw_wf_ind … Y1 X2) -Y1 -X2 #Y1 #X2 #IH
+#Y1 #X2 @(fw_ind … Y1 X2) -Y1 -X2 #Y1 #X2 #IH
 #L1 #T2 #U2 #d #e #H @(tpss_ind_alt … H) -L1 -T2 -U2 -d -e
 [ //
 | #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #HV12 #HVW2 #_ #L0 #HL01 #H1 #H2 destruct
diff --git a/matita/matita/contribs/lambda_delta/ground_2/arith.ma b/matita/matita/contribs/lambda_delta/ground_2/arith.ma
index f7f5e35c4..ad3ab4a3d 100644
--- a/matita/matita/contribs/lambda_delta/ground_2/arith.ma
+++ b/matita/matita/contribs/lambda_delta/ground_2/arith.ma
@@ -69,13 +69,17 @@ lemma false_lt_to_le: ∀x,y. (x < y → ⊥) → y ≤ x.
 #Hxy elim (H Hxy)
 qed-.
 
-lemma plus_xySz_x_false: ∀z,x,y. x + y + S z = x → ⊥.
-#z #x elim x -x normalize
-[ #y <plus_n_Sm #H destruct
-| /3 width=2/
+lemma le_plus_xySz_x_false: ∀y,z,x. x + y + S z ≤ x → ⊥.
+#y #z #x elim x -x
+[ #H lapply (le_n_O_to_eq … H) -H
+  <plus_n_Sm #H destruct
+| /3 width=1 by le_S_S_to_le/
 ]
 qed-.
 
+lemma plus_xySz_x_false: ∀z,x,y. x + y + S z = x → ⊥.
+/2 width=4 by le_plus_xySz_x_false/ qed-.
+
 (* iterators ****************************************************************)
 
 (* Note: see also: lib/arithemetcs/bigops.ma *)
diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma
index 649108f47..06266a4b0 100644
--- a/matita/matita/lib/arithmetics/nat.ma
+++ b/matita/matita/lib/arithmetics/nat.ma
@@ -135,9 +135,6 @@ theorem injective_plus_r: ∀n:nat.injective nat nat (λm.n+m).
 theorem injective_plus_l: ∀n:nat.injective nat nat (λm.m+n). 
 /2/ qed.
 
-theorem not_eq_S: ∀n,m:nat. n ≠ m → S n ≠ S m.
-/2/ qed.
-
 theorem times_Sn_m: ∀n,m:nat. m+n*m = S n*m.
 // qed.
 
@@ -192,6 +189,9 @@ lemma plus_plus_comm_23: ∀x,y,z. x + y + z = x + z + y.
 
 (* Negated equalities *******************************************************)
 
+theorem not_eq_S: ∀n,m:nat. n ≠ m → S n ≠ S m.
+/2/ qed.
+
 theorem not_eq_O_S : ∀n:nat. 0 ≠ S n.
 #n @nmk #eqOS (change with (not_zero O)) >eqOS // qed.
 
@@ -299,6 +299,12 @@ theorem le_plus_to_minus_r: ∀a,b,c. a + b ≤ c → a ≤ c -b.
 #a #b #c #H @(le_plus_to_le_r … b) /2/
 qed.
 
+lemma lt_to_le: ∀x,y. x < y → x ≤ y.
+/2 width=2/ qed.
+
+lemma inv_eq_minus_O: ∀x,y. x - y = 0 → x ≤ y.
+// qed-.
+
 (* lt *)
 
 theorem transitive_lt: transitive nat lt.
@@ -600,6 +606,9 @@ lemma le_plus_compatible: ∀x1,x2,y1,y2. x1 ≤ y1 → x2 ≤ y2 → x1 + x2 
 #x1 #y1 #x2 #y2 #H1 #H2 /2/ @le_plus // /2/ /3 by le_minus_to_plus, monotonic_le_plus_r, transitive_le/ qed.
 *)
 
+lemma minus_le: ∀x,y. x - y ≤ x.
+/2 width=1/ qed.
+
 (* lt *)
 
 theorem not_eq_to_le_to_lt: ∀n,m. n≠m → n≤m → n<m.
@@ -679,6 +688,12 @@ qed.
 lemma minus_minus_m_m: ∀m,n. n ≤ m → m - (m - n) = n.
 /2 width=1/ qed.
 
+lemma discr_minus_x_xy: ∀x,y. x = x - y → x = 0 ∨ y = 0.
+* /2 width=1/ #x * /2 width=1/ #y normalize #H 
+lapply (minus_le x y) <H -H #H
+elim (not_le_Sn_n x) #H0 elim (H0 ?) //
+qed-.
+
 (* Stilll more atomic conclusion ********************************************)
 
 (* le *)
@@ -796,4 +811,3 @@ lemma le_maxr: ∀i,n,m. max n m ≤ i → m ≤ i.
 lemma to_max: ∀i,n,m. n ≤ i → m ≤ i → max n m ≤ i.
 #i #n #m #leni #lemi normalize (cases (leb n m)) 
 normalize // qed.
-
diff --git a/matita/matita/lib/basics/star.ma b/matita/matita/lib/basics/star.ma
index 2e3b775e4..aafb3fa6b 100644
--- a/matita/matita/lib/basics/star.ma
+++ b/matita/matita/lib/basics/star.ma
@@ -340,3 +340,74 @@ lemma bi_TC_star_ind_dx: ∀A,B,R. bi_reflexive A B R →
 #A #B #R #HR #a2 #b2 #P #H2 #IH #a1 #b1 #H12
 @(bi_TC_ind_dx … P ? IH … H12) /3 width=5/
 qed-.
+
+definition bi_star: ∀A,B,R. bi_relation A B ≝ λA,B,R,a1,b1,a2,b2.
+                    (a1 = a2 ∧ b1 = b2) ∨ bi_TC A B R a1 b1 a2 b2.
+
+lemma bi_star_bi_reflexive: ∀A,B,R. bi_reflexive A B (bi_star … R).
+/3 width=1/ qed.
+
+lemma bi_TC_to_bi_star: ∀A,B,R,a1,b1,a2,b2.
+                        bi_TC A B R a1 b1 a2 b2 → bi_star A B R a1 b1 a2 b2.
+/2 width=1/ qed.
+
+lemma bi_R_to_bi_star: ∀A,B,R,a1,b1,a2,b2.
+                       R a1 b1 a2 b2 → bi_star A B R a1 b1 a2 b2.
+/3 width=1/ qed.
+
+lemma bi_star_strap1: ∀A,B,R,a1,a,a2,b1,b,b2. bi_star A B R a1 b1 a b →
+                      R a b a2 b2 → bi_star A B R a1 b1 a2 b2.
+#A #B #R #a1 #a #a2 #b1 #b #b2 *
+[ * #H1 #H2 destruct /2 width=1/
+| /3 width=4/
+]
+qed.
+
+lemma bi_star_strap2: ∀A,B,R,a1,a,a2,b1,b,b2. R a1 b1 a b →
+                      bi_star A B R a b a2 b2 → bi_star A B R a1 b1 a2 b2.
+#A #B #R #a1 #a #a2 #b1 #b #b2 #H *
+[ * #H1 #H2 destruct /2 width=1/
+| /3 width=4/
+]
+qed.
+
+lemma bi_star_to_bi_TC_to_bi_TC: ∀A,B,R,a1,a,a2,b1,b,b2. bi_star A B R a1 b1 a b →
+                                 bi_TC A B R a b a2 b2 → bi_TC A B R a1 b1 a2 b2.
+#A #B #R #a1 #a #a2 #b1 #b #b2 *
+[ * #H1 #H2 destruct /2 width=1/
+| /2 width=4/
+]
+qed.
+
+lemma bi_TC_to_bi_star_to_bi_TC: ∀A,B,R,a1,a,a2,b1,b,b2. bi_TC A B R a1 b1 a b →
+                                 bi_star A B R a b a2 b2 → bi_TC A B R a1 b1 a2 b2.
+#A #B #R #a1 #a #a2 #b1 #b #b2 #H *
+[ * #H1 #H2 destruct /2 width=1/
+| /2 width=4/
+]
+qed.
+
+lemma bi_tansitive_bi_star: ∀A,B,R. bi_transitive A B (bi_star … R).
+#A #B #R #a1 #a #b1 #b #H #a2 #b2 *
+[ * #H1 #H2 destruct /2 width=1/
+| /3 width=4/
+]
+qed.
+
+lemma bi_star_ind: ∀A,B,R,a1,b1. ∀P:relation2 A B. P a1 b1 →
+                   (∀a,a2,b,b2. bi_star … R a1 b1 a b → R a b a2 b2 → P a b → P a2 b2) →
+                   ∀a2,b2. bi_star … R a1 b1 a2 b2 → P a2 b2.
+#A #B #R #a1 #b1 #P #H #IH #a2 #b2 *
+[ * #H1 #H2 destruct //
+| #H12 elim H12 -a2 -b2 /2 width=5/ -H /3 width=5/
+]
+qed-.
+
+lemma bi_star_ind_dx: ∀A,B,R,a2,b2. ∀P:relation2 A B. P a2 b2 →
+                      (∀a1,a,b1,b. R a1 b1 a b → bi_star … R a b a2 b2 → P a b → P a1 b1) →
+                      ∀a1,b1. bi_star … R a1 b1 a2 b2 → P a1 b1.
+#A #B #R #a2 #b2 #P #H #IH #a1 #b1 *
+[ * #H1 #H2 destruct //
+| #H12 @(bi_TC_ind_dx ?????????? H12) -a1 -b1 /2 width=5/ -H /3 width=5/
+]
+qed-.
diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml
index 4d86409b7..9818e64fe 100644
--- a/matita/matita/predefined_virtuals.ml
+++ b/matita/matita/predefined_virtuals.ml
@@ -1524,7 +1524,7 @@ let predefined_classes = [
  ["}"; "❵"; "⦄" ] ;
  ["□"; "◽"; "▪"; "◾"; ];
  ["◊"; "♢"; "⧫"; "♦"; "⟐"; "⟠"; ] ;
- [">"; "⭃"; "〉"; "»"; "❭"; "❯"; "❱"; "▸"; "►"; "▶"; ] ;
+ [">"; "⭃"; "⧁"; "〉"; "»"; "❭"; "❯"; "❱"; "▸"; "►"; "▶"; ] ;
  ["≥"; "≽"; "⥸"; ]; 
  ["a"; "α"; "𝕒"; "𝐚"; "𝛂"; "ⓐ"; ] ;
  ["A"; "ℵ"; "𝔸"; "𝐀"; "Ⓐ"; ] ;
-- 
2.39.2