From fec1a061eeca5e7e05b4f0c3e299983b163569c3 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 20 Jun 2012 18:50:32 +0000
Subject: [PATCH] - star.ma: constructor inj of star conflicts with previous
 constructor inj of TC. constructor inj of star renamed to sstep and
 constructor injl of starl renamed to sstepl - lambda_delta: bug fix in
 reduction rule tpr_zeta which now has the structure of like tpr_delta. More
 lemas towards subject reduction of native typing

---
 .../basic_2/computation/cprs_delift.ma        |   1 +
 .../basic_2/computation/cprs_lcprs.ma         |  16 ++-
 .../basic_2/computation/cprs_tstc.ma          |  10 +-
 .../basic_2/computation/cprs_tstc_vector.ma   |   8 +-
 .../basic_2/computation/csn_lcpr.ma           |  12 +-
 .../lambda_delta/basic_2/dynamic/nta_ltpr.ma  |  94 +++-----------
 .../lambda_delta/basic_2/dynamic/nta_sta.ma   |  37 +++---
 .../lambda_delta/basic_2/dynamic/nta_thin.ma  |   3 +-
 .../basic_2/equivalence/cpcs_cpcs.ma          |   4 +
 .../basic_2/equivalence/cpcs_delift.ma        |  47 +++++++
 .../lambda_delta/basic_2/reducibility/cpr.ma  |  20 ---
 .../basic_2/reducibility/cpr_cpr.ma           |   2 +-
 .../basic_2/reducibility/cpr_lift.ma          |  25 +++-
 .../basic_2/reducibility/ltpr_aaa.ma          |  14 +-
 .../basic_2/reducibility/ltpr_ldrop.ma        |   2 +-
 .../basic_2/reducibility/tnf_tif.ma           |   4 +-
 .../lambda_delta/basic_2/reducibility/tpr.ma  |  63 +++++----
 .../basic_2/reducibility/tpr_delift.ma        |   2 +-
 .../basic_2/reducibility/tpr_lift.ma          |  40 +++---
 .../basic_2/reducibility/tpr_tpr.ma           |  48 ++++---
 .../basic_2/reducibility/tpr_tpss.ma          |  31 ++---
 .../lambda_delta/basic_2/static/sta_lift.ma   |   6 +-
 .../lambda_delta/basic_2/static/sta_ltpss.ma  | 122 ++++++++++++++++++
 .../basic_2/substitution/lift_lift.ma         |   8 ++
 .../basic_2/substitution/lsubs_sfr.ma         |   5 +
 .../lambda_delta/basic_2/unfold/tpss_tpss.ma  |   8 +-
 .../lambda_delta/ground_2/xoa.conf.xml        |   2 +-
 .../contribs/lambda_delta/ground_2/xoa.ma     |  16 +--
 .../lambda_delta/ground_2/xoa_notation.ma     |  20 +--
 matita/matita/lib/basics/star.ma              |  12 +-
 30 files changed, 406 insertions(+), 276 deletions(-)
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/static/sta_ltpss.ma

diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_delift.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_delift.ma
index 3965d1619..5ce6bb59c 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_delift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_delift.ma
@@ -20,6 +20,7 @@ include "basic_2/computation/cprs.ma".
 
 (* Properties on inverse basic term relocation ******************************)
 
+(* Note: this should be stated with tprs *)
 lemma cprs_zeta_delift: ∀L,V,T1,T2. L.ⓓV ⊢ T1 ▼*[O, 1] ≡ T2 → L ⊢ ⓓV.T1 ➡* T2.
 #L #V #T1 #T2 * #T #HT1 #HT2
 @(cprs_strap2 … (ⓓV.T)) [ /3 width=3/ | @inj /3 width=3/ ] (**) (* explicit constructor, /5 width=3/ is too slow *)
diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lcprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lcprs.ma
index 1c9e28ad8..5efdb4fa2 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lcprs.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lcprs.ma
@@ -25,6 +25,10 @@ lemma lcprs_cprs_trans: ∀L1,L2. L1 ⊢ ➡* L2 →
 #L1 #L2 #HL12 @(lcprs_ind … HL12) -L2 // /3 width=3/
 qed.
 
+lemma lcprs_cpr_trans: ∀L1,L2. L1 ⊢ ➡* L2 →
+                       ∀T1,T2. L2 ⊢ T1 ➡ T2 → L1 ⊢ T1 ➡* T2.
+/3 width=3 by lcprs_cprs_trans, inj/ qed.
+
 (* Advanced inversion lemmas ************************************************)
 
 (* Basic_1: was pr3_gen_abbr *)
@@ -32,7 +36,7 @@ lemma cprs_inv_abbr1: ∀L,V1,T1,U2. L ⊢ ⓓV1. T1 ➡* U2 →
                       (∃∃V2,T2. L ⊢ V1 ➡* V2 & L. ⓓV1 ⊢ T1 ➡* T2 &
                                 U2 = ⓓV2. T2
                       ) ∨
-                      ∃∃U. ⇧[0, 1] U2 ≡ U & L. ⓓV1 ⊢ T1 ➡* U.
+                      ∃∃T2. L. ⓓV1 ⊢ T1 ➡* T2 & ⇧[0, 1] U2 ≡ T2.
 #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5/
 #U0 #U2 #_ #HU02 * *
 [ #V0 #T0 #HV10 #HT10 #H destruct
@@ -41,12 +45,12 @@ lemma cprs_inv_abbr1: ∀L,V1,T1,U2. L ⊢ ⓓV1. T1 ➡* U2 →
     lapply (cpr_intro … HV0 … HV2) -HV2 #HV02
     lapply (ltpr_cpr_trans (L.ⓓV0) … HT02) /2 width=1/ -V #HT02
     lapply (lcprs_cprs_trans (L. ⓓV1) … HT02) -HT02 /2 width=1/ /4 width=5/
-  | -V0 #T2 #HT20 #HTU2
-    elim (lift_total U2 0 1) #U0 #HU20
-    lapply (cpr_lift (L.ⓓV1) … HT20 … HU20 HTU2) -T2 /2 width=1/ /4 width=5/
+  | #T2 #HT02 #HUT2
+    lapply (lcprs_cpr_trans (L.ⓓV1) … HT02) -HT02 /2 width=1/ -V0 #HT02
+    lapply (cprs_trans … HT10 … HT02) -T0 /3 width=3/
   ]
-| #U1 #HU01 #HTU1
+| #U1 #HTU1 #HU01
   elim (lift_total U2 0 1) #U #HU2
-  lapply (cpr_lift (L.ⓓV1) … HU01 … HU2 HU02) -U0 /2 width=1/ /4 width=5/
+  lapply (cpr_lift (L.ⓓV1) … HU01 … HU2 HU02) -U0 /2 width=1/ /4 width=3/
 ]
 qed-.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc.ma
index eb59c5f84..879b0bdae 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc.ma
@@ -61,11 +61,11 @@ elim (cprs_inv_appl1 … H) -H *
 | #V0 #W #T0 #HV10 #HT0 #HU
   elim (cprs_inv_abbr1 … HT0) -HT0 *
   [ #V3 #T3 #_ #_ #H destruct
-  | #X #H #HT2
+  | #X #HT2 #H 
     elim (lift_inv_bind1 … H) -H #W2 #T2 #HW2 #HT02 #H destruct
     @or_intror @(cprs_trans … HU) -U (**) (* explicit constructor *)
     @(cprs_trans … (ⓓV.ⓐV2.ⓛW2.T2)) [ /3 width=1/ ] -T
-    @(cprs_strap2 … (ⓐV1.ⓛW.T0)) [ /5 width=3/ ] -V -V2 -W2 -T2
+    @(cprs_strap2 … (ⓐV1.ⓛW.T0)) [ /5 width=7/ ] -V -V2 -W2 -T2
     @(cprs_strap2 … (ⓓV1.T0)) [ /3 width=1/ ] -W /2 width=1/
   ]
 | #V3 #V4 #V0 #T0 #HV13 #HV34 #HT0 #HU
@@ -74,12 +74,12 @@ elim (cprs_inv_appl1 … H) -H *
   [ #V5 #T5 #HV5 #HT5 #H destruct
     lapply (cprs_lift (L.ⓓV) … HV12 … HV13 … HV34) -V1 -V3 /2 width=1/
     /3 width=1/
-  | #X #H #HT1
+  | #X #HT1 #H
     elim (lift_inv_bind1 … H) -H #V5 #T5 #HV05 #HT05 #H destruct
     lapply (cprs_lift (L.ⓓV0) … HV12 … HV13 … HV34) -V3 /2 width=1/ #HV24
     @(cprs_trans … (ⓓV.ⓐV2.ⓓV5.T5)) [ /3 width=1/ ] -T
-    @(cprs_strap2 … (ⓐV1.ⓓV0.T0)) [ /5 width=3/ ] -V -V5 -T5
-    @(cprs_strap2 … (ⓓV0.ⓐV2.T0)) [ /3 width=3/ ] -V1 /3 width=9/
+    @(cprs_strap2 … (ⓐV1.ⓓV0.T0)) [ /5 width=7/ ] -V -V5 -T5
+    @(cprs_strap2 … (ⓓV0.ⓐV2.T0)) [ /3 width=3/ ] -V1 /3 width=1/
   ]
 ]
 qed-.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc_vector.ma
index 5a4c2bc34..a6aedd799 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc_vector.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc_vector.ma
@@ -105,10 +105,10 @@ elim (cprs_inv_appl1 … H) -H *
     @(cprs_trans … HU) -U
     elim (cprs_inv_abbr1 … HT0) -HT0 *
     [ -HV12a -HV12b -HV10a #V1 #T1 #_ #_ #H destruct
-    | -V1b #X #H #HT1
+    | -V1b #X #HT1 #H
       elim (lift_inv_bind1 … H) -H #W1 #T1 #HW01 #HT01 #H destruct
       @(cprs_trans … (ⓓV.ⓐV2a.ⓛW1.T1)) [ /3 width=1/ ] -T -V2b -V2s
-      @(cprs_strap2 … (ⓐV1a.ⓛW0.T0)) [ /5 width=3/ ] -V -V2a -W1 -T1
+      @(cprs_strap2 … (ⓐV1a.ⓛW0.T0)) [ /5 width=7/ ] -V -V2a -W1 -T1
       @(cprs_strap2 … (ⓓV1a.T0)) [ /3 width=1/ ] -W0 /2 width=1/
     ]
   ]
@@ -122,11 +122,11 @@ elim (cprs_inv_appl1 … H) -H *
     [ #V1 #T1 #HV1 #HT1 #H destruct
       lapply (cprs_lift (L.ⓓV) … HV12a … HV10a … HV0a) -V1a -V0a [ /2 width=1/ ] #HV2a
       @(cprs_trans … (ⓓV.ⓐV2a.T1)) [ /3 width=1/ ] -T -V2b -V2s /3 width=1/
-    | #X #H #HT1
+    | #X #HT1 #H
       elim (lift_inv_bind1 … H) -H #V1 #T1 #HW01 #HT01 #H destruct
       lapply (cprs_lift (L.ⓓV0) … HV12a … HV10a … HV0a) -V0a [ /2 width=1/ ] #HV2a
       @(cprs_trans … (ⓓV.ⓐV2a.ⓓV1.T1)) [ /3 width=1/ ] -T -V2b -V2s
-      @(cprs_strap2 … (ⓐV1a.ⓓV0.T0)) [ /5 width=3/ ] -V -V1 -T1
+      @(cprs_strap2 … (ⓐV1a.ⓓV0.T0)) [ /5 width=7/ ] -V -V1 -T1
       @(cprs_strap2 … (ⓓV0.ⓐV2a.T0)) [ /3 width=3/ ] -V1a /3 width=1/
     ]
   ]
diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr.ma
index 3cd83733e..4b1b9d2fc 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr.ma
@@ -40,8 +40,9 @@ elim (cpr_inv_abbr1 … H1) -H1 *
     @(csn_lcpr_conf (L. ⓓV)) /2 width=1/ -HLV1 /2 width=3/
   | -IHV -HLV1 * #H destruct /3 width=1/
   ]
-| -IHV -IHT -H2 #T0 #HT0 #HLT0
-  lapply (csn_inv_lift … HT … HT0) -HT /2 width=3/
+| -IHV -IHT -H2 #T0 #HLT0 #HT0
+  lapply (csn_cpr_trans … HT … HLT0) -T #HLT0
+  lapply (csn_inv_lift … HLT0 … HT0) -T0 /2 width=3/
 ]
 qed.
 
@@ -99,9 +100,10 @@ elim (cpr_inv_appl1 … HL) -HL *
       lapply (ltpr_cpr_trans (L. ⓓV) … HLT3) /2 width=1/ -HLT3 #HLT3
       @(IHVT … H … HV05) -IHVT // -H -HV05 /3 width=1/
     ]
-  | -H -IHVT #T0 #HT0 #HLT0
-    @(csn_cpr_trans … (ⓐV1.T0)) /2 width=1/ -V0 -Y
-    @(csn_inv_lift … 0 1 HVT) /2 width=1/
+  | -H -IHVT #T0 #HLT0 #HT0
+    lapply (csn_cpr_trans … HVT (ⓐV2.T0) ?) /2 width=1/ -T #HVT0
+    lapply (csn_inv_lift L … 1 HVT0 ? ? ?) -HVT0 [ /2 width=4/ |2,3: skip | /2 width=1/ ] -V2 -T0 #HVY
+    @(csn_cpr_trans … HVY) /2 width=1/
   ]
 | -HV -HV12 -HVT -IHVT -H #V0 #W0 #T0 #T1 #_ #_ #H destruct
 | -IHVT -H #V0 #V3 #W0 #W1 #T0 #T1 #HLV10 #HLW01 #HLT01 #HV03 #H1 #H2 destruct
diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_ltpr.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_ltpr.ma
index 3799dcbb8..c461e9f7e 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_ltpr.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_ltpr.ma
@@ -12,94 +12,38 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* FRAGMENT 0 
-include "basic_2/unfold/delift_lift.ma".
-
-  
-include "basic_2/equivalence/cpcs_cpcs.ma".
-include "basic_2/unfold/delift_delift.ma".
-
-
-
-axiom pippo1: ∀T1,V. ∃∃T2. ⓓV.T1 ➡ T2 & ⋆.ⓓV ⊢ T1 ▼*[0, 1] ≡ T2.
-(*
-#T1 #V elim (pippo0 (⋆.ⓓV) 0 1 ? T1)
-[ #T2 #HT12 @(ex2_1_intro … HT12)
-  @tpr
-*)
-
-axiom pippo: ∀L,V,T1. ∃∃T2. L ⊢ ⓓV.T1 ➡ T2 & L.ⓓV ⊢ T1 ▼*[0, 1] ≡ T2.
-
-axiom cprs_inv_appl1_cpcs: ∀L,V1,T1,U2. L ⊢ ⓐV1. T1 ➡* U2 → (
-                           ∃∃V2,T2.  L ⊢ V1 ➡* V2 & L ⊢ T1 ➡* T2 &
-                                     L ⊢ U2 ➡* ⓐV2. T2
-                           ) ∨
-                           ∃∃V2,W,T. L ⊢ V1 ➡* V2 &
-                                     L ⊢ T1 ➡* ⓛW. T & L ⊢ ⓓV2. T ⬌* U2.
-#L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5/
-#U #U2 #_ #HU2 * *
-[ #V0 #T0 #HV10 #HT10 #HUT0
-  elim (cprs_strip … HUT0 … HU2) -U #U #H #HU2
-  elim (cpr_inv_appl1 … H) -H *
-  [ #V2 #T2 #HV02 #HT02 #H destruct /4 width=5/
-  | #V2 #W2 #T #T2 #HV02 #HT2 #H1 #H2 destruct
-    lapply (cprs_strap1 … HV10 HV02) -V0 #HV12
-    lapply (cprs_div ? (ⓓV2.T) ? ? ? HU2) -HU2 /2 width=1/ /3 width=6/
-  | #V #V2 #W0 #W2 #T #T2 #HV0 #HW02 #HT2 #HV2 #H1 #H2 destruct
-    lapply (cprs_strap1 … HV10 HV0) -V0 #HV1
-    lapply (cprs_trans … HT10 (ⓓW2.T2) ?) -HT10 /2 width=1/ -W0 -T #HT1
-    elim (pippo L W2 T2) #T3 #H1T3 #H2T3
-    elim (pippo L W2 (ⓐV2.T2)) #X #H1X #H
-    elim (delift_inv_flat1 … H) -H #V3 #Y #HV23 #HY #H destruct
-      
-  
-    @or_introl @(ex3_2_intro … HV1 HT1) -HV1 -HT1  
-      
-  ]
-| /4 width=8/
-]
-qed-.
-
-
-include "basic_2/computation/cprs_lcprs.ma".
+include "basic_2/equivalence/cpcs_delift.ma".
 include "basic_2/dynamic/nta.ma".
-
-axiom cprs_inv_appl_abst: ∀L,V,T,W,U. L ⊢ ⓐV.T ➡* ⓛW.U →
-                          ∃∃V0,W0,T0,W1,U1. ⇧[O, 1] W ≡ W1 &
-                                            ⇧[O + 1, 1] U ≡ U1 &
-                                            L ⊢ V ➡* V0 & L ⊢ T ➡* ⓛW0.T0 &
-                                            L.ⓓV0 ⊢ T0 ➡* ⓛW1.U1.
-#L #V #T #W #U #H
-elim (cprs_inv_appl1 … H) -H *
-[ #V0 #T0 #_ #_ #H destruct
-| #V0 #W0 #T0 #HV0 #HT0 #H
-  elim (cprs_inv_abbr1 … H) -H *
-  [ #V1 #T1 #_ #_ #H destruct
-  | #X #H #HT01
-    elim (lift_inv_bind1 … H) -H #W1 #U1 #HW1 #HU1 #H destruct /2 width=10/ 
-  ]
-| #V0 #V1 #V2 #T0 #HV0 #HV01 #HT0 #H
-  elim (cprs_inv_abbr1 … H) -H *
-  [ #V3 #T3 #_ #_ #H destruct
-  | #X #H #HT3
-    elim (lift_inv_bind1 … H) -H #W3 #U3 #HW3 #HU3 #H destruct /2 width=10/ 
-
-axiom pippo: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀X,Y. L ⊢ T ➡* ⓛX.Y →
+(*
+lemma pippo: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀X,Y. L ⊢ T ➡* ⓛX.Y →
              ∃Z. L ⊢ U ➡* ⓛX.Z.
 #h #L #T #U #H elim H -L -T -U
 [
 |
 |
 |
-|
-| #L #V #W #T #U #HTU #HUW #IHTU #IHUW #X #Y #HTY
-  elim (cprs_inv_appl1 … HTY) -HTY *
+| #L #V #W #T #U #_ #_ #IHVW #IHTU #X #Y #H  
+| #L #V #W #T #U #_ #HUW #IHTU #IHUW #X #Y #HTY
+  elim (cprs_inv_appl_abst … HTY) -HTY #W1 #T1 #W2 #T2 #HT1 #HT12 #HYT2
+  elim (IHTU … HT1) -IHTU -HT1 #U1 #HU1 
+ 
+  
+  
+   *
   [ #V0 #T0 #_ #_ #H destruct
   | #V0 #W0 #T0 #HV0 #HT0 #HTY
     elim (IHTU … HT0) -IHTU -HT0 #Z #HUZ
     elim (cprs_inv_abbr1 … HTY) -HTY *
     [ #V1 #T1 #_ #_ #H destruct #X0  
 
+*)
+
+(*
+
+include "basic_2/computation/cprs_lcprs.ma".
+
+
+
 
 include "basic_2/dynamic/nta_ltpss.ma".
 include "basic_2/dynamic/nta_thin.ma".
diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_sta.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_sta.ma
index d064d2e7d..6268b98b1 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_sta.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_sta.ma
@@ -13,35 +13,30 @@
 (**************************************************************************)
 
 include "basic_2/static/sta.ma".
-include "basic_2/dynamic/nta_lift.ma".
+include "basic_2/equivalence/cpcs_cpcs.ma".
+include "basic_2/dynamic/nta.ma".
 
 (* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************)
 
-axiom pippo: ∀h,L,X,Y1,U. ⦃h, L⦄ ⊢ ⓐX.Y1 : U → ∀Y2. L ⊢ Y1 ⬌* Y2 →
-             ∀U2. ⦃h, L⦄ ⊢ Y2 : U2 → ⦃h, L⦄ ⊢ ⓐX.Y2 : U.
-
 (* Properties on static type assignment *************************************)
 
 lemma nta_fwd_sta: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U →
-                   ∃∃U0. ⦃h, L⦄ ⊢ T • U0 & L ⊢ U0 ⬌* U & ⦃h, L⦄ ⊢ T : U0.
+                   ∃∃U0. ⦃h, L⦄ ⊢ T • U0 & L ⊢ U0 ⬌* U.
 #h #L #T #U #H elim H -L -T -U
-[ /2 width=4/
-| #L #K #V #W1 #V1 #i #HLK #_ #HWV1 * #W0 #H1VW0 #HW01 #H2VW0
+[ /2 width=3/
+| #L #K #V #W1 #V1 #i #HLK #_ #HWV1 * #W0 #HVW0 #HW01
   elim (lift_total W0 0 (i+1)) #V0 #HWV0
   lapply (ldrop_fwd_ldrop2 … HLK) #HLK0
-  lapply (cpcs_lift … HLK0 … HWV0 … HWV1 HW01) -HLK0 -HWV1 -HW01 /3 width=9/
-| #L #K #W #V1 #W1 #i #HLK #HWV1 #HW1 * /3 width=9/
-| #I #L #V #W #T #U #_ #_ * #W0 #_ #_ #H2VW0 * /3 width=4/
-| #L #V #W #T #U #_ #_ * #W0 #_ #HW0 #H2VW0 * #X #H1 #HX #H2
-  elim (sta_inv_bind1 … H1) -H1 #U0 #HTU0 #H destruct
-  elim (nta_inv_bind1 … H2) /4 width=4/
-| #L #V #W #T #U #_ #_ * #U0 #H1TU0 #HU0 #H2TU0 * #W0 #_ #_ #H2UW0 -W
-  elim (nta_fwd_correct … H2TU0) #T0 #HUT0
-  @(ex3_1_intro … (ⓐV.U0)) /2 width=1/ -H1TU0
-  @(nta_pure … W0 … H2TU0) -T /3 width=3/
-| #L #T #U #HTU * #U0 #H1TU0 #HU0 #H2TU0
-  elim (nta_fwd_correct … H2TU0) -H2TU0 /4 width=8/
-| #L #T #U1 #U2 #V2 #_ #HU12 #_ * #U0 #H1TU0 #HU01 #H2TU0 #_
-  lapply (cpcs_trans … HU01 … HU12) -U1 /2 width=4/
+  lapply (cpcs_lift … HLK0 … HWV0 … HWV1 HW01) -HLK0 -HWV1 -HW01 /3 width=6/
+| #L #K #W #V1 #W1 #i #HLK #HWV1 #HW1 * /3 width=6/
+| #I #L #V #W #T #U #_ #_ * #W0 #_ #_ * /3 width=3/
+| #L #V #W #T #U #_ #_ * #W0 #_ #HW0 * #X #H #HX
+  elim (sta_inv_bind1 … H) -H #U0 #HTU0 #H destruct
+  @(ex2_1_intro … (ⓐV.ⓛW.U0)) /2 width=1/ /3 width=1/
+| #L #V #W #T #U #_ #_ * #U0 #HTU0 #HU0 #_ -W
+  @(ex2_1_intro … (ⓐV.U0)) /2 width=1/
+| #L #T #U #HTU * #U0 #HTU0 #HU0 /3 width=3/
+| #L #T #U1 #U2 #V2 #_ #HU12 #_ * #U0 #HTU0 #HU01 #_
+  lapply (cpcs_trans … HU01 … HU12) -U1 /2 width=3/
 ]
 qed-.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_thin.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_thin.ma
index e2e568d3a..f927f841a 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_thin.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_thin.ma
@@ -12,14 +12,13 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/unfold/delift_lift.ma".
 include "basic_2/unfold/thin_ldrop.ma".
 include "basic_2/equivalence/cpcs_delift.ma".
 include "basic_2/dynamic/nta_lift.ma".
 
 (* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************)
 
-(* Properties on basic local environment thibbing ***************************)
+(* Properties on basic local environment thinning ***************************)
 
 (* Note: this is known as the substitution lemma *)
 (* Basic_1: was only: ty3_gen_cabbr *)
diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma
index d67e66630..fcad182e0 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma
@@ -73,6 +73,10 @@ elim (cprs_inv_abst1 Abst W1 … H1) -H1 #W2 #T2 #HW12 #HT12 #H destruct
 @(ex2_2_intro … H2) -H2 /2 width=2/ (**) (* explicit constructor, /3 width=6/ is slow *)
 qed-.
 
+lemma cpcs_inv_abst2: ∀L,W1,T1,T. L ⊢ T ⬌* ⓛW1.T1 →
+                      ∃∃W2,T2. L ⊢ T ➡* ⓛW2.T2 & L ⊢ ⓛW1.T1 ➡* ⓛW2.T2.
+/3 width=1 by cpcs_inv_abst1, cpcs_sym/ qed-.
+
 (* Basic_1: was: pc3_gen_lift *)
 lemma cpcs_inv_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K →
                      ∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀T2,U2. ⇧[d, e] T2 ≡ U2 →
diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_delift.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_delift.ma
index b812830ee..c568941a5 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_delift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_delift.ma
@@ -12,12 +12,59 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basic_2/unfold/delift_lift.ma".
 include "basic_2/unfold/delift_delift.ma".
 include "basic_2/computation/cprs_delift.ma".
 include "basic_2/equivalence/cpcs_cpcs.ma".
 
 (* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************)
 
+(* Advanced inversion lemmas ************************************************)
+
+lemma cprs_inv_appl1_cpcs: ∀L,V1,T1,U2. L ⊢ ⓐV1. T1 ➡* U2 → (
+                           ∃∃V2,T2.  L ⊢ V1 ➡* V2 & L ⊢ T1 ➡* T2 &
+                                     L ⊢ U2 ➡* ⓐV2. T2
+                           ) ∨
+                           ∃∃V2,W,T. L ⊢ V1 ➡* V2 &
+                                     L ⊢ T1 ➡* ⓛW. T & L ⊢ ⓓV2. T ⬌* U2.
+#L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5/
+#U #U2 #_ #HU2 * *
+[ #V0 #T0 #HV10 #HT10 #HUT0
+  elim (cprs_strip … HUT0 … HU2) -U #U #H #HU2
+  elim (cpr_inv_appl1 … H) -H *
+  [ #V2 #T2 #HV02 #HT02 #H destruct /4 width=5/
+  | #V2 #W2 #T #T2 #HV02 #HT2 #H1 #H2 destruct
+    lapply (cprs_strap1 … HV10 HV02) -V0 #HV12
+    lapply (cprs_div ? (ⓓV2.T) ? ? ? HU2) -HU2 /2 width=1/ /3 width=6/
+  | #V #V2 #W0 #W2 #T #T2 #HV0 #HW02 #HT2 #HV2 #H1 #H2 destruct
+    lapply (cprs_strap1 … HV10 HV0) -V0 #HV1
+    lapply (cprs_trans … HT10 (ⓓW2.T2) ?) -HT10 /2 width=1/ -W0 -T #HT1
+    elim (sfr_delift (L.ⓓW2) (ⓐV2.T2) 0 1 ? ?) // #X #H1
+    lapply (cprs_zeta_delift … H1) #H2
+    lapply (cprs_trans … HU2 … H2) -HU2 -H2 #HU2T3
+    elim (delift_inv_flat1 … H1) -H1 #V3 #T3 #HV23 #HT23 #H destruct
+    lapply (delift_inv_lift1_eq … HV23 … HV2) -V2 [ /2 width=1/ | skip ] #H destruct
+    lapply (cprs_zeta_delift … HT23) -HT23 #H
+    lapply (cprs_trans … HT1 … H) -W2 -T2 /3 width=5/
+  ]
+| /4 width=8/
+]
+qed-.
+
+lemma cprs_inv_appl_abst: ∀L,V,T,W,U. L ⊢ ⓐV.T ➡* ⓛW.U →
+                          ∃∃W0,T0,V1,T1. L ⊢ T ➡* ⓛW0.T0 &
+                                         L ⊢ ⓓV.T0 ➡* ⓛV1.T1 &
+                                         L ⊢ ⓛW.U ➡* ⓛV1.T1.
+#L #V #T #W #U #H
+elim (cprs_inv_appl1_cpcs … H) -H *
+[ #V0 #T0 #HV0 #HT0 #H
+  elim (cprs_inv_abst1 Abst W … H) -H #W0 #U0 #_ #_ #H destruct
+| #V0 #W0 #T0 #HV0 #HT0 #H
+  elim (cpcs_inv_abst2 … H) -H #V1 #T1 #H1 #H2
+  lapply (cprs_trans … (ⓓV.T0) … H1) -H1 /2 width=1/ -V0 /2 width=7/
+]
+qed-.
+
 (* Properties on inverse basic term relocation ******************************)
 
 lemma cpcs_zeta_delift_comm: ∀L,V,T1,T2. L.ⓓV ⊢ T1 ▼*[O, 1] ≡ T2 →
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma
index 401a4be64..5a572d5e1 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma
@@ -75,26 +75,6 @@ lemma cpr_inv_sort1: ∀L,T2,k. L ⊢ ⋆k ➡ T2 → T2 = ⋆k.
 >(tpss_inv_sort1 … H) -H //
 qed-.
 
-(* Basic_1: was pr2_gen_abbr *)
-lemma cpr_inv_abbr1: ∀L,V1,T1,U2. L ⊢ ⓓV1. T1 ➡ U2 →
-                     (∃∃V,V2,T2. V1 ➡ V & L ⊢ V ▶* [O, |L|] V2 &
-                                 L. ⓓV ⊢ T1 ➡ T2 &
-                                 U2 = ⓓV2. T2
-                      ) ∨
-                      ∃∃T. ⇧[0,1] T ≡ T1 & L ⊢ T ➡ U2.
-#L #V1 #T1 #Y * #X #H1 #H2
-elim (tpr_inv_abbr1 … H1) -H1 *
-[ #V #T0 #T #HV1 #HT10 #HT0 #H destruct
-  elim (tpss_inv_bind1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H destruct
-  lapply (tps_lsubs_trans … HT0 (L. ⓓV) ?) -HT0 /2 width=1/ #HT0
-  lapply (tps_weak_all … HT0) -HT0 #HT0
-  lapply (tpss_lsubs_trans … HT2 (L. ⓓV) ?) -HT2 /2 width=1/ #HT2
-  lapply (tpss_weak_all … HT2) -HT2 #HT2
-  lapply (tpss_strap … HT0 HT2) -T /4 width=7/
-| /4 width=5/
-]
-qed-.
-
 (* Basic_1: was: pr2_gen_cast *)
 lemma cpr_inv_cast1: ∀L,V1,T1,U2. L ⊢ ⓝV1. T1 ➡ U2 → (
                         ∃∃V2,T2. L ⊢ V1 ➡ V2 & L ⊢ T1 ➡ T2 &
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_cpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_cpr.ma
index 583726cd4..87eaa161f 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_cpr.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_cpr.ma
@@ -31,7 +31,7 @@ lemma cpr_bind_dx: ∀I,L,V1,V2,T1,T2. V1 ➡ V2 → L. ⓑ{I} V2 ⊢ T1 ➡ T2
 #I #L #V1 #V2 #T1 #T2 #HV12 * #T #HT1 normalize #HT2
 elim (tpss_split_up … HT2 1 ? ?) -HT2 // #T0 <minus_n_O #HT0 normalize <minus_plus_m_m #HT02
 lapply (tpss_lsubs_trans … HT0 (⋆. ⓑ{I} V2) ?) -HT0 /2 width=1/ #HT0
-lapply (tpss_tps … HT0) -HT0 #HT0
+lapply (tpss_inv_SO2 … HT0) -HT0 #HT0
 @ex2_1_intro [2: @(tpr_delta … HV12 HT1 HT0) | skip | /2 width=1/ ] (**) (* /3 width=5/ is too slow *)
 qed.
 
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma
index 6db1a47aa..068a5f751 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma
@@ -63,6 +63,29 @@ elim (tpss_inv_lref1 … H) -H /2 width=1/
 * /3 width=6/
 qed-.
 
+(* Basic_1: was pr2_gen_abbr *)
+lemma cpr_inv_abbr1: ∀L,V1,T1,U2. L ⊢ ⓓV1. T1 ➡ U2 →
+                     (∃∃V,V2,T2. V1 ➡ V & L ⊢ V ▶* [O, |L|] V2 &
+                                 L. ⓓV ⊢ T1 ➡ T2 &
+                                 U2 = ⓓV2. T2
+                      ) ∨
+                      ∃∃T2. L.ⓓV1 ⊢ T1 ➡ T2 & ⇧[0,1] U2 ≡ T2.
+#L #V1 #T1 #Y * #X #H1 #H2
+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_lsubs_trans … HT0 (L. ⓓV) ?) -HT0 /2 width=1/ #HT0
+  lapply (tps_weak_all … HT0) -HT0 #HT0
+  lapply (tpss_lsubs_trans … HT02 (L. ⓓV) ?) -HT02 /2 width=1/ #HT02
+  lapply (tpss_weak_all … HT02) -HT02 #HT02
+  lapply (tpss_strap … HT0 HT02) -T0 /4 width=7/
+| #T2 #HT12 #HXT2
+  elim (lift_total Y 0 1) #Z #HYZ
+  lapply (tpss_lift_ge … H2 (L.ⓓV1) … HXT2 … HYZ) -X // /2 width=1/ #H
+  lapply (cpr_intro … HT12 … H) -T2 /3 width=3/
+]
+qed-.
+
 (* Basic_1: was: pr2_gen_abst *)
 lemma cpr_inv_abst1: ∀L,V1,T1,U2. L ⊢ ⓛV1. T1 ➡ U2 → ∀I,W.
                      ∃∃V2,T2. L ⊢ V1 ➡ V2 & L. ⓑ{I} W ⊢ T1 ➡ T2 & U2 = ⓛV2. T2.
@@ -132,7 +155,7 @@ lemma cpr_inv_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K →
                     ∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀U2. L ⊢ U1 ➡ U2 →
                     ∃∃T2. ⇧[d, e] T2 ≡ U2 & K ⊢ T1 ➡ T2.
 #L #K #d #e #HLK #T1 #U1 #HTU1 #U2 * #U #HU1 #HU2
-elim (tpr_inv_lift … HU1 … HTU1) -U1 #T #HTU #T1
+elim (tpr_inv_lift1 … HU1 … HTU1) -U1 #T #HTU #T1
 elim (lt_or_ge (|L|) d) #HLd
 [ elim (tpss_inv_lift1_le … HU2 … HLK … HTU ?) -U -HLK [ /5 width=4/ | /2 width=2/ ]
 | elim (lt_or_ge (|L|) (d + e)) #HLde
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma
index a7d12a5e2..45cde4dc3 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma
@@ -34,15 +34,13 @@ fact aaa_ltpr_tpr_conf_aux: ∀L,T,L1,T1,A. L1 ⊢ T1 ⁝ A → L = L1 → T = T
   lapply (IH … HKV1 … HK1 … HK12 … HV12) // -L1 -K1 -V1 /2 width=5/
 | #L1 #V1 #T1 #B #A #HB #HA #H1 #H2 #L2 #HL12 #X #H destruct
   elim (tpr_inv_abbr1 … H) -H *
-  [ #V2 #T0 #T2 #HV12 #HT10 #HT02 #H destruct
-    lapply (tps_lsubs_trans … HT02 (L2.ⓓV2) ?) -HT02 /2 width=1/ #HT02
+  [ #V2 #T #T2 #HV12 #HT1 #HT2 #H destruct
+    lapply (tps_lsubs_trans … HT2 (L2.ⓓV2) ?) -HT2 /2 width=1/ #HT2
     lapply (IH … HB … HL12 … HV12) -HB /width=5/ #HB
-    lapply (IH … HA … (L2.ⓓV2) … HT10) -IH -HA -HT10 /width=5/ -T1 /2 width=1/ -L1 -V1 /3 width=5/
-  | -B #T #HT1 #HTX
-    elim (lift_total X 0 1) #X1 #HX1
-    lapply (tpr_lift … HTX … HT1 … HX1) -T #HTX1
-    lapply (IH … HA … (L2.ⓓV1) … HTX1) /width=5/ -T1 /2 width=1/ -L1 #HA
-    @(aaa_inv_lift … HA … HX1) /2 width=1/
+    lapply (IH … HA … (L2.ⓓV2) … HT1) -IH -HA -HT1 /width=5/ -T1 /2 width=1/ -L1 -V1 /3 width=5/
+  | -B #T #HT1 #HXT
+    lapply (IH … HA … (L2.ⓓV1) … HT1) /width=5/ -T1 /2 width=1/ -L1 #HA
+    @(aaa_inv_lift … HA … HXT) /2 width=1/
   ]
 | #L1 #V1 #T1 #B #A #HB #HA #H1 #H2 #L2 #HL12 #X #H destruct
   elim (tpr_inv_abst1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ldrop.ma
index bb9195138..91ba46c60 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ldrop.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ldrop.ma
@@ -29,7 +29,7 @@ lemma ltpr_ldrop_conf: ∀L1,K1,d,e. ⇩[d, e] L1 ≡ K1 → ∀L2. L1 ➡ L2 
   elim (IHLK1 … HL12) -L1 /3 width=3/
 | #L1 #K1 #I #V1 #W1 #d #e #_ #HWV1 #IHLK1 #X #H
   elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct
-  elim (tpr_inv_lift … HV12 … HWV1) -V1
+  elim (tpr_inv_lift1 … HV12 … HWV1) -V1
   elim (IHLK1 … HL12) -L1 /3 width=5/
 ]
 qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf_tif.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf_tif.ma
index 2a8ea3c49..7b6ed1dc7 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf_tif.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf_tif.ma
@@ -40,9 +40,9 @@ lemma tpr_tif_eq: ∀T1,T2. T1 ➡ T2 →  𝐈⦃T1⦄ → T1 = T2.
 | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #H
   elim (tif_inv_appl … H) -H #_ #_ #H
   elim (simple_inv_bind … H)
-| #V1 #T1 #T2 #T #_ #_ #_ #H
+| #V1 #T1 #T #T2 #_ #_ #_ #H
   elim (tif_inv_abbr … H)
-| #V1 #T1 #T #_ #_ #H
+| #V1 #T1 #T2 #_ #_ #H
   elim (tif_inv_cast … H)
 ]
 qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma
index 79d8df114..20508df5f 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma
@@ -23,13 +23,13 @@ inductive tpr: relation term ≝
              tpr (ⓕ{I} V1. T1) (ⓕ{I} V2. T2)
 | tpr_beta : ∀V1,V2,W,T1,T2.
              tpr V1 V2 → tpr T1 T2 → tpr (ⓐV1. ⓛW. T1) (ⓓV2. T2)
-| tpr_delta: ∀I,V1,V2,T1,T2,T.
-             tpr V1 V2 → tpr T1 T2 → ⋆. ⓑ{I} V2 ⊢ T2 ▶ [0, 1] T →
-             tpr (ⓑ{I} V1. T1) (ⓑ{I} V2. T)
+| tpr_delta: ∀I,V1,V2,T1,T,T2.
+             tpr V1 V2 → tpr T1 T → ⋆. ⓑ{I} V2 ⊢ T ▶ [0, 1] T2 →
+             tpr (ⓑ{I} V1. T1) (ⓑ{I} V2. T2)
 | tpr_theta: ∀V,V1,V2,W1,W2,T1,T2.
              tpr V1 V2 → ⇧[0,1] V2 ≡ V → tpr W1 W2 → tpr T1 T2 →
              tpr (ⓐV1. ⓓW1. T1) (ⓓW2. ⓐV. T2)
-| tpr_zeta : ∀V,T,T1,T2. ⇧[0,1] T1 ≡ T → tpr T1 T2 → tpr (ⓓV. T) T2
+| tpr_zeta : ∀V,T1,T,T2. tpr T1 T → ⇧[0, 1] T2 ≡ T → tpr (ⓓV. T1) T2
 | tpr_tau  : ∀V,T1,T2. tpr T1 T2 → tpr (ⓝV. T1) T2
 .
 
@@ -55,9 +55,9 @@ fact tpr_inv_atom1_aux: ∀U1,U2. U1 ➡ U2 → ∀I. U1 = ⓪{I} → U2 = ⓪{I
 [ //
 | #I #V1 #V2 #T1 #T2 #_ #_ #k #H destruct
 | #V1 #V2 #W #T1 #T2 #_ #_ #k #H destruct
-| #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #k #H destruct
+| #I #V1 #V2 #T1 #T #T2 #_ #_ #_ #k #H destruct
 | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #k #H destruct
-| #V #T #T1 #T2 #_ #_ #k #H destruct
+| #V #T1 #T #T2 #_ #_ #k #H destruct
 | #V #T1 #T2 #_ #k #H destruct
 ]
 qed.
@@ -67,37 +67,37 @@ lemma tpr_inv_atom1: ∀I,U2. ⓪{I} ➡ U2 → U2 = ⓪{I}.
 /2 width=3/ qed-.
 
 fact tpr_inv_bind1_aux: ∀U1,U2. U1 ➡ U2 → ∀I,V1,T1. U1 = ⓑ{I} V1. T1 →
-                        (∃∃V2,T2,T. V1 ➡ V2 & T1 ➡ T2 &
-                                    ⋆.  ⓑ{I} V2 ⊢ T2 ▶ [0, 1] T &
-                                    U2 = ⓑ{I} V2. T
+                        (∃∃V2,T,T2. V1 ➡ V2 & T1 ➡ T &
+                                    ⋆.  ⓑ{I} V2 ⊢ T ▶ [0, 1] T2 &
+                                    U2 = ⓑ{I} V2. T2
                         ) ∨
-                        ∃∃T. ⇧[0,1] T ≡ T1 & T ➡ U2 & I = Abbr.
+                        ∃∃T. T1 ➡ T & ⇧[0, 1] U2 ≡ T & I = Abbr.
 #U1 #U2 * -U1 -U2
 [ #J #I #V #T #H destruct
 | #I1 #V1 #V2 #T1 #T2 #_ #_ #I #V #T #H destruct
 | #V1 #V2 #W #T1 #T2 #_ #_ #I #V #T #H destruct
-| #I1 #V1 #V2 #T1 #T2 #T #HV12 #HT12 #HT2 #I0 #V0 #T0 #H destruct /3 width=7/
+| #I1 #V1 #V2 #T1 #T #T2 #HV12 #HT1 #HT2 #I0 #V0 #T0 #H destruct /3 width=7/
 | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #I0 #V0 #T0 #H destruct
-| #V #T #T1 #T2 #HT1 #HT12 #I0 #V0 #T0 #H destruct /3 width=3/
+| #V #T1 #T #T2 #HT1 #HT2 #I0 #V0 #T0 #H destruct /3 width=3/
 | #V #T1 #T2 #_ #I0 #V0 #T0 #H destruct
 ]
 qed.
 
 lemma tpr_inv_bind1: ∀V1,T1,U2,I. ⓑ{I} V1. T1 ➡ U2 →
-                     (∃∃V2,T2,T. V1 ➡ V2 & T1 ➡ T2 &
-                                 ⋆.  ⓑ{I} V2 ⊢ T2 ▶ [0, 1] T &
-                                 U2 = ⓑ{I} V2. T
+                     (∃∃V2,T,T2. V1 ➡ V2 & T1 ➡ T &
+                                 ⋆.  ⓑ{I} V2 ⊢ T ▶ [0, 1] T2 &
+                                 U2 = ⓑ{I} V2. T2
                      ) ∨
-                     ∃∃T. ⇧[0,1] T ≡ T1 & T ➡ U2 & I = Abbr.
+                     ∃∃T. T1 ➡ T & ⇧[0,1] U2 ≡ T & I = Abbr.
 /2 width=3/ qed-.
 
 (* Basic_1: was pr0_gen_abbr *)
 lemma tpr_inv_abbr1: ∀V1,T1,U2. ⓓV1. T1 ➡ U2 →
-                     (∃∃V2,T2,T. V1 ➡ V2 & T1 ➡ T2 &
-                                 ⋆.  ⓓV2 ⊢ T2 ▶ [0, 1] T &
-                                 U2 = ⓓV2. T
+                     (∃∃V2,T,T2. V1 ➡ V2 & T1 ➡ T &
+                                 ⋆.  ⓓV2 ⊢ T ▶ [0, 1] T2 &
+                                 U2 = ⓓV2. T2
                       ) ∨
-                      ∃∃T. ⇧[0,1] T ≡ T1 & T ➡ U2.
+                      ∃∃T. T1 ➡ T & ⇧[0, 1] U2 ≡ T.
 #V1 #T1 #U2 #H
 elim (tpr_inv_bind1 … H) -H * /3 width=7/
 qed-.
@@ -118,9 +118,9 @@ fact tpr_inv_flat1_aux: ∀U1,U2. U1 ➡ U2 → ∀I,V1,U0. U1 = ⓕ{I} V1. U0 
 [ #I #J #V #T #H destruct
 | #I #V1 #V2 #T1 #T2 #HV12 #HT12 #J #V #T #H destruct /3 width=5/
 | #V1 #V2 #W #T1 #T2 #HV12 #HT12 #J #V #T #H destruct /3 width=8/
-| #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #J #V0 #T0 #H destruct
+| #I #V1 #V2 #T1 #T #T2 #_ #_ #_ #J #V0 #T0 #H destruct
 | #V #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HV2 #HW12 #HT12 #J #V0 #T0 #H destruct /3 width=12/
-| #V #T #T1 #T2 #_ #_ #J #V0 #T0 #H destruct
+| #V #T1 #T #T2 #_ #_ #J #V0 #T0 #H destruct
 | #V #T1 #T2 #HT12 #J #V0 #T0 #H destruct /3 width=1/
 ]
 qed.
@@ -180,26 +180,25 @@ elim (tpr_inv_flat1 … H) -H * /3 width=5/
 qed-.
 
 fact tpr_inv_lref2_aux: ∀T1,T2. T1 ➡ T2 → ∀i. T2 = #i →
-                        ∨∨           T1 = #i
-                         | ∃∃V,T,T0. ⇧[O,1] T0 ≡ T & T0 ➡ #i &
-                                     T1 = ⓓV. T
-                         | ∃∃V,T.    T ➡ #i & T1 = ⓝV. T.
+                        ∨∨        T1 = #i
+                         | ∃∃V,T. T ➡ #(i+1) & T1 = ⓓV. T
+                         | ∃∃V,T. T ➡ #i & T1 = ⓝV. T.
 #T1 #T2 * -T1 -T2
 [ #I #i #H destruct /2 width=1/
 | #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct
 | #V1 #V2 #W #T1 #T2 #_ #_ #i #H destruct
-| #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #i #H destruct
+| #I #V1 #V2 #T1 #T #T2 #_ #_ #_ #i #H destruct
 | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #i #H destruct
-| #V #T #T1 #T2 #HT1 #HT12 #i #H destruct /3 width=6/
+| #V #T1 #T #T2 #HT1 #HT2 #i #H destruct
+  lapply (lift_inv_lref1_ge … HT2 ?) -HT2 // #H destruct /3 width=4/
 | #V #T1 #T2 #HT12 #i #H destruct /3 width=4/
 ]
 qed.
 
 lemma tpr_inv_lref2: ∀T1,i. T1 ➡ #i →
-                     ∨∨           T1 = #i
-                      | ∃∃V,T,T0. ⇧[O,1] T0 ≡ T & T0 ➡ #i &
-                                  T1 = ⓓV. T
-                      | ∃∃V,T.    T ➡ #i & T1 = ⓝV. T.
+                     ∨∨        T1 = #i
+                      | ∃∃V,T. T ➡ #(i+1) & T1 = ⓓV. T
+                      | ∃∃V,T. T ➡ #i & T1 = ⓝV. T.
 /2 width=3/ qed-.
 
 (* Basic_1: removed theorems 3:
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_delift.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_delift.ma
index 762640521..ade2050e3 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_delift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_delift.ma
@@ -23,5 +23,5 @@ lemma tpr_delift_conf: ∀U1,U2. U1 ➡ U2 → ∀L,T1,d,e. L ⊢ U1 ▼*[d, e]
                        ∃∃T2. T1 ➡ T2 & L ⊢ U2 ▼*[d, e] ≡ T2.
 #U1 #U2 #HU12 #L #T1 #d #e * #W1 #HUW1 #HTW1
 elim (tpr_tpss_conf … HU12 … HUW1) -U1 #U1 #HWU1 #HU21
-elim (tpr_inv_lift … HWU1 … HTW1) -W1 /3 width=5/
+elim (tpr_inv_lift1 … HWU1 … HTW1) -W1 /3 width=5/
 qed. 
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_lift.ma
index c55894034..1c1248526 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_lift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_lift.ma
@@ -36,30 +36,30 @@ lemma tpr_lift: ∀T1,T2. T1 ➡ T2 →
   elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct
   elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct
   elim (lift_inv_bind1 … HX2) -HX2 #V3 #T3 #HV23 #HT23 #HX2 destruct /3 width=4/
-| #I #V1 #V2 #T1 #T2 #T0 #HV12 #HT12 #HT2 #IHV12 #IHT12 #d #e #X1 #HX1 #X2 #HX2
+| #I #V1 #V2 #T1 #T #T2 #_ #_ #HT2 #IHV12 #IHT1 #d #e #X1 #HX1 #X2 #HX2
   elim (lift_inv_bind1 … HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct
   elim (lift_inv_bind1 … HX2) -HX2 #W2 #U0 #HVW2 #HTU0 #HX2 destruct
-  elim (lift_total T2 (d + 1) e) #U2 #HTU2
+  elim (lift_total T (d + 1) e) #U #HTU
   @tpr_delta
-  [4: @(tps_lift_le … HT2 … HTU2 HTU0 ?) /2 width=1/ |1: skip |2: /2 width=4/ |3: /2 width=4/ ] (**) (*/3. is too slow *)
+  [4: @(tps_lift_le … HT2 … HTU HTU0 ?) /2 width=1/ |1: skip |2: /2 width=4/ |3: /2 width=4/ ] (**) (*/3. is too slow *)
 | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #d #e #X1 #HX1 #X2 #HX2
   elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct
   elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct
   elim (lift_inv_bind1 … HX2) -HX2 #W3 #X #HW23 #HX #HX2 destruct
   elim (lift_inv_flat1 … HX) -HX #V3 #T3 #HV3 #HT23 #HX destruct
   elim (lift_trans_ge … HV2 … HV3 ?) -V // /3 width=4/
-| #V #T #T1 #T2 #HT1 #_ #IHT12 #d #e #X #HX #T0 #HT20
-  elim (lift_inv_bind1 … HX) -HX #V3 #T3 #_ #HT3 #HX destruct
-  elim (lift_trans_ge … HT1 … HT3 ?) -T // /3 width=6/
+| #V #T1 #T #T2 #_ #HT2 #IHT1 #d #e #X #H #U2 #HTU2
+  elim (lift_inv_bind1 … H) -H #V3 #T3 #_ #HT13 #H destruct -V
+  elim (lift_conf_O1 … HTU2 … HT2) -T2 /3 width=4/
 | #V #T1 #T2 #_ #IHT12 #d #e #X #HX #T #HT2
   elim (lift_inv_flat1 … HX) -HX #V0 #T0 #_ #HT0 #HX destruct /3 width=4/
 ]
 qed.
 
 (* Basic_1: was: pr0_gen_lift *)
-lemma tpr_inv_lift: ∀T1,T2. T1 ➡ T2 →
-                    ∀d,e,U1. ⇧[d, e] U1 ≡ T1 →
-                    ∃∃U2. ⇧[d, e] U2 ≡ T2 & U1 ➡ U2.
+lemma tpr_inv_lift1: ∀T1,T2. T1 ➡ T2 →
+                     ∀d,e,U1. ⇧[d, e] U1 ≡ T1 →
+                     ∃∃U2. ⇧[d, e] U2 ≡ T2 & U1 ➡ U2.
 #T1 #T2 #H elim H -T1 -T2
 [ * #i #d #e #U1 #HU1
   [ lapply (lift_inv_sort2 … HU1) -HU1 #H destruct /2 width=3/
@@ -75,11 +75,11 @@ lemma tpr_inv_lift: ∀T1,T2. T1 ➡ T2 →
   elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct
   elim (IHV12 … HV01) -V1
   elim (IHT12 … HT01) -T1 /3 width=5/
-| #I #V1 #V2 #T1 #T2 #T0 #_ #_ #HT20 #IHV12 #IHT12 #d #e #X #HX
+| #I #V1 #V2 #T1 #T #T2 #_ #_ #HT2 #IHV12 #IHT1 #d #e #X #HX
   elim (lift_inv_bind2 … HX) -HX #W1 #U1 #HWV1 #HUT1 #HX destruct
   elim (IHV12 … HWV1) -V1 #W2 #HWV2 #HW12
-  elim (IHT12 … HUT1) -T1 #U2 #HUT2 #HU12
-  elim (tps_inv_lift1_le … HT20 … HUT2 ?) -T2 // [3: /2 width=5/ |2: skip ] #U0 #HU20 #HUT0
+  elim (IHT1 … HUT1) -T1 #U #HUT #HU1
+  elim (tps_inv_lift1_le … HT2 … HUT ?) -T // [3: /2 width=5/ |2: skip ] #U2 #HU2 #HUT2
   @ex2_1_intro  [2: /2 width=2/ |1: skip |3: /2 width=3/ ] (**) (* /3 width=5/ is slow *)
 | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #d #e #X #HX
   elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct
@@ -89,15 +89,15 @@ lemma tpr_inv_lift: ∀T1,T2. T1 ➡ T2 →
   elim (IHT12 … HT01) -T1 #T3 #HT32 #HT03
   elim (lift_trans_le … HV32 … HV2 ?) -V2 // #V2 #HV32 #HV2
   @ex2_1_intro [2: /3 width=2/ |1: skip |3: /2 width=3/ ] (**) (* /4 width=5/ is slow *)
-| #V #T #T1 #T2 #HT1 #_ #IHT12 #d #e #X #HX
-  elim (lift_inv_bind2 … HX) -HX #V0 #T0 #_ #HT0 #H destruct
-  elim (lift_div_le … HT1 … HT0 ?) -T // #T #HT0 #HT1
-  elim (IHT12 … HT1) -T1 /3 width=5/
+| #V #T1 #T #T2 #_ #HT2 #IHT1 #d #e #X #HX
+  elim (lift_inv_bind2 … HX) -HX #V3 #T3 #_ #HT31 #H destruct
+  elim (IHT1 … HT31) -T1 #T1 #HT1 #HT31
+  elim (lift_div_le … HT2 … HT1 ?) -T // /3 width=5/
 | #V #T1 #T2 #_ #IHT12 #d #e #X #HX
   elim (lift_inv_flat2 … HX) -HX #V0 #T0 #_ #HT01 #H destruct
   elim (IHT12 … HT01) -T1 /3 width=3/
 ]
-qed.
+qed-.
 
 (* Advanced inversion lemmas ************************************************)
 
@@ -107,10 +107,10 @@ fact tpr_inv_abst1_aux: ∀U1,U2. U1 ➡ U2 → ∀V1,T1. U1 = ⓛV1. T1 →
 [ #I #V #T #H destruct
 | #I #V1 #V2 #T1 #T2 #_ #_ #V #T #H destruct
 | #V1 #V2 #W #T1 #T2 #_ #_ #V #T #H destruct
-| #I #V1 #V2 #T1 #T2 #T #HV12 #HT12 #HT2 #V0 #T0 #H destruct
-  <(tps_inv_refl_SO2 … HT2 ? ? ?) -T /2 width=5/
+| #I #V1 #V2 #T1 #T #T2 #HV12 #HT1 #HT2 #V0 #T0 #H destruct
+  <(tps_inv_refl_SO2 … HT2 ? ? ?) -T2 /2 width=5/
 | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #V0 #T0 #H destruct
-| #V #T #T1 #T2 #_ #_ #V0 #T0 #H destruct
+| #V #T1 #T #T2 #_ #_ #V0 #T0 #H destruct
 | #V #T1 #T2 #_ #V0 #T0 #H destruct
 ]
 qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpr.ma
index fcb2350e9..11412c541 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpr.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpr.ma
@@ -49,7 +49,7 @@ elim (IH … HV01 … HV02) -HV01 -HV02 /2 width=1/ #V #HV1 #HV2
 elim (IH … HT02 … HU01) -HT02 -HU01 -IH /2 width=1/ /3 width=5/
 qed.
 
-(* basic-1: was:
+(* Basic-1: was:
             pr0_cong_upsilon_refl pr0_cong_upsilon_zeta
             pr0_cong_upsilon_cong pr0_cong_upsilon_delta
 *)
@@ -78,15 +78,10 @@ elim (tpr_inv_abbr1 … H) -H *
   |3: @tpr_delta [3: @tpr_flat |1: skip ] /2 width=5/
   ] (**) (* /5 width=14/ is too slow *)
 (* case 3: zeta *)
-| -HW02 -HVV -HVVV #UU1 #HUU10 #HUUT1
-  elim (tpr_inv_lift … HU02 … HUU10) -HU02 #UU #HUU2 #HUU1
-  lapply (tw_lift … HUU10) -HUU10 #HUU10
-  elim (IH … HUUT1 … HUU1) -HUUT1 -HUU1 -IH /2 width=1/ -HUU10 #U #HU2 #HUUU2
-  @ex2_1_intro
-  [2: @tpr_flat
-  |1: skip 
-  |3: @tpr_zeta [2: @lift_flat |1: skip |3: @tpr_flat ]
-  ] /2 width=5/ (**) (* /5 width=5/ is too slow *)
+| -HV2 -HW02 -HVV2 #U1 #HU01 #HTU1
+  elim (IH … HU01 … HU02) -HU01 -HU02 -IH // -U0 #U #HU1 #HU2
+  elim (tpr_inv_lift1 … HU1 … HTU1) -U1 #UU #HUU #HT1UU
+  @(ex2_1_intro … (ⓐVV.UU)) /2 width=1/ /3 width=5/ (**) (* /4 width=9/ is too slow *)
 ]
 qed.
 
@@ -142,13 +137,13 @@ fact tpr_conf_delta_zeta:
       ∃∃X. X1 ➡ X & X2 ➡ X
    ) →
    V0 ➡ V1 → T0 ➡ T1 → ⋆. ⓓV1 ⊢ T1 ▶ [O,1] TT1 →
-   T2 ➡ X2 → ⇧[O, 1] T2 ≡ T0 →
+   T0 ➡ T2 → ⇧[O, 1] X2 ≡ T2 →
    ∃∃X. ⓓV1. TT1 ➡ X & X2 ➡ X.
-#X2 #V0 #V1 #T0 #T1 #TT1 #T2 #IH #_ #HT01 #HTT1 #HTX2 #HTT20
-elim (tpr_inv_lift … HT01 … HTT20) -HT01 #TT2 #HTT21 #HTT2
-lapply (tps_inv_lift1_eq … HTT1 … HTT21) -HTT1 #HTT1 destruct
-lapply (tw_lift … HTT20) -HTT20 #HTT20
-elim (IH … HTX2 … HTT2) -HTX2 -HTT2 -IH // /3 width=3/
+#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_inv_lift1 … HT2 … HXT2) -T2 #X #HXT #HX2
+lapply (tps_inv_lift1_eq … HTT … HXT) -HTT #H destruct /3 width=3/
 qed.
 
 (* Basic_1: was: pr0_upsilon_upsilon *)
@@ -172,18 +167,19 @@ lapply (tpr_lift … HV2 … HVV2 … HVV) -V2 -HVV #HVV2
 qed.
 
 fact tpr_conf_zeta_zeta:
-   ∀V0:term. ∀X2,TT0,T0,T1,T2. (
+   ∀V0:term. ∀X2,TT0,T0,T1,TT2. (
       ∀X0:term. #[X0] < #[V0] + #[TT0] + 1 →
       ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 →
       ∃∃X. X1 ➡ X & X2 ➡ X
    ) →
-   T0 ➡ T1 → T2 ➡ X2 →
-   ⇧[O, 1] T0 ≡ TT0 → ⇧[O, 1] T2 ≡ TT0 →
+   TT0 ➡ T0 → ⇧[O, 1] T1 ≡ T0 →
+   TT0 ➡ TT2 → ⇧[O, 1] X2 ≡ TT2 →
    ∃∃X. T1 ➡ X & X2 ➡ X.
-#V0 #X2 #TT0 #T0 #T1 #T2 #IH #HT01 #HTX2 #HTT0 #HTT20
-lapply (lift_inj … HTT0 … HTT20) -HTT0 #H destruct
-lapply (tw_lift … HTT20) -HTT20 #HTT20
-elim (IH … HT01 … HTX2) -HT01 -HTX2 -IH // /2 width=3/
+#V0 #X2 #TT0 #T0 #T1 #TT2 #IH #HTT0 #HT10 #HTT02 #HXTT2
+elim (IH … HTT0 … HTT02) -IH -HTT0 -HTT02 // -V0 -TT0 #T #HT0 #HTT2
+elim (tpr_inv_lift1 … HT0 … HT10) -T0 #T0 #HT0 #HT10
+elim (tpr_inv_lift1 … HTT2 … HXTT2) -TT2 #TT2 #HTT2 #HXTT2
+lapply (lift_inj … HTT2 … HT0) -HTT2 #H destruct /2 width=3/
 qed.
 
 fact tpr_conf_tau_tau:
@@ -244,7 +240,7 @@ fact tpr_conf_aux:
 (* case 9: delta, delta *)
   [ #V2 #T2 #TT2 #HV02 #HT02 #HTT2 #H destruct
     /3 width=11 by tpr_conf_delta_delta/ (**) (* /3 width=11/ is too slow *)
-(* case 10: delta, zata *)
+(* case 10: delta, zeta *)
   | #T2 #HT20 #HTX2 #H destruct
     /3 width=10 by tpr_conf_delta_zeta/ (**) (* /3 width=10/ is too slow *)
   ]
@@ -262,10 +258,10 @@ fact tpr_conf_aux:
 | #V0 #TT0 #T0 #T1 #HTT0 #HT01 #H1 #H2 destruct
   elim (tpr_inv_abbr1 … H1) -H1 *
 (* case 14: zeta, delta (repeated) *)
-  [ #V2 #T2 #TT2 #HV02 #HT02 #HTT2 #H destruct
+  [ #V2 #TT2 #T2 #HV02 #HTT02 #HTT2 #H destruct
     @ex2_1_comm /3 width=10 by tpr_conf_delta_zeta/
 (* case 15: zeta, zeta *)
-  | #T2 #HTT20 #HTX2
+  | #TT2 #HTT02 #HXTT2
     /3 width=9 by tpr_conf_zeta_zeta/ (**) (* /3 width=9/ is too slow *)
   ] 
 | #V0 #T0 #T1 #HT01 #H1 #H2 destruct
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpss.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpss.ma
index 5bb210876..f8001ac6c 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpss.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpss.ma
@@ -45,16 +45,16 @@ lemma tpr_tps_ltpr: ∀T1,T2. T1 ➡ T2 →
   elim (IHV12 … HVV1 … HL12) -V1 #VV2 #HVV12 #HVV2
   elim (IHT12 … HTT1 (L2. ⓛWW) ?) -T1 /2 width=1/ -HL12 #TT2 #HTT12 #HTT2
   lapply (tpss_lsubs_trans … HTT2 (L2. ⓓVV2) ?) -HTT2 /3 width=5/
-| #I #V1 #V2 #T1 #T2 #U2 #HV12 #_ #HTU2 #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12
-  elim (tps_inv_bind1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct
-  elim (IHV12 … HVV1 … HL12) -V1 #VV2 #HVV12 #HVV2
-  elim (IHT12 … HTT1 (L2. ⓑ{I} VV2) ?) -T1 /2 width=1/ -HL12 #TT2 #HTT12 #HTT2
-  elim (tpss_strip_neq … HTT2 … HTU2 ?) -T2 /2 width=1/ #T2 #HTT2 #HUT2
-  lapply (tps_lsubs_trans … HTT2 (L2. ⓑ{I} V2) ?) -HTT2 /2 width=1/ #HTT2
-  elim (ltpss_tps_conf … HTT2 (L2. ⓑ{I} VV2) (d + 1) e ?) -HTT2 /2 width=1/ #W2 #HTTW2 #HTW2
-  lapply (tps_lsubs_trans … HTTW2 (⋆. ⓑ{I} VV2) ?) -HTTW2 /2 width=1/ #HTTW2
-  lapply (tpss_lsubs_trans … HTW2 (L2. ⓑ{I} VV2) ?) -HTW2 /2 width=1/ #HTW2
-  lapply (tpss_trans_eq … HUT2 … HTW2) -T2 /3 width=5/
+| #I #V1 #V2 #T1 #T #T2 #HV12 #_ #HT2 #IHV12 #IHT1 #L1 #d #e #X #H #L2 #HL12
+  elim (tps_inv_bind1 … H) -H #W1 #U1 #HVW1 #HTU1 #H destruct
+  elim (IHV12 … HVW1 … HL12) -V1 #W2 #HW12 #HVW2
+  elim (IHT1 … HTU1 (L2. ⓑ{I} W2) ?) -T1 /2 width=1/ -HL12 #U #HU1 #HTU
+  elim (tpss_strip_neq … HTU … HT2 ?) -T /2 width=1/ #U2 #HU2 #HTU2
+  lapply (tps_lsubs_trans … HU2 (L2. ⓑ{I} V2) ?) -HU2 /2 width=1/ #HU2
+  elim (ltpss_tps_conf … HU2 (L2. ⓑ{I} W2) (d + 1) e ?) -HU2 /2 width=1/ #U3 #HU3 #HU23
+  lapply (tps_lsubs_trans … HU3 (⋆. ⓑ{I} W2) ?) -HU3 /2 width=1/ #HU3
+  lapply (tpss_lsubs_trans … HU23 (L2. ⓑ{I} W2) ?) -HU23 /2 width=1/ #HU23
+  lapply (tpss_trans_eq … HTU2 … HU23) -U2 /3 width=5/
 | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #L1 #d #e #X #H #L2 #HL12
   elim (tps_inv_flat1 … H) -H #VV1 #Y #HVV1 #HY #HX destruct
   elim (tps_inv_bind1 … HY) -HY #WW1 #TT1 #HWW1 #HTT1 #H destruct
@@ -64,10 +64,10 @@ lemma tpr_tps_ltpr: ∀T1,T2. T1 ➡ T2 →
   elim (lift_total VV2 0 1) #VV #H2VV
   lapply (tpss_lift_ge … HVV2 (L2. ⓓWW2) … HV2 … H2VV) -V2 /2 width=1/ #HVV
   @ex2_1_intro [2: @tpr_theta |1: skip |3: @tpss_bind [2: @tpss_flat ] ] /width=11/ (**) (* /4 width=11/ is too slow *)
-| #V1 #TT1 #T1 #T2 #HTT1 #_ #IHT12 #L1 #d #e #X #H #L2 #HL12
-  elim (tps_inv_bind1 … H) -H #V2 #TT2 #HV12 #HTT12 #H destruct
-  elim (tps_inv_lift1_ge … HTT12 L1 … HTT1 ?) -TT1 /2 width=1/ #T2 #HT12 #HTT2
-  elim (IHT12 … HT12 … HL12) -T1 -HL12 <minus_plus_m_m /3 width=3/
+| #V #T1 #T #T2 #_ #HT2 #IHT1 #L1 #d #e #X #H #L2 #HL12
+  elim (tps_inv_bind1 … H) -H #W #U1 #_ #HTU1 #H destruct -V
+  elim (IHT1 … HTU1 (L2.ⓓW) ?) -T1 /2 width=1/ -HL12 #U #HU1 #HTU
+  elim (tpss_inv_lift1_ge … HTU L2 … HT2 ?) -T <minus_plus_m_m /3 width=3/
 | #V1 #T1 #T2 #_ #IHT12 #L1 #d #e #X #H #L2 #HL12
   elim (tps_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct
   elim (IHT12 … HTT1 … HL12) -T1 -HL12 /3 width=3/
@@ -78,7 +78,8 @@ 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.
 #I #V1 #V2 #T1 #T2 #U1 #HV12 #HT12 #HTU1
-elim (tpr_tps_ltpr … HT12 … HTU1 (⋆. ⓑ{I} V2) ?) -T1 /2 width=1/ /3 width=3/
+elim (tpr_tps_ltpr … HT12 … HTU1 (⋆. ⓑ{I} V2) ?) -T1 /2 width=1/ -V1 #U2 #HU12 #HTU2
+lapply (tpss_inv_SO2 … HTU2) -HTU2 /2 width=3/
 qed.
 
 lemma tpr_tpss_ltpr: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. T1 ➡ T2 →
diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/sta_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/static/sta_lift.ma
index 45465cbce..c9fbda014 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/static/sta_lift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/static/sta_lift.ma
@@ -59,9 +59,9 @@ lemma sta_lift: ∀h,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 • U1 → ∀L2,d,e. ⇩[d, e
 qed.
 
 (* Note: apparently this was missing in basic_1 *)
-lemma sta_inv_lift: ∀h,L2,T2,U2. ⦃h, L2⦄ ⊢ T2 • U2 → ∀L1,d,e. ⇩[d, e] L2 ≡ L1 →
-                    ∀T1. ⇧[d, e] T1 ≡ T2 →
-                    ∃∃U1. ⦃h, L1⦄ ⊢ T1 • U1 & ⇧[d, e] U1 ≡ U2.
+lemma sta_inv_lift1: ∀h,L2,T2,U2. ⦃h, L2⦄ ⊢ T2 • U2 → ∀L1,d,e. ⇩[d, e] L2 ≡ L1 →
+                     ∀T1. ⇧[d, e] T1 ≡ T2 →
+                     ∃∃U1. ⦃h, L1⦄ ⊢ T1 • U1 & ⇧[d, e] U1 ≡ U2.
 #h #L2 #T2 #U2 #H elim H -L2 -T2 -U2
 [ #L2 #k #L1 #d #e #_ #X #H
   >(lift_inv_sort2 … H) -X /2 width=3/
diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/sta_ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/static/sta_ltpss.ma
new file mode 100644
index 000000000..b0232f5a6
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/static/sta_ltpss.ma
@@ -0,0 +1,122 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/unfold/tpss_tpss.ma".
+include "basic_2/unfold/ltpss_tpss.ma".
+include "basic_2/static/sta_lift.ma".
+
+(* STATIC TYPE ASSIGNMENT ON TERMS ******************************************)
+
+(* Properties about parallel unfold *****************************************)
+
+lemma sta_ltpss_tpss_conf: ∀h,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 • U1 →
+                           ∀L2,d,e. L1 ▶* [d, e] L2 →
+                           ∀T2. L2 ⊢ T1 ▶* [d, e] T2 →
+                           ∃∃U2. ⦃h, L2⦄ ⊢ T2 • U2 & L2 ⊢ U1 ▶* [d, e] U2.
+#h #L1 #T1 #U #H elim H -L1 -T1 -U
+[ #L1 #k1 #L2 #d #e #_ #T2 #H
+  >(tpss_inv_sort1 … H) -H /2 width=3/
+| #L1 #K1 #V1 #W1 #U1 #i #HLK1 #HVW1 #HWU1 #IHVW1 #L2 #d #e #HL12 #T2 #H
+  elim (tpss_inv_lref1 … H) -H [ | -HVW1 ]
+  [ #H destruct
+    elim (lt_or_ge i d) #Hdi [ -HVW1 | ]
+    [ elim (ltpss_ldrop_conf_le … HL12 … HLK1 ?) -L1 /2 width=2/ #X #H #HLK2
+      elim (ltpss_inv_tpss11 … H ?) -H /2 width=1/ #K2 #V2 #HK12 #HV12 #H destruct
+      elim (IHVW1 … HK12 … HV12) -IHVW1 -HK12 -HV12 #W2 #HVW2 #HW12
+      lapply (ldrop_fwd_ldrop2 … HLK2) #H
+      elim (lift_total W2 0 (i+1)) #U2 #HWU2
+      lapply (tpss_lift_ge … HW12 … H … HWU1 … HWU2) // -HW12 -H -HWU1
+      >minus_plus <plus_minus_m_m // -Hdi /3 width=6/
+    | elim (lt_or_ge i (d + e)) #Hide [ -HVW1 | -Hdi -IHVW1 ]
+      [ elim (ltpss_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HLK2
+        elim (ltpss_inv_tpss21 … H ?) -H /2 width=1/ #K2 #V2 #HK12 #HV12 #H destruct
+        elim (IHVW1 … HK12 … HV12) -IHVW1 -HK12 -HV12 #W2 #HVW2 #HW12
+        lapply (ldrop_fwd_ldrop2 … HLK2) #H
+        elim (lift_total W2 0 (i+1)) #U2 #HWU2
+        lapply (tpss_lift_ge … HW12 … H … HWU1 … HWU2) // -HW12 -H -HWU1 >minus_plus #H
+        lapply (tpss_weak … H d e ? ?) [1,2: normalize [ >commutative_plus <plus_minus_m_m // | /2 width=1/ ]] -Hdi -Hide /3 width=6/
+      | lapply (ltpss_ldrop_conf_ge … HL12 … HLK1 ?) -L1 // -Hide /3 width=6/
+      ]
+    ]
+  | * #K2 #V2 #W2 #Hdi #Hide #HLK2 #HVW2 #HWT2
+    elim (ltpss_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HL2K0
+    elim (ltpss_inv_tpss21 … H ?) -H /2 width=1/ #K0 #V0 #HK12 #HV12 #H destruct
+    lapply (ldrop_mono … HL2K0 … HLK2) -HL2K0 #H destruct
+    lapply (ldrop_fwd_ldrop2 … HLK2) -HLK2 #HLK2
+    lapply (tpss_trans_eq … HV12 HVW2) -V2 #HV1W2
+    elim (IHVW1 … HK12 … HV1W2) -IHVW1 -HK12 -HV1W2 #V2 #HWV2 #HW1V2
+    elim (lift_total V2 0 (i+1)) #U2 #HVU2
+    lapply (sta_lift … HWV2 … HLK2 … HWT2 … HVU2) -HWV2 -HWT2 #HTU2
+    lapply (tpss_lift_ge … HW1V2 … HLK2 … HWU1 … HVU2) // -HW1V2 -HLK2 -HWU1 -HVU2 >minus_plus #H
+    lapply (tpss_weak … H d e ? ?) [1,2: normalize [ >commutative_plus <plus_minus_m_m // | /2 width=1/ ]] -Hdi -Hide /2 width=3/
+  ]
+| #L1 #K1 #W1 #V1 #U1 #i #HLK1 #HWV1 #HWU1 #IHWV1 #L2 #d #e #HL12 #T2 #H
+  elim (tpss_inv_lref1 … H) -H [ | -HWV1 -HWU1 -IHWV1 ]
+  [ #H destruct
+    elim (lt_or_ge i d) #Hdi [ -HWV1 ]
+    [ elim (ltpss_ldrop_conf_le … HL12 … HLK1 ?) -L1 /2 width=2/ #X #H #HLK2
+      elim (ltpss_inv_tpss11 … H ?) -H /2 width=1/ #K2 #W2 #HK12 #HW12 #H destruct
+      elim (IHWV1 … HK12 … HW12) -IHWV1 -HK12 #V2 #HWV2 #_
+      lapply (ldrop_fwd_ldrop2 … HLK2) #HLK
+      elim (lift_total W2 0 (i+1)) #U2 #HWU2
+      lapply (tpss_lift_ge … HW12 … HLK … HWU1 … HWU2) // -HW12 -HLK -HWU1
+      >minus_plus <plus_minus_m_m // -Hdi /3 width=6/
+    | elim (lt_or_ge i (d + e)) #Hide [ -HWV1 | -IHWV1 -Hdi ]
+      [ elim (ltpss_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HLK2
+        elim (ltpss_inv_tpss21 … H ?) -H /2 width=1/ #K2 #W2 #HK12 #HW12 #H destruct
+        elim (IHWV1 … HK12 … HW12) -IHWV1 -HK12 #V2 #HWV2 #_
+        lapply (ldrop_fwd_ldrop2 … HLK2) #HLK
+        elim (lift_total W2 0 (i+1)) #U2 #HWU2
+        lapply (tpss_lift_ge … HW12 … HLK … HWU1 … HWU2) // -HW12 -HLK -HWU1 >minus_plus #H
+        lapply (tpss_weak … H d e ? ?) [1,2: normalize [ >commutative_plus <plus_minus_m_m // | /2 width=1/ ]] -Hdi -Hide /3 width=6/
+      | lapply (ltpss_ldrop_conf_ge … HL12 … HLK1 ?) -L1 // -Hide /3 width=6/
+      ]
+    ]
+  | * #K2 #V2 #W2 #Hdi #Hide #HLK2 #_ #_
+    elim (ltpss_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HL2K0
+    elim (ltpss_inv_tpss21 … H ?) -H /2 width=1/ -Hdi -Hide #K0 #V0 #_ #_ #H destruct
+    lapply (ldrop_mono … HL2K0 … HLK2) -HL2K0 -HLK2 #H destruct
+  ]
+| #I #L1 #V1 #T1 #U1 #_ #IHTU1 #L2 #d #e #HL12 #X #H
+  elim (tpss_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
+  elim (IHTU1 … HT12) -IHTU1 -HT12 /2 width=1/ -HL12 /3 width=5/
+| #L1 #V1 #T1 #U1 #_ #IHTU1 #L2 #d #e #HL12 #X #H
+  elim (tpss_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
+  elim (IHTU1 … HT12) -IHTU1 -HT12 // -HL12 /3 width=5/
+| #L1 #W1 #T1 #U1 #_ #IHTU1 #L2 #d #e #HL12 #X #H
+  elim (tpss_inv_flat1 … H) -H #W2 #T2 #HW12 #HT12 #H destruct
+  elim (IHTU1 … HT12) -IHTU1 -HT12 // -HL12 /3 width=3/
+]
+qed.
+
+lemma sta_ltpss_tps_conf: ∀h,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 • U1 →
+                          ∀L2,d,e. L1 ▶* [d, e] L2 →
+                          ∀T2. L2 ⊢ T1 ▶ [d, e] T2 →
+                          ∃∃U2. ⦃h, L2⦄ ⊢ T2 • U2 & L2 ⊢ U1 ▶* [d, e] U2.
+/3 width=5/ qed.
+
+lemma sta_ltpss_conf: ∀h,L1,T,U1. ⦃h, L1⦄ ⊢ T • U1 →
+                      ∀L2,d,e. L1 ▶* [d, e] L2 →
+                      ∃∃U2. ⦃h, L2⦄ ⊢ T • U2 & L2 ⊢ U1 ▶* [d, e] U2.
+/2 width=5/ qed.
+
+lemma sta_tpss_conf: ∀h,L,T1,U1. ⦃h, L⦄ ⊢ T1 • U1 →
+                     ∀T2,d,e. L ⊢ T1 ▶* [d, e] T2 →
+                     ∃∃U2. ⦃h, L⦄ ⊢ T2 • U2 & L ⊢ U1 ▶* [d, e] U2.
+/2 width=5/ qed.
+
+lemma sta_tps_conf: ∀h,L,T1,U1. ⦃h, L⦄ ⊢ T1 • U1 →
+                    ∀T2,d,e. L ⊢ T1 ▶ [d, e] T2 →
+                    ∃∃U2. ⦃h, L⦄ ⊢ T2 • U2 & L ⊢ U1 ▶* [d, e] U2.
+/2 width=5/ qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/lift_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/lift_lift.ma
index 3d53cc942..f302b16ad 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/substitution/lift_lift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/lift_lift.ma
@@ -201,6 +201,14 @@ qed.
 
 (* Advanced properties ******************************************************)
 
+lemma lift_conf_O1: ∀T,T1,d1,e1. ⇧[d1, e1] T ≡ T1 → ∀T2,e2. ⇧[0, e2] T ≡ T2 →
+                    ∃∃T0. ⇧[0, e2] T1 ≡ T0 & ⇧[d1 + e2, e1] T2 ≡ T0.
+#T #T1 #d1 #e1 #HT1 #T2 #e2 #HT2
+elim (lift_total T1 0 e2) #T0 #HT10
+elim (lift_trans_le … HT1 … HT10 ?) -HT1 // #X #HTX #HT20
+lapply (lift_mono … HTX … HT2) -T #H destruct /2 width=3/
+qed.
+
 lemma lift_conf_be: ∀T,T1,d,e1. ⇧[d, e1] T ≡ T1 → ∀T2,e2. ⇧[d, e2] T ≡ T2 →
                     e1 ≤ e2 → ⇧[d + e1, e2 - e1] T1 ≡ T2.
 #T #T1 #d #e1 #HT1 #T2 #e2 #HT2 #He12
diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/lsubs_sfr.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/lsubs_sfr.ma
index 2b71621fa..b71f25e51 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/substitution/lsubs_sfr.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/lsubs_sfr.ma
@@ -43,6 +43,11 @@ elim (lsubs_inv_abbr2 … H ?) -H // <minus_plus_m_m #X #HLX #H destruct
 lapply (HL … HLX) -HL -HLX /2 width=1/
 qed.
 
+lemma sfr_abbr_O: ∀L,V. ≽[0,1] L.ⓓV.
+#L #V
+@(sfr_abbr … 0) //
+qed.
+
 lemma sfr_skip: ∀I,L,V,d,e. ≽ [d, e] L → ≽ [d + 1, e] L.ⓑ{I}V.
 #I #L #V #d #e #HL #K #H
 elim (lsubs_inv_skip2 … H ?) -H // <minus_plus_m_m #J #X #W #HLX #H destruct
diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_tpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_tpss.ma
index 7ec6dc07b..3f41b0083 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_tpss.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_tpss.ma
@@ -17,13 +17,15 @@ include "basic_2/unfold/tpss_lift.ma".
 
 (* PARTIAL UNFOLD ON TERMS **************************************************)
 
-(* Advanced properties ******************************************************)
+(* Advanced inversion lemmas ************************************************)
 
-lemma tpss_tps: ∀L,T1,T2,d. L ⊢ T1 ▶* [d, 1] T2 → L ⊢ T1 ▶ [d, 1] T2.
+lemma tpss_inv_SO2: ∀L,T1,T2,d. L ⊢ T1 ▶* [d, 1] T2 → L ⊢ T1 ▶ [d, 1] T2.
 #L #T1 #T2 #d #H @(tpss_ind … H) -T2 //
 #T #T2 #_ #HT2 #IHT1
 lapply (tps_trans_ge … IHT1 … HT2 ?) //
-qed.
+qed-.
+
+(* Advanced properties ******************************************************)
 
 lemma tpss_strip_eq: ∀L,T0,T1,d1,e1. L ⊢ T0 ▶* [d1, e1] T1 →
                      ∀T2,d2,e2. L ⊢ T0 ▶ [d2, e2] T2 →
diff --git a/matita/matita/contribs/lambda_delta/ground_2/xoa.conf.xml b/matita/matita/contribs/lambda_delta/ground_2/xoa.conf.xml
index 4aaba50b3..f1eaa39dd 100644
--- a/matita/matita/contribs/lambda_delta/ground_2/xoa.conf.xml
+++ b/matita/matita/contribs/lambda_delta/ground_2/xoa.conf.xml
@@ -22,13 +22,13 @@
     <key name="ex">3 1</key>
     <key name="ex">3 2</key>
     <key name="ex">3 3</key>
+    <key name="ex">3 4</key>
     <key name="ex">4 2</key>
     <key name="ex">4 3</key>
     <key name="ex">4 4</key>
     <key name="ex">5 2</key>
     <key name="ex">5 3</key>
     <key name="ex">5 4</key>
-    <key name="ex">5 5</key>
     <key name="ex">6 4</key>
     <key name="ex">6 6</key>
     <key name="ex">7 6</key>
diff --git a/matita/matita/contribs/lambda_delta/ground_2/xoa.ma b/matita/matita/contribs/lambda_delta/ground_2/xoa.ma
index 6214557bb..d96b471e6 100644
--- a/matita/matita/contribs/lambda_delta/ground_2/xoa.ma
+++ b/matita/matita/contribs/lambda_delta/ground_2/xoa.ma
@@ -80,6 +80,14 @@ inductive ex3_3 (A0,A1,A2:Type[0]) (P0,P1,P2:A0→A1→A2→Prop) : Prop ≝
 
 interpretation "multiple existental quantifier (3, 3)" 'Ex P0 P1 P2 = (ex3_3 ? ? ? P0 P1 P2).
 
+(* multiple existental quantifier (3, 4) *)
+
+inductive ex3_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2:A0→A1→A2→A3→Prop) : Prop ≝
+   | ex3_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → P2 x0 x1 x2 x3 → ex3_4 ? ? ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (3, 4)" 'Ex P0 P1 P2 = (ex3_4 ? ? ? ? P0 P1 P2).
+
 (* multiple existental quantifier (4, 2) *)
 
 inductive ex4_2 (A0,A1:Type[0]) (P0,P1,P2,P3:A0→A1→Prop) : Prop ≝
@@ -128,14 +136,6 @@ inductive ex5_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4:A0→A1→A2→A3→Prop)
 
 interpretation "multiple existental quantifier (5, 4)" 'Ex P0 P1 P2 P3 P4 = (ex5_4 ? ? ? ? P0 P1 P2 P3 P4).
 
-(* multiple existental quantifier (5, 5) *)
-
-inductive ex5_5 (A0,A1,A2,A3,A4:Type[0]) (P0,P1,P2,P3,P4:A0→A1→A2→A3→A4→Prop) : Prop ≝
-   | ex5_5_intro: ∀x0,x1,x2,x3,x4. P0 x0 x1 x2 x3 x4 → P1 x0 x1 x2 x3 x4 → P2 x0 x1 x2 x3 x4 → P3 x0 x1 x2 x3 x4 → P4 x0 x1 x2 x3 x4 → ex5_5 ? ? ? ? ? ? ? ? ? ?
-.
-
-interpretation "multiple existental quantifier (5, 5)" 'Ex P0 P1 P2 P3 P4 = (ex5_5 ? ? ? ? ? P0 P1 P2 P3 P4).
-
 (* multiple existental quantifier (6, 4) *)
 
 inductive ex6_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2→A3→Prop) : Prop ≝
diff --git a/matita/matita/contribs/lambda_delta/ground_2/xoa_notation.ma b/matita/matita/contribs/lambda_delta/ground_2/xoa_notation.ma
index e1e2240ce..44453eae0 100644
--- a/matita/matita/contribs/lambda_delta/ground_2/xoa_notation.ma
+++ b/matita/matita/contribs/lambda_delta/ground_2/xoa_notation.ma
@@ -94,6 +94,16 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break
  non associative with precedence 20
  for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P2) }.
 
+(* multiple existental quantifier (3, 4) *)
+
+notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P2) }.
+
+notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) }.
+
 (* multiple existental quantifier (4, 2) *)
 
 notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)"
@@ -154,16 +164,6 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term
  non associative with precedence 20
  for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P4) }.
 
-(* multiple existental quantifier (5, 5) *)
-
-notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)"
- non associative with precedence 20
- for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P4) }.
-
-notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)"
- non associative with precedence 20
- for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P4) }.
-
 (* multiple existental quantifier (6, 4) *)
 
 notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)"
diff --git a/matita/matita/lib/basics/star.ma b/matita/matita/lib/basics/star.ma
index c8d2a9473..1e2a48000 100644
--- a/matita/matita/lib/basics/star.ma
+++ b/matita/matita/lib/basics/star.ma
@@ -46,7 +46,7 @@ qed.
   
 (* star *)
 inductive star (A:Type[0]) (R:relation A) (a:A): A → Prop ≝
-  |inj: ∀b,c.star A R a b → R b c → star A R a c
+  |sstep: ∀b,c.star A R a b → R b c → star A R a c
   |refl: star A R a a.
 
 lemma R_to_star: ∀A,R,a,b. R a b → star A R a b.
@@ -93,22 +93,22 @@ qed.
 
 (* right associative version of star *)
 inductive starl (A:Type[0]) (R:relation A) : A → A → Prop ≝
-  |injl: ∀a,b,c.R a b → starl A R b c → starl A R a c
+  |sstepl: ∀a,b,c.R a b → starl A R b c → starl A R a c
   |refll: ∀a.starl A R a a.
  
 lemma starl_comp : ∀A,R,a,b,c.
   starl A R a b → R b c → starl A R a c.
 #A #R #a #b #c #Hstar elim Hstar 
-  [#a1 #b1 #c1 #Rab #sbc #Hind #a1 @(injl … Rab) @Hind //
-  |#a1 #Rac @(injl … Rac) //
+  [#a1 #b1 #c1 #Rab #sbc #Hind #a1 @(sstepl … Rab) @Hind //
+  |#a1 #Rac @(sstepl … Rac) //
   ]
 qed.
 
 lemma star_compl : ∀A,R,a,b,c.
   R a b → star A R b c → star A R a c.
 #A #R #a #b #c #Rab #Hstar elim Hstar 
-  [#b1 #c1 #sbb1 #Rb1c1 #Hind @(inj … Rb1c1) @Hind
-  |@(inj … Rab) //
+  [#b1 #c1 #sbb1 #Rb1c1 #Hind @(sstep … Rb1c1) @Hind
+  |@(sstep … Rab) //
   ]
 qed.
 
-- 
2.39.2