From 636c25914e83819c2f529edc891a7eb899499a97 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 10 May 2012 10:58:45 +0000
Subject: [PATCH] - lib: some additions - lambda_delta: more properties on
 native type assignment                 change of notation for consand append

---
 .../apps_2/functional/rtm_step.ma             |   4 +-
 .../contribs/lambda_delta/basic_2/basic_1.txt |   4 -
 .../basic_2/computation/acp_aaa.ma            |   4 +-
 .../basic_2/computation/acp_cr.ma             |  10 +-
 .../basic_2/computation/cprs_delift.ma        |  30 +++
 .../basic_2/computation/csn_tstc_vector.ma    |   2 +-
 .../basic_2/computation/csn_vector.ma         |   2 +-
 .../lambda_delta/basic_2/dynamic/nta_alt.ma   | 190 ++++++++++++++++++
 .../basic_2/dynamic/nta_delift.ma             |  84 ++++++++
 .../lambda_delta/basic_2/dynamic/nta_lift.ma  | 124 ++++--------
 .../lambda_delta/basic_2/dynamic/nta_nta.ma   |  59 ++++++
 .../lambda_delta/basic_2/equivalence/cpcs.ma  |   3 +
 .../basic_2/equivalence/cpcs_delift.ma        |  32 +++
 .../lambda_delta/basic_2/grammar/cl_weight.ma |   2 +-
 .../contribs/lambda_delta/basic_2/notation.ma |   4 +
 .../basic_2/reducibility/cpr_cpr.ma           |   2 +-
 .../basic_2/reducibility/cpr_delift.ma        |  37 ++++
 .../basic_2/reducibility/tpr_delift.ma        |  27 +++
 .../basic_2/reducibility/tpr_tpss.ma          |   5 +
 .../basic_2/substitution/lift_vector.ma       |  10 +-
 .../basic_2/substitution/tps_lift.ma          |  19 +-
 .../lambda_delta/basic_2/unfold/delift.ma     |   4 +-
 .../lambda_delta/basic_2/unfold/delift_alt.ma |   6 +-
 .../basic_2/unfold/delift_delift.ma           |   2 +-
 .../basic_2/unfold/delift_lift.ma             |   6 +-
 .../basic_2/unfold/delift_ltpss.ma            |   2 +-
 .../basic_2/unfold/delift_tpss.ma             |  38 +++-
 .../lambda_delta/basic_2/unfold/gr2.ma        |  12 +-
 .../lambda_delta/basic_2/unfold/gr2_minus.ma  |  18 +-
 .../lambda_delta/basic_2/unfold/gr2_plus.ma   |   6 +-
 .../lambda_delta/basic_2/unfold/ldrops.ma     |   6 +-
 .../basic_2/unfold/ldrops_ldrops.ma           |   2 +-
 .../lambda_delta/basic_2/unfold/lifts.ma      |   6 +-
 .../basic_2/unfold/lifts_lifts.ma             |   2 +-
 .../basic_2/unfold/lifts_vector.ma            |   2 +-
 .../lambda_delta/basic_2/unfold/thin.ma       |   4 +-
 .../basic_2/unfold/thin_delift.ma             |  58 +++++-
 .../lambda_delta/basic_2/unfold/thin_ldrop.ma |   2 +-
 .../lambda_delta/basic_2/unfold/tpss_lift.ma  |  25 ++-
 .../contribs/lambda_delta/ground_2/list.ma    |   2 +-
 .../lambda_delta/ground_2/notation.ma         |   6 +-
 matita/matita/lib/arithmetics/nat.ma          |   4 +
 matita/matita/lib/basics/star.ma              |  26 ++-
 43 files changed, 721 insertions(+), 172 deletions(-)
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/computation/cprs_delift.ma
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_alt.ma
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_delift.ma
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_nta.ma
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_delift.ma
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_delift.ma
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_delift.ma

diff --git a/matita/matita/contribs/lambda_delta/apps_2/functional/rtm_step.ma b/matita/matita/contribs/lambda_delta/apps_2/functional/rtm_step.ma
index f67d9dc1f..9a04c8070 100644
--- a/matita/matita/contribs/lambda_delta/apps_2/functional/rtm_step.ma
+++ b/matita/matita/contribs/lambda_delta/apps_2/functional/rtm_step.ma
@@ -41,9 +41,9 @@ inductive rtm_step: relation rtm ≝
                        (mk_rtm G u E S T)
 | rtm_appl  : ∀G,u,E,S,V,T.
               rtm_step (mk_rtm G u E S (ⓐV. T))
-                       (mk_rtm G u E ({E, V} :: S) T)
+                       (mk_rtm G u E ({E, V} @ S) T)
 | rtm_beta  : ∀G,u,E,F,V,S,W,T.
-              rtm_step (mk_rtm G u E ({F, V} :: S) (ⓛW. T))
+              rtm_step (mk_rtm G u E ({F, V} @ S) (ⓛW. T))
                        (mk_rtm G u (E. ④{Abbr} {u, F, V}) S T)
 | rtm_push  : ∀G,u,E,W,T.
               rtm_step (mk_rtm G u E ⟠ (ⓛW. T))
diff --git a/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt b/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt
index 1b6aaa13f..0c6fcb34a 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt
+++ b/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt
@@ -180,7 +180,6 @@ pc3/props pc3_pr2_pr2_t
 pc3/props pc3_pr2_pr3_t
 pc3/props pc3_pr3_pc3_t
 pc3/props pc3_eta
-pc3/subst1 pc3_gen_cabbr
 pc3/wcpr0 pc3_wcpr0__pc3_wcpr0_t_aux
 pc3/wcpr0 pc3_wcpr0_t
 pc3/wcpr0 pc3_wcpr0
@@ -198,11 +197,9 @@ pr1/props pr1_head_2
 pr1/props pr1_comp
 pr1/props pr1_eta
 pr2/fwd pr2_gen_void
-pr2/subst1 pr2_gen_cabbr
 pr3/fwd pr3_gen_void
 pr3/pr1 pr3_pr1
 pr3/props pr3_eta
-pr3/subst1 pr3_gen_cabbr
 sn3/props sns3_lifts
 sty1/cnt sty1_cnt
 sty1/props sty1_trans
@@ -260,7 +257,6 @@ ty3/pr3_props ty3_tred
 ty3/pr3_props ty3_sconv_pc3
 ty3/pr3_props ty3_sred_back
 ty3/pr3_props ty3_sconv
-ty3/props ty3_unique
 ty3/props ty3_gen_abst_abst
 ty3/sty0 ty3_sty0
 ty3/subst1 ty3_gen_cabbr
diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/acp_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/acp_aaa.ma
index 190a595cf..788c39902 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/acp_aaa.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/acp_aaa.ma
@@ -73,8 +73,8 @@ theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP.
     #L3 #V3 #T3 #des3 #HL32 #HT03 #HB
     elim (lifts_total des3 W0) #W2 #HW02
     elim (ldrops_lsubc_trans … H1RP H2RP … HL32 … HL02) -L2 #L2 #HL32 #HL20
-    lapply (aaa_lifts … L2 W2 … (des @ des3) … HLWB) -HLWB /2 width=3/ #HLW2B
-    @(IHA (L2. ⓛW2) … (des + 1 @ des3 + 1)) -IHA
+    lapply (aaa_lifts … L2 W2 … (des @@ des3) … HLWB) -HLWB /2 width=3/ #HLW2B
+    @(IHA (L2. ⓛW2) … (des + 1 @@ des3 + 1)) -IHA
     /2 width=3/ /3 width=5/
   ]
 | #L #V #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL20
diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/acp_cr.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/acp_cr.ma
index c300d19de..222f00da8 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/acp_cr.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/acp_cr.ma
@@ -119,12 +119,12 @@ lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
 | #L #Vs #HVs #T #H1T #H2T #L0 #V0 #X #des #HB #HL0 #H
   elim (lifts_inv_applv1 … H) -H #V0s #T0 #HV0s #HT0 #H destruct
   lapply (s1 … IHB … HB) #HV0
-  @(s2 … IHA … (V0 :: V0s)) /2 width=4 by lifts_simple_dx/ /3 width=6/
+  @(s2 … IHA … (V0 @ V0s)) /2 width=4 by lifts_simple_dx/ /3 width=6/
 | #L #Vs #U #T #W #HA #HW #L0 #V0 #X #des #HB #HL0 #H
   elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
   elim (lifts_inv_flat1 … HY) -HY #U0 #X #HU0 #HX #H destruct
   elim (lifts_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT0 #H destruct
-  @(s3 … IHA … (V0 :: V0s)) /2 width=6 by rp_lifts/ /4 width=5/
+  @(s3 … IHA … (V0 @ V0s)) /2 width=6 by rp_lifts/ /4 width=5/
 | #L #K #Vs #V1 #V2 #i #HA #HV12 #HLK #L0 #V0 #X #des #HB #HL0 #H
   elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
   elim (lifts_inv_lref1 … HY) -HY #i0 #Hi0 #H destruct
@@ -134,13 +134,13 @@ lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
   elim (lift_total W1 0 (i0 + 1)) #W2 #HW12
   elim (lifts_lift_trans  … Hdes0 … HVW1 … HW12) // -Hdes0 -Hi0 #V3 #HV13 #HVW2
   >(lift_mono … HV13 … HV12) in HVW2; -V3 #HVW2
-  @(s4 … IHA … (V0 :: V0s) … HW12 HL02) /3 width=4/
+  @(s4 … IHA … (V0 @ V0s) … HW12 HL02) /3 width=4/
 | #L #V1s #V2s #HV12s #V #T #HA #HV #L0 #V10 #X #des #HB #HL0 #H
   elim (lifts_inv_applv1 … H) -H #V10s #Y #HV10s #HY #H destruct
   elim (lifts_inv_bind1 … HY) -HY #V0 #T0 #HV0 #HT0 #H destruct
   elim (lift_total V10 0 1) #V20 #HV120
   elim (liftv_total 0 1 V10s) #V20s #HV120s
-  @(s5 … IHA … (V10 :: V10s) (V20 :: V20s)) /2 width=1/ /2 width=6 by rp_lifts/
+  @(s5 … IHA … (V10 @ V10s) (V20 @ V20s)) /2 width=1/ /2 width=6 by rp_lifts/
   @(HA … (des + 1)) /2 width=1/
   [ @(s7 … IHB … HB … HV120) /2 width=1/
   | @lifts_applv //
@@ -150,7 +150,7 @@ lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
 | #L #Vs #T #W #HA #HW #L0 #V0 #X #des #HB #HL0 #H
   elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
   elim (lifts_inv_flat1 … HY) -HY #W0 #T0 #HW0 #HT0 #H destruct
-  @(s6 … IHA … (V0 :: V0s)) /2 width=6 by rp_lifts/ /3 width=4/
+  @(s6 … IHA … (V0 @ V0s)) /2 width=6 by rp_lifts/ /3 width=4/
 | /3 width=7/
 ]
 qed.
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
new file mode 100644
index 000000000..65488a734
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_delift.ma
@@ -0,0 +1,30 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/reducibility/cpr_delift.ma".
+include "basic_2/computation/cprs.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
+
+(* Properties on inverse basic term relocation ******************************)
+
+(* Basic_1: was only: pr3_gen_cabbr *)
+lemma thin_cprs_delift_conf: ∀L,U1,U2. L ⊢ U1 ➡* U2 →
+                             ∀K,d,e. L [d, e] ≡ K → ∀T1. L ⊢ U1 [d, e] ≡ T1 →
+                             ∃∃T2. K ⊢ T1 ➡* T2 & L ⊢ U2 [d, e] ≡ T2.
+#L #U1 #U2 #H @(cprs_ind … H) -U2 /2 width=3/
+#U #U2 #_ #HU2 #IHU1 #K #d #e #HLK #T1 #HTU1
+elim (IHU1 … HLK … HTU1) -U1 #T #HT1 #HUT
+elim (thin_cpr_delift_conf … HU2 … HLK … HUT) -U -HLK /3 width=3/
+qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma
index 3aa7170f5..e1a641505 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma
@@ -81,7 +81,7 @@ lapply (csn_appl_theta … HW12 … H) -H -HW12 #H
 lapply (csn_fwd_pair_sn … H) #HW1
 lapply (csn_fwd_flat_dx … H) #H1
 @csn_appl_simple_tstc // -HW1 /2 width=3/ -IHV12s -HV -H1 #X #H1 #H2
-elim (cprs_fwd_theta_vector … (V2::V2s) … H1) -H1 /2 width=1/ -HV12s -HV12
+elim (cprs_fwd_theta_vector … (V2@V2s) … H1) -H1 /2 width=1/ -HV12s -HV12
 [ -H #H elim (H2 ?) -H2 //
 | -H2 #H1 @(csn_cprs_trans … H) -H /2 width=1/
 ]
diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_vector.ma
index a8663d8ba..92aae5465 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_vector.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_vector.ma
@@ -26,5 +26,5 @@ interpretation
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma csnv_inv_cons: ∀L,T,Ts. L ⊢ ⬇* T :: Ts → L ⊢ ⬇* T ∧ L ⊢ ⬇* Ts.
+lemma csnv_inv_cons: ∀L,T,Ts. L ⊢ ⬇* T @ Ts → L ⊢ ⬇* T ∧ L ⊢ ⬇* Ts.
 normalize // qed-.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_alt.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_alt.ma
new file mode 100644
index 000000000..9c1567460
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_alt.ma
@@ -0,0 +1,190 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/equivalence/cpcs_cpcs.ma".
+include "basic_2/dynamic/nta.ma".
+
+(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************)
+
+(* alternative definition of nta *)
+inductive ntaa (h:sh): lenv → relation term ≝
+| ntaa_sort: ∀L,k. ntaa h L (⋆k) (⋆(next h k))
+| ntaa_ldef: ∀L,K,V,W,U,i. ⇩[0, i] L ≡ K. ⓓV → ntaa h K V W →
+             ⇧[0, i + 1] W ≡ U → ntaa h L (#i) U
+| ntaa_ldec: ∀L,K,W,V,U,i. ⇩[0, i] L ≡ K. ⓛW → ntaa h K W V →
+             ⇧[0, i + 1] W ≡ U → ntaa h L (#i) U
+| ntaa_bind: ∀I,L,V,W,T,U. ntaa h L V W → ntaa h (L. ⓑ{I} V) T U →
+             ntaa h L (ⓑ{I}V.T) (ⓑ{I}V.U)
+| ntaa_appl: ∀L,V,W,T,U. ntaa h L V W → ntaa h L (ⓛW.T) (ⓛW.U) →
+             ntaa h L (ⓐV.ⓛW.T) (ⓐV.ⓛW.U)
+| ntaa_pure: ∀L,V,W,T,U. ntaa h L T U → ntaa h L (ⓐV.U) W →
+             ntaa h L (ⓐV.T) (ⓐV.U)
+| ntaa_cast: ∀L,T,U,W. ntaa h L T U → ntaa h L U W → ntaa h L (ⓣU. T) U
+| ntaa_conv: ∀L,T,U1,U2,V2. ntaa h L T U1 → L ⊢ U1 ⬌* U2 → ntaa h L U2 V2 →
+             ntaa h L T U2
+.
+
+interpretation "native type assignment (term) alternative"
+   'NativeTypeAlt h L T U = (ntaa h L T U).
+
+(* Advanced inversion lemmas ************************************************)
+
+fact ntaa_inv_bind1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T :: U → ∀J,X,Y. T = ⓑ{J}Y.X →
+                         ∃∃Z1,Z2. ⦃h, L⦄ ⊢ Y :: Z1 & ⦃h, L.ⓑ{J}Y⦄ ⊢ X :: Z2 &
+                                  L ⊢ ⓑ{J}Y.Z2 ⬌* U.
+#h #L #T #U #H elim H -L -T -U
+[ #L #k #J #X #Y #H destruct
+| #L #K #V #W #U #i #_ #_ #_ #_ #J #X #Y #H destruct
+| #L #K #W #V #U #i #_ #_ #_ #_ #J #X #Y #H destruct
+| #I #L #V #W #T #U #HVW #HTU #_ #_ #J #X #Y #H destruct /2 width=3/
+| #L #V #W #T #U #_ #_ #_ #_ #J #X #Y #H destruct
+| #L #V #W #T #U #_ #_ #_ #_ #J #X #Y #H destruct
+| #L #T #U #W #_ #_ #_ #_ #J #X #Y #H destruct
+| #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #J #X #Y #H destruct
+  elim (IHTU1 ????) -IHTU1 [5: // |2,3,4: skip ] #Z1 #Z2 #HZ1 #HZ2 #HU1
+  lapply (cpcs_trans … HU1 … HU12) -U1 /2 width=3/
+]
+qed.
+
+lemma ntaa_inv_bind1: ∀h,J,L,Y,X,U. ⦃h, L⦄ ⊢ ⓑ{J}Y.X :: U →
+                      ∃∃Z1,Z2. ⦃h, L⦄ ⊢ Y :: Z1 & ⦃h, L.ⓑ{J}Y⦄ ⊢ X :: Z2 &
+                               L ⊢ ⓑ{J}Y.Z2 ⬌* U.
+/2 width=3/ qed-.                            
+
+lemma ntaa_nta: ∀h,L,T,U. ⦃h, L⦄ ⊢ T :: U → ⦃h, L⦄ ⊢ T : U.
+#h #L #T #U #H elim H -L -T -U
+// /2 width=1/ /2 width=2/ /2 width=3/ /2 width=6/
+qed-.
+
+(* Properties on relocation *************************************************)
+
+lemma ntaa_lift: ∀h,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 :: U1 → ∀L2,d,e. ⇩[d, e] L2 ≡ L1 →
+                 ∀T2. ⇧[d, e] T1 ≡ T2 → ∀U2. ⇧[d, e] U1 ≡ U2 → ⦃h, L2⦄ ⊢ T2 :: U2.
+#h #L1 #T1 #U1 #H elim H -L1 -T1 -U1
+[ #L1 #k #L2 #d #e #HL21 #X1 #H1 #X2 #H2
+  >(lift_inv_sort1 … H1) -X1
+  >(lift_inv_sort1 … H2) -X2 //
+| #L1 #K1 #V1 #W1 #W #i #HLK1 #_ #HW1 #IHVW1 #L2 #d #e #HL21 #X #H #U2 #HWU2
+  elim (lift_inv_lref1 … H) * #Hid #H destruct
+  [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // #W2 #HW12 #HWU2
+    elim (ldrop_trans_le … HL21 … HLK1 ?) -L1 /2 width=2/ #X #HLK2 #H
+    elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K2 #V2 #HK21 #HV12 #H destruct
+    /3 width=8/
+  | lapply (lift_trans_be … HW1 … HWU2 ? ?) -W // /2 width=1/ #HW1U2
+    lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/
+  ]
+| #L1 #K1 #W1 #V1 #W #i #HLK1 #_ #HW1 #IHWV1 #L2 #d #e #HL21 #X #H #U2 #HWU2
+  elim (lift_inv_lref1 … H) * #Hid #H destruct
+  [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // <minus_plus #W #HW1 #HWU2
+    elim (ldrop_trans_le … HL21 … HLK1 ?) -L1 /2 width=2/ #X #HLK2 #H
+    elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K2 #W2 #HK21 #HW12 #H destruct
+    lapply (lift_mono … HW1 … HW12) -HW1 #H destruct
+    elim (lift_total V1 (d-i-1) e) /3 width=8/
+  | lapply (lift_trans_be … HW1 … HWU2 ? ?) -W // /2 width=1/ #HW1U2
+    lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/
+  ]
+| #I #L1 #V1 #W1 #T1 #U1 #_ #_ #IHVW1 #IHTU1 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
+  elim (lift_inv_bind1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H destruct
+  elim (lift_inv_bind1 … H2) -H2 #X #U2 #H1 #HU12 #H2 destruct
+  lapply (lift_mono … H1 … HV12) -H1 #H destruct
+  elim (lift_total W1 d e) /4 width=6/
+| #L1 #V1 #W1 #T1 #U1 #_ #_ #IHVW1 #IHTU1 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
+  elim (lift_inv_flat1 … H1) -H1 #V2 #X #HV12 #H1 #H destruct
+  elim (lift_inv_bind1 … H1) -H1 #W2 #T2 #HW12 #HT12 #H destruct
+  elim (lift_inv_flat1 … H2) -H2 #Y2 #X #HY #H2 #H destruct
+  elim (lift_inv_bind1 … H2) -H2 #X2 #U2 #HX #HU12 #H destruct
+  lapply (lift_mono … HY … HV12) -HY #H destruct
+  lapply (lift_mono … HX … HW12) -HX #H destruct /4 width=6/
+| #L1 #V1 #W1 #T1 #U1 #_ #_ #IHTU1 #IHUW1 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
+  elim (lift_inv_flat1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H destruct
+  elim (lift_inv_flat1 … H2) -H2 #X #U2 #H1 #HU12 #H2 destruct
+  lapply (lift_mono … H1 … HV12) -H1 #H destruct
+  elim (lift_total W1 d e) /4 width=6/
+| #L1 #T1 #U1 #W1 #_ #_ #IHTU1 #IHUW1 #L2 #d #e #HL21 #X #H #U2 #HU12
+  elim (lift_inv_flat1 … H) -H #X2 #T2 #HUX2 #HT12 #H destruct
+  lapply (lift_mono … HUX2 … HU12) -HUX2 #H destruct
+  elim (lift_total W1 d e) /3 width=6/
+| #L1 #T1 #U11 #U12 #V12 #_ #HU112 #_ #IHTU11 #IHUV12 #L2 #d #e #HL21 #U1 #HTU1 #U2 #HU12
+  elim (lift_total U11 d e) #U #HU11
+  elim (lift_total V12 d e) #V22 #HV122
+  lapply (cpcs_lift … HL21 … HU11 … HU12 HU112) -HU112 /3 width=6/
+]
+qed.
+
+(* Advanced forvard lemmas **************************************************)
+
+lemma ntaa_fwd_correct: ∀h,L,T,U. ⦃h, L⦄ ⊢ T :: U → ∃T0. ⦃h, L⦄ ⊢ U :: T0.
+#h #L #T #U #H elim H -L -T -U
+[ /2 width=2/
+| #L #K #V #W #W0 #i #HLK #_ #HW0 * #V0 #HWV0
+  lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
+  elim (lift_total V0 0 (i+1)) /3 width=10/
+| #L #K #W #V #V0 #i #HLK #HWV #HWV0 #_
+  lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
+  elim (lift_total V 0 (i+1)) /3 width=10/
+| #I #L #V #W #T #U #HVW #_ #_ * /3 width=2/
+| #L #V #W #T #U #HVW #_ #_ * #X #H
+  elim (ntaa_inv_bind1 … H) -H /4 width=2/
+| #L #V #W #T #U #_ #HUW * #T0 #HUT0 /3 width=2/
+| /2 width=2/
+| /2 width=2/
+]
+qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma nta_ntaa: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ⦃h, L⦄ ⊢ T :: U.
+#h #L #T #U #H elim H -L -T -U
+// /2 width=1/ /2 width=2/ /2 width=3/ /2 width=6/
+#L #T #U #_ #HTU
+elim (ntaa_fwd_correct … HTU) /2 width=2/
+qed.
+
+(* Advanced eliminators *****************************************************)
+
+lemma nta_ind_alt: ∀h. ∀R:lenv→relation term.
+   (∀L,k. R L ⋆k ⋆(next h k)) →
+   (∀L,K,V,W,U,i.
+      ⇩[O, i] L ≡ K.ⓓV → ⦃h, K⦄ ⊢ V : W → ⇧[O, i + 1] W ≡ U →
+      R K V W → R L (#i) U 
+   ) →
+   (∀L,K,W,V,U,i.
+      ⇩[O, i] L ≡ K.ⓛW → ⦃h, K⦄ ⊢ W : V → ⇧[O, i + 1] W ≡ U →
+      R K W V → R L (#i) U
+   ) →
+   (∀I,L,V,W,T,U.
+      ⦃h, L⦄ ⊢ V : W → ⦃h, L.ⓑ{I}V⦄ ⊢ T : U →
+      R L V W → R (L.ⓑ{I}V) T U → R L (ⓑ{I}V.T) (ⓑ{I}V.U)
+   ) →
+   (∀L,V,W,T,U.
+      ⦃h, L⦄ ⊢ V : W → ⦃h, L⦄ ⊢ (ⓛW.T):(ⓛW.U) →
+      R L V W →R L (ⓛW.T) (ⓛW.U) →R L (ⓐV.ⓛW.T) (ⓐV.ⓛW.U)
+   ) →
+   (∀L,V,W,T,U.
+      ⦃h, L⦄ ⊢ T : U → ⦃h, L⦄ ⊢ (ⓐV.U) : W →
+      R L T U → R L (ⓐV.U) W → R L (ⓐV.T) (ⓐV.U)
+   ) →
+   (∀L,T,U,W.
+      ⦃h, L⦄ ⊢ T : U → ⦃h, L⦄ ⊢ U : W →
+      R L T U → R L U W → R L (ⓣU.T) U
+   ) →
+   (∀L,T,U1,U2,V2.
+      ⦃h, L⦄ ⊢ T : U1 → L ⊢ U1 ⬌* U2 → ⦃h, L⦄ ⊢ U2 : V2 →
+      R L T U1 →R L U2 V2 →R L T U2
+   ) →
+   ∀L,T,U. ⦃h, L⦄ ⊢ T : U → R L T U.
+#h #R #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #L #T #U #H elim (nta_ntaa … H) -L -T -U
+// /3 width=1 by ntaa_nta/ /3 width=3 by ntaa_nta/ /3 width=4 by ntaa_nta/
+/3 width=7 by ntaa_nta/
+qed-.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_delift.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_delift.ma
new file mode 100644
index 000000000..e36695081
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_delift.ma
@@ -0,0 +1,84 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/unfold/delift_lift.ma".
+include "basic_2/unfold/thin_ldrop.ma".
+include "basic_2/equivalence/cpcs_delift.ma".
+include "basic_2/dynamic/nta_nta.ma".
+
+(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************)
+
+(* Properties on reverse basic term relocation ******************************)
+
+(* Basic_1: was only: ty3_gen_cabbr *)
+axiom thin_nta_delift_conf: ∀h,L1,T1,X1. ⦃h, L1⦄ ⊢ T1 : X1 →
+                            ∀L2,d,e. L1 [d, e] ≡ L2 →
+                            ∀T2. L1 ⊢ T1 [d, e] ≡ T2 →
+                            ∃∃U1,U2. ⦃h, L2⦄ ⊢ T2 : U2 & L1 ⊢ U1 [d, e] ≡ U2 &
+                                     L1 ⊢ U1 ⬌* X1.
+(*
+#h #L1 #T1 #U1 #H @(nta_ind_alt … H) -L1 -T1 -U1
+[ #L1 #k #L2 #d #e #HL12 #X #H
+  >(delift_inv_sort1 … H) -X /2 width=5/
+| #L1 #K1 #V1 #W1 #U1 #i #HLK1 #_ #HWU1 #IHVW1 #L2 #d #e #HL12 #X #H
+(*
+  elim (delift_inv_lref1 … H) -H *
+  [ #Hid #H destruct
+    elim (thin_ldrop_conf_le … HL12 … HLK1 ?) -HL12 /2 width=2/ #X #H #HLK2
+    lapply (ldrop_fwd_ldrop2 … HLK1) -HLK1 #HLK1
+    elim (thin_inv_delift1 … H ?) -H /2 width=1/ #K2 #V2 #HK12 #HV12 #H destruct
+    elim (IHVW1 … HK12 … HV12) -IHVW1 -HK12 -HV12 #W2 #HVW2 #HW12
+    elim (lift_total W2 0 (i+1)) #U2 #HWU2
+    @(ex2_1_intro … U2)
+    [ /2 width=6/
+    | -HVW2 -HLK2 
+    ]
+  |
+  |
+  ]
+*)
+|
+|
+|
+| #L1 #V1 #W1 #T1 #U1 #_ #_ #IHTU1 #IHVW1 #L2 #d #e #HL12 #X #H
+  elim (delift_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
+(*  
+  elim (IHTU1 … HL12 … HT12) -T1 #U2 #HTU2 #HU12
+  elim (IHVW1 … HL12 (ⓐV2.U2) ?) -IHVW1 -HL12
+  [ /3 width=5/ | /2 width=1/ ]
+*)
+| #L1 #T1 #X1 #Y1 #_ #_ #IHTX1 #IHXY1 #L2 #d #e #HL12 #X #H
+  elim (delift_inv_flat1 … H) -H #X2 #T2 #HX12 #HT12 #H destruct
+  elim (IHTX1 … HL12 … HT12) -T1 #U1 #U2 #HTU2 #HU12 #HUX1
+  elim (IHXY1 … HL12 … HX12) -IHXY1 #W1 #W2 #HXW2 #_ #_ -Y1 -W1
+  lapply (thin_cpcs_delift_mono … HUX1 … HL12 … HU12 … HX12) -HL12 -HX12 /4 width=5/
+| #L1 #T1 #X11 #X12 #V1 #_ #HX112 #_ #IHT1 #_ #L2 #d #e #HL12 #T2 #HT12
+  elim (IHT1 … HL12 … HT12) -T1 -HL12 #U21 #U22 #HTU22 #HU212 #HUX211
+  lapply (cpcs_trans … HUX211 … HX112) -X11 /2 width=5/
+]
+*)
+lemma nta_inv_lift1_delift: ∀h,L1,T1,X. ⦃h, L1⦄ ⊢ T1 : X →
+                            ∀L2,d,e. ⇩[d, e] L1 ≡ L2 → ∀T2. ⇧[d, e] T2 ≡ T1 →
+                            ∃∃U1,U2. ⦃h, L2⦄ ⊢ T2 : U2 & L1 ⊢ U1 [d, e] ≡ U2 &
+                                     L1 ⊢ U1 ⬌* X.
+/3 width=3/ qed-.
+
+lemma nta_inv_lift1: ∀h,L1,T1,X. ⦃h, L1⦄ ⊢ T1 : X →
+                     ∀L2,d,e. ⇩[d, e] L1 ≡ L2 → ∀T2. ⇧[d, e] T2 ≡ T1 →
+                     ∃∃U1,U2. ⦃h, L2⦄ ⊢ T2 : U2 & ⇧[d, e] U2 ≡ U1 &
+                              L1 ⊢ U1 ⬌* X.
+#h #L1 #T1 #X #H #L2 #d #e #HL12 #T2 #HT21
+elim (nta_inv_lift1_delift … H … HL12 … HT21) -T1 -HL12 #U1 #U2 #HTU2 * #U #HU1 #HU2 #HU1X
+lapply (cpcs_cpr_conf … U … HU1X) -HU1X /2 width=3/ -U1 /2 width=5/
+qed-.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_lift.ma
index 1bdb9b1ac..294c1710e 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_lift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_lift.ma
@@ -12,8 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/equivalence/cpcs_cpcs.ma".
-include "basic_2/dynamic/nta.ma".
+include "basic_2/dynamic/nta_alt.ma".
 
 (* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************)
 
@@ -70,28 +69,13 @@ lemma nta_inv_lref1: ∀h,L,U,i. ⦃h, L⦄ ⊢ #i : U →
                      ).
 /2 width=3/ qed-.
 
-fact nta_inv_bind1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀J,X,Y. T = ⓑ{J}Y.X →
-                        ∃∃Z1,Z2. ⦃h, L⦄ ⊢ Y : Z1 & ⦃h, L.ⓑ{J}Y⦄ ⊢ X : Z2 &
-                                 L ⊢ ⓑ{J}Y.Z2 ⬌* U.
-#h #L #T #U #H elim H -L -T -U
-[ #L #k #J #X #Y #H destruct
-| #L #K #V #W #U #i #_ #_ #_ #_ #J #X #Y #H destruct
-| #L #K #W #V #U #i #_ #_ #_ #_ #J #X #Y #H destruct
-| #I #L #V #W #T #U #HVW #HTU #_ #_ #J #X #Y #H destruct /2 width=3/
-| #L #V #W #T #U #_ #_ #_ #_ #J #X #Y #H destruct
-| #L #V #W #T #U #_ #_ #_ #_ #J #X #Y #H destruct
-| #L #T #U #_ #_ #J #X #Y #H destruct
-| #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #J #X #Y #H destruct
-  elim (IHTU1 ????) -IHTU1 [5: // |2,3,4: skip ] #Z1 #Z2 #HZ1 #HZ2 #HU1
-  lapply (cpcs_trans … HU1 … HU12) -U1 /2 width=3/
-]
-qed.
-
 (* Basic_1: was: ty3_gen_bind *)
-lemma nta_inv_bind1: ∀h,J,L,Y,X,U. ⦃h, L⦄ ⊢ ⓑ{J}Y.X : U →
-                     ∃∃Z1,Z2. ⦃h, L⦄ ⊢ Y : Z1 & ⦃h, L.ⓑ{J}Y⦄ ⊢ X : Z2 &
-                              L ⊢ ⓑ{J}Y.Z2 ⬌* U.
-/2 width=3/ qed-.                            
+lemma nta_inv_bind1: ∀h,I,L,Y,X,U. ⦃h, L⦄ ⊢ ⓑ{I}Y.X : U →
+                     ∃∃Z1,Z2. ⦃h, L⦄ ⊢ Y : Z1 & ⦃h, L.ⓑ{I}Y⦄ ⊢ X : Z2 &
+                              L ⊢ ⓑ{I}Y.Z2 ⬌* U.
+#h #I #L #Y #X #U #H
+elim (ntaa_inv_bind1 … (nta_ntaa … H)) -H /3 width=3 by ntaa_nta, ex3_2_intro/
+qed-.
 
 fact nta_inv_cast1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀X,Y. T = ⓣY.X →
                      ⦃h, L⦄ ⊢ X : Y ∧ L ⊢ Y ⬌* U.
@@ -113,80 +97,33 @@ qed.
 lemma nta_inv_cast1: ∀h,L,X,Y,U. ⦃h, L⦄ ⊢ ⓣY.X : U →  ⦃h, L⦄ ⊢ X : Y ∧ L ⊢ Y ⬌* U.
 /2 width=3/ qed-.
 
-(* Properties on relocation *************************************************)
+(* Advanced forvard lemmas **************************************************)
 
-(* Basic_1: was: ty3_lift *)
-lemma nta_lift: ∀h,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 : U1 → ∀L2,d,e. ⇩[d, e] L2 ≡ L1 →
-                ∀T2. ⇧[d, e] T1 ≡ T2 → ∀U2. ⇧[d, e] U1 ≡ U2 → ⦃h, L2⦄ ⊢ T2 : U2.
-#h #L1 #T1 #U1 #H elim H -L1 -T1 -U1
-[ #L1 #k #L2 #d #e #HL21 #X1 #H1 #X2 #H2
-  >(lift_inv_sort1 … H1) -X1
-  >(lift_inv_sort1 … H2) -X2 //
-| #L1 #K1 #V1 #W1 #W #i #HLK1 #_ #HW1 #IHVW1 #L2 #d #e #HL21 #X #H #U2 #HWU2
-  elim (lift_inv_lref1 … H) * #Hid #H destruct
-  [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // #W2 #HW12 #HWU2
-    elim (ldrop_trans_le … HL21 … HLK1 ?) -L1 /2 width=2/ #X #HLK2 #H
-    elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K2 #V2 #HK21 #HV12 #H destruct
-    /3 width=8/
-  | lapply (lift_trans_be … HW1 … HWU2 ? ?) -W // /2 width=1/ #HW1U2
-    lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/
-  ]
-| #L1 #K1 #W1 #V1 #W #i #HLK1 #_ #HW1 #IHWV1 #L2 #d #e #HL21 #X #H #U2 #HWU2
-  elim (lift_inv_lref1 … H) * #Hid #H destruct
-  [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // <minus_plus #W #HW1 #HWU2
-    elim (ldrop_trans_le … HL21 … HLK1 ?) -L1 /2 width=2/ #X #HLK2 #H
-    elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K2 #W2 #HK21 #HW12 #H destruct
-    lapply (lift_mono … HW1 … HW12) -HW1 #H destruct
-    elim (lift_total V1 (d-i-1) e) /3 width=8/
-  | lapply (lift_trans_be … HW1 … HWU2 ? ?) -W // /2 width=1/ #HW1U2
-    lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/
-  ]
-| #I #L1 #V1 #W1 #T1 #U1 #_ #_ #IHVW1 #IHTU1 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
-  elim (lift_inv_bind1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H destruct
-  elim (lift_inv_bind1 … H2) -H2 #X #U2 #H1 #HU12 #H2 destruct
-  lapply (lift_mono … H1 … HV12) -H1 #H destruct
-  elim (lift_total W1 d e) /4 width=6/
-| #L1 #V1 #W1 #T1 #U1 #_ #_ #IHVW1 #IHTU1 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
-  elim (lift_inv_flat1 … H1) -H1 #V2 #X #HV12 #H1 #H destruct
-  elim (lift_inv_bind1 … H1) -H1 #W2 #T2 #HW12 #HT12 #H destruct
-  elim (lift_inv_flat1 … H2) -H2 #Y2 #X #HY #H2 #H destruct
-  elim (lift_inv_bind1 … H2) -H2 #X2 #U2 #HX #HU12 #H destruct
-  lapply (lift_mono … HY … HV12) -HY #H destruct
-  lapply (lift_mono … HX … HW12) -HX #H destruct /4 width=6/
-| #L1 #V1 #W1 #T1 #U1 #_ #_ #IHTU1 #IHUW1 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
-  elim (lift_inv_flat1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H destruct
-  elim (lift_inv_flat1 … H2) -H2 #X #U2 #H1 #HU12 #H2 destruct
-  lapply (lift_mono … H1 … HV12) -H1 #H destruct
-  elim (lift_total W1 d e) /4 width=6/
-| #L1 #T1 #U1 #_ #IHTU1 #L2 #d #e #HL21 #X #H #U2 #HU12
-  elim (lift_inv_flat1 … H) -H #X2 #T2 #HUX2 #HT12 #H destruct
-  lapply (lift_mono … HUX2 … HU12) -HUX2 #H destruct /3 width=5/
-| #L1 #T1 #U11 #U12 #V12 #_ #HU112 #_ #IHTU11 #IHUV12 #L2 #d #e #HL21 #U1 #HTU1 #U2 #HU12
-  elim (lift_total U11 d e) #U #HU11
-  elim (lift_total V12 d e) #V22 #HV122
-  lapply (cpcs_lift … HL21 … HU11 … HU12 HU112) -HU112 /3 width=6/
+fact nta_fwd_appl1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀X,Y. T = ⓐY.X →
+                        ∃∃V,W. ⦃h, L⦄ ⊢ Y : W & ⦃h, L⦄ ⊢ X : V & L ⊢ ⓐY.V ⬌* U.
+#h #L #T #U #H elim H -L -T -U
+[ #L #k #X #Y #H destruct
+| #L #K #V #W #U #i #_ #_ #_ #_ #X #Y #H destruct
+| #L #K #W #V #U #i #_ #_ #_ #_ #X #Y #H destruct
+| #I #L #V #W #T #U #_ #_ #_ #_ #X #Y #H destruct
+| #L #V #W #T #U #HVW #HTU #_ #_ #X #Y #H destruct /2 width=3/
+| #L #V #W #T #U #HTU #_ #_ #IHUW #X #Y #H destruct
+  elim (IHUW U Y ?) -IHUW // /2 width=3/
+| #L #T #U #_ #_ #X #Y #H destruct
+| #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #X #Y #H destruct
+  elim (IHTU1 ???) -IHTU1 [4: // |2,3: skip ] #V #W #HYW #HXV #HU1
+  lapply (cpcs_trans … HU1 … HU12) -U1 /2 width=3/
 ]
 qed.
 
-(* Advanced forvard lemmas **************************************************)
+lemma nta_fwd_appl1: ∀h,L,X,Y,U. ⦃h, L⦄ ⊢ ⓐY.X : U →
+                     ∃∃V,W. ⦃h, L⦄ ⊢ Y : W & ⦃h, L⦄ ⊢ X : V & L ⊢ ⓐY.V ⬌* U.
+/2 width=3/ qed-.
 
 (* Basic_1: was: ty3_correct *)
 lemma nta_fwd_correct: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∃T0. ⦃h, L⦄ ⊢ U : T0.
-#h #L #T #U #H elim H -L -T -U
-[ /2 width=2/
-| #L #K #V #W #W0 #i #HLK #_ #HW0 * #V0 #HWV0
-  lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
-  elim (lift_total V0 0 (i+1)) /3 width=10/
-| #L #K #W #V #V0 #i #HLK #HWV #HWV0 #_
-  lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
-  elim (lift_total V 0 (i+1)) /3 width=10/
-| #I #L #V #W #T #U #HVW #_ #_ * /3 width=2/
-| #L #V #W #T #U #HVW #_ #_ * #X #H
-  elim (nta_inv_bind1 … H) -H /4 width=2/
-| #L #V #W #T #U #_ #HUW * #T0 #HUT0 /3 width=2/
-| #L #T #U #_ * /2 width=2/
-| /2 width=2/
-]
+#h #L #T #U #H
+elim (ntaa_fwd_correct … (nta_ntaa … H)) -H /3 width=2 by ntaa_nta, ex_intro/
 qed-.
 
 (* Advanced properties ******************************************************)
@@ -198,3 +135,10 @@ lemma nta_appl_old: ∀h,L,V,W,T,U. ⦃h, L⦄ ⊢ V : W → ⦃h, L⦄ ⊢ T :
 elim (nta_fwd_correct … HTU) #X #H
 elim (nta_inv_bind1 … H) -H /4 width=2/
 qed.
+
+(* Properties on relocation *************************************************)
+
+(* Basic_1: was: ty3_lift *)
+lemma nta_lift: ∀h,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 : U1 → ∀L2,d,e. ⇩[d, e] L2 ≡ L1 →
+                ∀T2. ⇧[d, e] T1 ≡ T2 → ∀U2. ⇧[d, e] U1 ≡ U2 → ⦃h, L2⦄ ⊢ T2 : U2.
+/4 width=9 by ntaa_nta, nta_ntaa, ntaa_lift/ qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_nta.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_nta.ma
new file mode 100644
index 000000000..f0bf7119e
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_nta.ma
@@ -0,0 +1,59 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/dynamic/nta_lift.ma".
+
+(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************)
+
+(* Main properties **********************************************************)
+
+(* Basic_1: was: ty3_unique *)
+theorem nta_mono: ∀h,L,T,U1. ⦃h, L⦄ ⊢ T : U1 → ∀U2. ⦃h, L⦄ ⊢ T : U2 →
+                  L ⊢ U1 ⬌* U2.
+#h #L #T #U1 #H elim H -L -T -U1
+[ #L #k #X #H
+  lapply (nta_inv_sort1 … H) -H //
+| #L #K #V #W11 #W12 #i #HLK #_ #HW112 #IHVW11 #X #H
+  elim (nta_inv_lref1 … H) -H * #K0 #V0 #W21 #W22 #HLK0 #HVW21 #HW212 #HX
+  lapply (ldrop_mono … HLK0 … HLK) -HLK0 #H destruct
+  lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
+  @(cpcs_trans … HX) -X /3 width=9 by cpcs_lift/ (**) (* to slow without trace *)
+| #L #K #W #V1 #V #i #HLK #_ #HWV #_ #X #H
+  elim (nta_inv_lref1 … H) -H * #K0 #W0 #V2 #V0 #HLK0 #_ #HWV0 #HX
+  lapply (ldrop_mono … HLK0 … HLK) -HLK0 -HLK #H destruct
+  lapply (lift_mono … HWV0 … HWV) -HWV0 -HWV #H destruct //
+| #I #L #V #W1 #T #U1 #_ #_ #_ #IHTU1 #X #H
+  elim (nta_inv_bind1 … H) -H #W2 #U2 #_ #HTU2 #H
+  @(cpcs_trans … H) -X /3 width=1/
+| #L #V #W1 #T #U1 #_ #_ #_ #IHTU1 #X #H
+  elim (nta_fwd_appl1 … H) -H #U2 #W2 #_ #HTU2 #H
+  @(cpcs_trans … H) -X /3 width=1/
+| #L #V #W1 #T #U1 #_ #_ #IHTU1 #_ #X #H
+  elim (nta_fwd_appl1 … H) -H #U2 #W2 #_ #HTU2 #H
+  @(cpcs_trans … H) -X /3 width=1/
+| #L #T #U1 #_ #_ #X #H
+  elim (nta_inv_cast1 … H) -H //
+| #L #T #U11 #U12 #V12 #_ #HU112 #_ #IHTU11 #_ #U2 #HTU2
+  @(cpcs_canc_sn … HU112) -U12 /2 width=1/
+]
+qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma nta_cast_alt: ∀h,L,T,W,U. ⦃h, L⦄ ⊢ T : W → ⦃h, L⦄ ⊢ T : U →
+             ⦃h, L⦄ ⊢ ⓣW.T : U.
+#h #L #T #W #U #HTW #HTU
+lapply (nta_mono … HTW … HTU) #HWU
+elim (nta_fwd_correct … HTU) -HTU /3 width=3/
+qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs.ma
index e38825fe1..5ee8d1696 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs.ma
@@ -43,6 +43,9 @@ qed-.
 lemma cpcs_refl: ∀L,T. L ⊢ T ⬌* T.
 /2 width=1/ qed.
 
+lemma cpcs_sym: ∀L,T1,T2. L ⊢ T1 ⬌* T2 → L ⊢ T2 ⬌* T1.
+/3 width=1/ qed.
+
 lemma cpcs_strap1: ∀L,T1,T,T2. L ⊢ T1 ⬌* T → L ⊢ T ⬌ T2 → L ⊢ T1 ⬌* T2.
 /2 width=3/ qed.
 
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
new file mode 100644
index 000000000..58697b9c1
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_delift.ma
@@ -0,0 +1,32 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/unfold/delift_delift.ma".
+include "basic_2/computation/cprs_delift.ma".
+include "basic_2/equivalence/cpcs_cpcs.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************)
+
+(* Properties on inverse basic term relocation ******************************)
+
+(* Basic_1: was only: pc3_gen_cabbr *)
+lemma thin_cpcs_delift_mono: ∀L,U1,U2. L ⊢ U1 ⬌* U2 →
+                             ∀K,d,e. L [d, e] ≡ K → ∀T1. L ⊢ U1 [d, e] ≡ T1 →
+                             ∀T2. L ⊢ U2 [d, e] ≡ T2 → K ⊢ T1 ⬌* T2.
+#L #U1 #U2 #H #K #d #e #HLK #T1 #HTU1 #T2 #HTU2
+elim (cpcs_inv_cprs … H) -H #U #HU1 #HU2
+elim (thin_cprs_delift_conf … HU1 … HLK … HTU1) -U1 #T #HT1 #HUT
+elim (thin_cprs_delift_conf … HU2 … HLK … HTU2) -U2 -HLK #X #HT2 #H
+lapply (delift_mono … H … HUT) -L #H destruct /2 width=3/
+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 e3dee1e0b..69f76386b 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
@@ -35,7 +35,7 @@ lemma cw_shift: ∀K,I,V,T. #[K. ⓑ{I} V, T] < #[K, ②{I} V. T].
 normalize //
 qed.
 
-lemma tw_shift: ∀L,T. #[L, T] ≤ #[L @ T].
+lemma tw_shift: ∀L,T. #[L, T] ≤ #[L @@ T].
 #L elim L //
 #K #I #V #IHL #T
 @transitive_le [3: @IHL |2: /2 width=2/ | skip ]
diff --git a/matita/matita/contribs/lambda_delta/basic_2/notation.ma b/matita/matita/contribs/lambda_delta/basic_2/notation.ma
index ae40690e7..1e1daa375 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/notation.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/notation.ma
@@ -346,6 +346,10 @@ notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 : break term 46 T2 )"
    non associative with precedence 45
    for @{ 'NativeType $h $L $T1 $T2 }.
 
+notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 :: break term 46 T2 )"
+   non associative with precedence 45
+   for @{ 'NativeTypeAlt $h $L $T1 $T2 }.
+
 notation "hvbox( h ⊢ break term 46 L1 : ⊑ break term 46 L2 )"
    non associative with precedence 45
    for @{ 'CrSubEqN $h $L1 $L2 }.
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 4fa94673e..aadf05b82 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
@@ -43,7 +43,7 @@ qed.
 
 (* Advanced forward lemmas **************************************************)
 
-lemma cpr_shift_fwd: ∀L,T1,T2. L ⊢ T1 ➡ T2 → L @ T1 ➡ L @ T2.
+lemma cpr_shift_fwd: ∀L,T1,T2. L ⊢ T1 ➡ T2 → L @@ T1 ➡ L @@ T2.
 #L elim L -L
 [ #T1 #T2 #HT12 @(cpr_inv_atom … HT12)
 | normalize /3 width=1/
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_delift.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_delift.ma
new file mode 100644
index 000000000..7437e6ac8
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_delift.ma
@@ -0,0 +1,37 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/unfold/thin_delift.ma".
+include "basic_2/reducibility/tpr_delift.ma".
+include "basic_2/reducibility/cpr.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************)
+
+(* Properties on inverse basic term relocation ******************************)
+
+(* Basic_1: was only: pr2_gen_cabbr *)
+lemma thin_cpr_delift_conf: ∀L,U1,U2. L ⊢ U1 ➡ U2 →
+                            ∀K,d,e. L [d, e] ≡ K → ∀T1. L ⊢ U1 [d, e] ≡ T1 →
+                            ∃∃T2. K ⊢ T1 ➡ T2 & L ⊢ U2 [d, e] ≡ T2.
+#L #U1 #U2 * #U #HU1 #HU2 #K #d #e #HLK #T1 #HTU1
+elim (tpr_delift_conf … HU1 … HTU1) -U1 #T #HT1 #HUT
+elim (le_or_ge (|L|) d) #Hd
+[ elim (thin_delift_tpss_conf_le … HU2 … HUT … HLK ?)
+| elim (le_or_ge (|L|) (d+e)) #Hde
+  [ elim (thin_delift_tpss_conf_le_up … HU2 … HUT … HLK ? ? ?)
+  | elim (thin_delift_tpss_conf_be … HU2 … HUT … HLK ? ?)
+  ]
+] -U -HLK // -Hd [2,3: -Hde] #T2 #HT2
+lapply (cpr_intro … HT1 HT2) -T /2 width=3/
+qed.
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
new file mode 100644
index 000000000..3cbff71ce
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_delift.ma
@@ -0,0 +1,27 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/unfold/delift.ma".
+include "basic_2/reducibility/tpr_tpss.ma".
+
+(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
+
+(* Properties on inverse basic term relocation ******************************)
+
+lemma tpr_delift_conf: ∀U1,U2. U1 ➡ U2 → ∀L,T1,d,e. L ⊢ U1 [d, e] ≡ T1 →
+                       ∃∃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/
+qed. 
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 ec95afc02..40032ef8a 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
@@ -91,3 +91,8 @@ lemma tpr_tpss_ltpr: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. T1 ➡ T2 →
   lapply (tpss_trans_eq … HT2 … HTU2) -T /2 width=3/
 ]
 qed.
+
+lemma tpr_tpss_conf: ∀T1,T2. T1 ➡ T2 →
+                     ∀L,U1,d,e. L ⊢ T1 [d, e] ▶* U1 →
+                     ∃∃U2. U1 ➡ U2 & L ⊢ T2 [d, e] ▶* U2.
+/2 width=5/ qed. 
diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/lift_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/lift_vector.ma
index d812f1cda..35ecb6535 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/substitution/lift_vector.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/lift_vector.ma
@@ -21,7 +21,7 @@ inductive liftv (d,e:nat) : relation (list term) ≝
 | liftv_nil : liftv d e ◊ ◊
 | liftv_cons: ∀T1s,T2s,T1,T2.
               ⇧[d, e] T1 ≡ T2 → liftv d e T1s T2s →
-              liftv d e (T1 :: T1s) (T2 :: T2s)
+              liftv d e (T1 @ T1s) (T2 @ T2s)
 .
 
 interpretation "relocation (vector)" 'RLift d e T1s T2s = (liftv d e T1s T2s).
@@ -37,18 +37,18 @@ lemma liftv_inv_nil1: ∀T2s,d,e. ⇧[d, e] ◊ ≡ T2s → T2s = ◊.
 /2 width=5/ qed-.
 
 fact liftv_inv_cons1_aux: ∀T1s,T2s,d,e. ⇧[d, e] T1s ≡ T2s →
-                          ∀U1,U1s. T1s = U1 :: U1s →
+                          ∀U1,U1s. T1s = U1 @ U1s →
                           ∃∃U2,U2s. ⇧[d, e] U1 ≡ U2 & ⇧[d, e] U1s ≡ U2s &
-                                    T2s = U2 :: U2s.
+                                    T2s = U2 @ U2s.
 #T1s #T2s #d #e * -T1s -T2s
 [ #U1 #U1s #H destruct
 | #T1s #T2s #T1 #T2 #HT12 #HT12s #U1 #U1s #H destruct /2 width=5/
 ]
 qed.
 
-lemma liftv_inv_cons1: ∀U1,U1s,T2s,d,e. ⇧[d, e] U1 :: U1s ≡ T2s →
+lemma liftv_inv_cons1: ∀U1,U1s,T2s,d,e. ⇧[d, e] U1 @ U1s ≡ T2s →
                        ∃∃U2,U2s. ⇧[d, e] U1 ≡ U2 & ⇧[d, e] U1s ≡ U2s &
-                                 T2s = U2 :: U2s.
+                                 T2s = U2 @ U2s.
 /2 width=3/ qed-.
 
 (* Basic properties *********************************************************)
diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/tps_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/tps_lift.ma
index 581f1fda5..ce4c5815b 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/substitution/tps_lift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/tps_lift.ma
@@ -262,10 +262,10 @@ qed.
                                         (le d i) -> (lt i (plus d h)) ->
 				        (EX u1 | t1 = (lift (minus (plus d h) (S i)) (S i) u1)).
 *)
-lemma tps_inv_lift1_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶ U2 →
-                        ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
-                        d ≤ dt → dt ≤ d + e → d + e ≤ dt + et →
-                        ∃∃T2. K ⊢ T1 [d, dt + et - (d + e)] ▶ T2 & ⇧[d, e] T2 ≡ U2.
+lemma tps_inv_lift1_ge_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶ U2 →
+                           ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
+                           d ≤ dt → dt ≤ d + e → d + e ≤ dt + et →
+                           ∃∃T2. K ⊢ T1 [d, dt + et - (d + e)] ▶ T2 & ⇧[d, e] T2 ≡ U2.
 #L #U1 #U2 #dt #et #HU12 #K #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet
 elim (tps_split_up … HU12 (d + e) ? ?) -HU12 // -Hdedet #U #HU1 #HU2
 lapply (tps_weak … HU1 d e ? ?) -HU1 // [ >commutative_plus /2 width=1/ ] -Hddt -Hdtde #HU1
@@ -281,3 +281,14 @@ lemma tps_inv_lift1_be_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶ U2 →
 lapply (tps_weak … HU12 dt (d + e - dt) ? ?) -HU12 // /2 width=3/ -Hdetde #HU12
 elim (tps_inv_lift1_be … HU12 … HLK … HTU1 ? ?) -U1 -L // /2 width=3/
 qed.
+
+lemma tps_inv_lift1_le_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶ U2 →
+                           ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
+                           dt ≤ d → d ≤ dt + et → dt + et ≤ d + e →
+                           ∃∃T2. K ⊢ T1 [dt, d - dt] ▶ T2 & ⇧[d, e] T2 ≡ U2.
+#L #U1 #U2 #dt #et #HU12 #K #d #e #HLK #T1 #HTU1 #Hdtd #Hddet #Hdetde
+elim (tps_split_up … HU12 d ? ?) -HU12 // #U #HU1 #HU2
+elim (tps_inv_lift1_le … HU1 … HLK … HTU1 ?) -U1 [2: >commutative_plus /2 width=1/ ] -Hdtd #T #HT1 #HTU
+lapply (tps_weak … HU2 d e ? ?) -HU2 // [ >commutative_plus <plus_minus_m_m // ] -Hddet -Hdetde #HU2
+lapply (tps_inv_lift1_eq … HU2 … HTU) -L #H destruct /2 width=3/
+qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma
index 7fbf16fbd..eb9124089 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma
@@ -14,12 +14,12 @@
 
 include "basic_2/unfold/tpss.ma".
 
-(* INVERSE TERM RELOCATION  *************************************************)
+(* INVERSE BASIC TERM RELOCATION  *******************************************)
 
 definition delift: nat → nat → lenv → relation term ≝
                    λd,e,L,T1,T2. ∃∃T. L ⊢ T1 [d, e] ▶* T & ⇧[d, e] T2 ≡ T.
 
-interpretation "inverse relocation (term)"
+interpretation "inverse basic relocation (term)"
    'TSubst L T1 d e T2 = (delift d e L T1 T2).
 
 (* Basic properties *********************************************************)
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 a53fd9f5d..25d13702a 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
@@ -14,9 +14,9 @@
 
 include "basic_2/unfold/delift_lift.ma".
 
-(* INVERSE TERM RELOCATION  *************************************************)
+(* INVERSE BASIC TERM RELOCATION  *******************************************)
 
-(* alternative definition of inverse relocation *)
+(* alternative definition of inverse basic term relocation *)
 inductive delifta: nat → nat → lenv → relation term ≝
 | delifta_sort   : ∀L,d,e,k. delifta d e L (⋆k) (⋆k)
 | delifta_lref_lt: ∀L,d,e,i. i < d → delifta d e L (#i) (#i)
@@ -33,7 +33,7 @@ inductive delifta: nat → nat → lenv → relation term ≝
                    delifta d e L (ⓕ{I} V1. T1) (ⓕ{I} V2. T2)
 .
 
-interpretation "inverse relocation (term) alternative"
+interpretation "inverse basic relocation (term) alternative"
    'TSubstAlt L T1 d e T2 = (delifta d e L T1 T2).
 
 (* Basic properties *********************************************************)
diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_delift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_delift.ma
index a23501653..753e88796 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_delift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_delift.ma
@@ -15,7 +15,7 @@
 include "basic_2/unfold/tpss_tpss.ma".
 include "basic_2/unfold/delift.ma".
 
-(* INVERSE TERM RELOCATION  *************************************************)
+(* INVERSE BASIC TERM RELOCATION  *******************************************)
 
 (* Main properties **********************************************************)
 
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 a7f31fb80..837e160e6 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
@@ -15,7 +15,7 @@
 include "basic_2/unfold/tpss_lift.ma".
 include "basic_2/unfold/delift.ma".
 
-(* INVERSE TERM RELOCATION  *************************************************)
+(* INVERSE BASIC TERM RELOCATION  *******************************************)
 
 (* Advanced properties ******************************************************)
 
@@ -28,7 +28,7 @@ lapply (lift_trans_be … HV2 … HVU ? ?) -HV2 // >minus_plus <plus_minus_m_m
 /2 width=1/ /3 width=6/
 qed.
  
-(* Advanced forward lemmas **************************************************)
+(* Advanced inversion lemmas ************************************************)
 
 lemma delift_inv_lref1_lt: ∀L,U2,i,d,e. L ⊢ #i [d, e] ≡ U2 → i < d → U2 = #i.
 #L #U2 #i #d #e * #U #HU #HU2 #Hid
@@ -82,7 +82,7 @@ elim (lt_or_ge i d) #Hdi
 ]
 qed-.
 
-(* Relocation properties ****************************************************)
+(* Properties on basic term relocation **************************************)
 
 lemma delift_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≡ T2 →
                       ∀L,U1,d,e. dt + et ≤ d → ⇩[d, e] L ≡ K →
diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_ltpss.ma
index 7bcab46fa..a6d39c1c9 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_ltpss.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_ltpss.ma
@@ -15,7 +15,7 @@
 include "basic_2/unfold/ltpss_ltpss.ma".
 include "basic_2/unfold/delift.ma".
 
-(* INVERSE TERM RELOCATION  *************************************************)
+(* INVERSE BASIC TERM RELOCATION  *******************************************)
 
 (* Properties on partial unfold on local environments ***********************)
 
diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_tpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_tpss.ma
index b7bc126df..5ba077c6d 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_tpss.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_tpss.ma
@@ -15,10 +15,44 @@
 include "basic_2/unfold/tpss_tpss.ma".
 include "basic_2/unfold/delift.ma".
 
-(* INVERSE TERM RELOCATION  *************************************************)
+(* INVERSE BASIC TERM RELOCATION  *******************************************)
 
 (* Properties on partial unfold on terms ************************************)
 
+lemma delift_tpss_conf_le: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶* U2 →
+                           ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
+                           ∀K. ⇩[dd, ee] L ≡ K → d + e ≤ dd →
+                           ∃∃T2. K ⊢ T1 [d, e] ▶* T2 & L ⊢ U2 [dd, ee] ≡ T2.
+#L #U1 #U2 #d #e #HU12 #T1 #dd #ee * #X1 #HUX1 #HTX1 #K #HLK #H1
+elim (tpss_conf_eq … HU12 … HUX1) -U1 #U1 #HU21 #HXU1
+elim (tpss_inv_lift1_le … HXU1 … HLK … HTX1 ?) -X1 -HLK // -H1 /3 width=5/
+qed.
+
+lemma delift_tps_conf_le: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶ U2 →
+                          ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
+                          ∀K. ⇩[dd, ee] L ≡ K → d + e ≤ dd →
+                          ∃∃T2. K ⊢ T1 [d, e] ▶* T2 & L ⊢ U2 [dd, ee] ≡ T2.
+/3 width=3/ qed.
+
+lemma delift_tpss_conf_le_up: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶* U2 →
+                              ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
+                              ∀K. ⇩[dd, ee] L ≡ K →
+                              d ≤ dd → dd ≤ d + e → d + e ≤ dd + ee →
+                              ∃∃T2. K ⊢ T1 [d, dd - d] ▶* T2 &
+                                    L ⊢ U2 [dd, ee] ≡ T2.
+#L #U1 #U2 #d #e #HU12 #T1 #dd #ee * #X1 #HUX1 #HTX1 #K #HLK #H1 #H2 #H3
+elim (tpss_conf_eq … HU12 … HUX1) -U1 #U1 #HU21 #HXU1
+elim (tpss_inv_lift1_le_up … HXU1 … HLK … HTX1 ? ? ?) -X1 -HLK // -H1 -H2 -H3 /3 width=5/
+qed.
+
+lemma delift_tps_conf_le_up: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶ U2 →
+                             ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
+                             ∀K. ⇩[dd, ee] L ≡ K →
+                             d ≤ dd → dd ≤ d + e → d + e ≤ dd + ee →
+                             ∃∃T2. K ⊢ T1 [d, dd - d] ▶* T2 &
+                                   L ⊢ U2 [dd, ee] ≡ T2.
+/3 width=6/ qed.
+
 lemma delift_tpss_conf_be: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶* U2 →
                            ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
                            ∀K. ⇩[dd, ee] L ≡ K → d ≤ dd → dd + ee ≤ d + e →
@@ -26,7 +60,7 @@ lemma delift_tpss_conf_be: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶* U2 →
                                  L ⊢ U2 [dd, ee] ≡ T2.
 #L #U1 #U2 #d #e #HU12 #T1 #dd #ee * #X1 #HUX1 #HTX1 #K #HLK #H1 #H2
 elim (tpss_conf_eq … HU12 … HUX1) -U1 #U1 #HU21 #HXU1
-elim (tpss_inv_lift1_be … HXU1 … HLK … HTX1 ? ?) -X1 -HLK // /3 width=5/
+elim (tpss_inv_lift1_be … HXU1 … HLK … HTX1 ? ?) -X1 -HLK // -H1 -H2 /3 width=5/
 qed.
 
 lemma delift_tps_conf_be: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶ U2 →
diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/gr2.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/gr2.ma
index b8dab57ae..1168e52df 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/gr2.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/gr2.ma
@@ -19,9 +19,9 @@ include "basic_2/grammar/term_vector.ma".
 inductive at: list2 nat nat → relation nat ≝
 | at_nil: ∀i. at ⟠ i i
 | at_lt : ∀des,d,e,i1,i2. i1 < d →
-          at des i1 i2 → at ({d, e} :: des) i1 i2
+          at des i1 i2 → at ({d, e} @ des) i1 i2
 | at_ge : ∀des,d,e,i1,i2. d ≤ i1 →
-          at des (i1 + e) i2 → at ({d, e} :: des) i1 i2
+          at des (i1 + e) i2 → at ({d, e} @ des) i1 i2
 .
 
 interpretation "application (generic relocation with pairs)"
@@ -41,7 +41,7 @@ lemma at_inv_nil: ∀i1,i2. @[i1] ⟠ ≡ i2 → i1 = i2.
 /2 width=3/ qed-.
 
 fact at_inv_cons_aux: ∀des,i1,i2. @[i1] des ≡ i2 →
-                      ∀d,e,des0. des = {d, e} :: des0 →
+                      ∀d,e,des0. des = {d, e} @ des0 →
                       i1 < d ∧ @[i1] des0 ≡ i2 ∨
                       d ≤ i1 ∧ @[i1 + e] des0 ≡ i2.
 #des #i1 #i2 * -des -i1 -i2
@@ -51,12 +51,12 @@ fact at_inv_cons_aux: ∀des,i1,i2. @[i1] des ≡ i2 →
 ]
 qed.
 
-lemma at_inv_cons: ∀des,d,e,i1,i2. @[i1] {d, e} :: des ≡ i2 →
+lemma at_inv_cons: ∀des,d,e,i1,i2. @[i1] {d, e} @ des ≡ i2 →
                    i1 < d ∧ @[i1] des ≡ i2 ∨
                    d ≤ i1 ∧ @[i1 + e] des ≡ i2.
 /2 width=3/ qed-.
 
-lemma at_inv_cons_lt: ∀des,d,e,i1,i2. @[i1] {d, e} :: des ≡ i2 →
+lemma at_inv_cons_lt: ∀des,d,e,i1,i2. @[i1] {d, e} @ des ≡ i2 →
                       i1 < d → @[i1] des ≡ i2.
 #des #d #e #i1 #e2 #H
 elim (at_inv_cons … H) -H * // #Hdi1 #_ #Hi1d
@@ -64,7 +64,7 @@ lapply (le_to_lt_to_lt … Hdi1 Hi1d) -Hdi1 -Hi1d #Hd
 elim (lt_refl_false … Hd)
 qed-.
 
-lemma at_inv_cons_ge: ∀des,d,e,i1,i2. @[i1] {d, e} :: des ≡ i2 →
+lemma at_inv_cons_ge: ∀des,d,e,i1,i2. @[i1] {d, e} @ des ≡ i2 →
                       d ≤ i1 → @[i1 + e] des ≡ i2.
 #des #d #e #i1 #e2 #H
 elim (at_inv_cons … H) -H * // #Hi1d #_ #Hdi1
diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/gr2_minus.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/gr2_minus.ma
index 5287e0f66..6138548cd 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/gr2_minus.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/gr2_minus.ma
@@ -19,9 +19,9 @@ include "basic_2/unfold/gr2.ma".
 inductive minuss: nat → relation (list2 nat nat) ≝
 | minuss_nil: ∀i. minuss i ⟠ ⟠ 
 | minuss_lt : ∀des1,des2,d,e,i. i < d → minuss i des1 des2 →
-              minuss i ({d, e} :: des1) ({d - i, e} :: des2)
+              minuss i ({d, e} @ des1) ({d - i, e} @ des2)
 | minuss_ge : ∀des1,des2,d,e,i. d ≤ i → minuss (e + i) des1 des2 →
-              minuss i ({d, e} :: des1) des2
+              minuss i ({d, e} @ des1) des2
 .
 
 interpretation "minus (generic relocation with pairs)"
@@ -41,10 +41,10 @@ lemma minuss_inv_nil1: ∀des2,i. ⟠ ▭ i ≡ des2 → des2 = ⟠.
 /2 width=4/ qed-.
 
 fact minuss_inv_cons1_aux: ∀des1,des2,i. des1 ▭ i ≡ des2 →
-                           ∀d,e,des. des1 = {d, e} :: des →
+                           ∀d,e,des. des1 = {d, e} @ des →
                            d ≤ i ∧ des ▭ e + i ≡ des2 ∨
                            ∃∃des0. i < d & des ▭ i ≡ des0 &
-                                   des2 = {d - i, e} :: des0.
+                                   des2 = {d - i, e} @ des0.
 #des1 #des2 #i * -des1 -des2 -i
 [ #i #d #e #des #H destruct 
 | #des1 #des #d1 #e1 #i1 #Hid1 #Hdes #d2 #e2 #des2 #H destruct /3 width=3/
@@ -52,13 +52,13 @@ fact minuss_inv_cons1_aux: ∀des1,des2,i. des1 ▭ i ≡ des2 →
 ]
 qed.
 
-lemma minuss_inv_cons1: ∀des1,des2,d,e,i. {d, e} :: des1 ▭ i ≡ des2 →
+lemma minuss_inv_cons1: ∀des1,des2,d,e,i. {d, e} @ des1 ▭ i ≡ des2 →
                         d ≤ i ∧ des1 ▭ e + i ≡ des2 ∨
                         ∃∃des. i < d & des1 ▭ i ≡ des &
-                               des2 = {d - i, e} :: des.
+                               des2 = {d - i, e} @ des.
 /2 width=3/ qed-.
 
-lemma minuss_inv_cons1_ge: ∀des1,des2,d,e,i. {d, e} :: des1 ▭ i ≡ des2 →
+lemma minuss_inv_cons1_ge: ∀des1,des2,d,e,i. {d, e} @ des1 ▭ i ≡ des2 →
                            d ≤ i → des1 ▭ e + i ≡ des2.
 #des1 #des2 #d #e #i #H
 elim (minuss_inv_cons1 … H) -H * // #des #Hid #_ #_ #Hdi
@@ -66,9 +66,9 @@ lapply (lt_to_le_to_lt … Hid Hdi) -Hid -Hdi #Hi
 elim (lt_refl_false … Hi)
 qed-.
 
-lemma minuss_inv_cons1_lt: ∀des1,des2,d,e,i. {d, e} :: des1 ▭ i ≡ des2 →
+lemma minuss_inv_cons1_lt: ∀des1,des2,d,e,i. {d, e} @ des1 ▭ i ≡ des2 →
                            i < d → 
-                           ∃∃des. des1 ▭ i ≡ des & des2 = {d - i, e} :: des.
+                           ∃∃des. des1 ▭ i ≡ des & des2 = {d - i, e} @ des.
 #des1 #des2 #d #e #i #H
 elim (minuss_inv_cons1 … H) -H * /2 width=3/ #Hdi #_ #Hid
 lapply (lt_to_le_to_lt … Hid Hdi) -Hid -Hdi #Hi
diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/gr2_plus.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/gr2_plus.ma
index 6d66f0dab..bd8d1a9be 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/gr2_plus.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/gr2_plus.ma
@@ -18,7 +18,7 @@ include "basic_2/unfold/gr2.ma".
 
 let rec pluss (des:list2 nat nat) (i:nat) on des ≝ match des with
 [ nil2          ⇒ ⟠
-| cons2 d e des ⇒ {d + i, e} :: pluss des i
+| cons2 d e des ⇒ {d + i, e} @ pluss des i
 ].
 
 interpretation "plus (generic relocation with pairs)"
@@ -31,8 +31,8 @@ lemma pluss_inv_nil2: ∀i,des. des + i = ⟠ → des = ⟠.
 #d #e #des #H destruct
 qed.
 
-lemma pluss_inv_cons2: ∀i,d,e,des2,des. des + i = {d, e} :: des2 →
-                       ∃∃des1. des1 + i = des2 & des = {d - i, e} :: des1.
+lemma pluss_inv_cons2: ∀i,d,e,des2,des. des + i = {d, e} @ des2 →
+                       ∃∃des1. des1 + i = des2 & des = {d - i, e} @ des1.
 #i #d #e #des2 * normalize
 [ #H destruct
 | #d1 #e1 #des1 #H destruct /2 width=3/ 
diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ldrops.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ldrops.ma
index 70c09b1f5..b899bd273 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ldrops.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ldrops.ma
@@ -21,7 +21,7 @@ include "basic_2/unfold/lifts.ma".
 inductive ldrops: list2 nat nat → relation lenv ≝
 | ldrops_nil : ∀L. ldrops ⟠ L L
 | ldrops_cons: ∀L1,L,L2,des,d,e.
-               ldrops des L1 L → ⇩[d,e] L ≡ L2 → ldrops ({d, e} :: des) L1 L2
+               ldrops des L1 L → ⇩[d,e] L ≡ L2 → ldrops ({d, e} @ des) L1 L2
 .
 
 interpretation "generic local environment slicing"
@@ -39,7 +39,7 @@ lemma ldrops_inv_nil: ∀L1,L2. ⇩*[⟠] L1 ≡ L2 → L1 = L2.
 /2 width=3/ qed-.
 
 fact ldrops_inv_cons_aux: ∀L1,L2,des. ⇩*[des] L1 ≡ L2 →
-                          ∀d,e,tl. des = {d, e} :: tl →
+                          ∀d,e,tl. des = {d, e} @ tl →
                           ∃∃L. ⇩*[tl] L1 ≡ L & ⇩[d, e] L ≡ L2.
 #L1 #L2 #des * -L1 -L2 -des
 [ #L #d #e #tl #H destruct
@@ -48,7 +48,7 @@ fact ldrops_inv_cons_aux: ∀L1,L2,des. ⇩*[des] L1 ≡ L2 →
 qed.
 
 (* Basic_1: was: drop1_gen_pcons *)
-lemma ldrops_inv_cons: ∀L1,L2,d,e,des. ⇩*[{d, e} :: des] L1 ≡ L2 →
+lemma ldrops_inv_cons: ∀L1,L2,d,e,des. ⇩*[{d, e} @ des] L1 ≡ L2 →
                        ∃∃L. ⇩*[des] L1 ≡ L & ⇩[d, e] L ≡ L2.
 /2 width=3/ qed-.
 
diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ldrops_ldrops.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ldrops_ldrops.ma
index 1cb1724fd..7709561a2 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ldrops_ldrops.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ldrops_ldrops.ma
@@ -20,6 +20,6 @@ include "basic_2/unfold/ldrops_ldrop.ma".
 
 (* Basic_1: was: drop1_trans *)
 theorem ldrops_trans: ∀L,L2,des2. ⇩*[des2] L ≡ L2 → ∀L1,des1. ⇩*[des1] L1 ≡ L →
-                      ⇩*[des2 @ des1] L1 ≡ L2.
+                      ⇩*[des2 @@ des1] L1 ≡ L2.
 #L #L2 #des2 #H elim H -L -L2 -des2 // /3 width=3/
 qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts.ma
index 492ffdcbe..3f26426e3 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts.ma
@@ -20,7 +20,7 @@ include "basic_2/unfold/gr2_plus.ma".
 inductive lifts: list2 nat nat → relation term ≝
 | lifts_nil : ∀T. lifts ⟠ T T
 | lifts_cons: ∀T1,T,T2,des,d,e.
-              ⇧[d,e] T1 ≡ T → lifts des T T2 → lifts ({d, e} :: des) T1 T2
+              ⇧[d,e] T1 ≡ T → lifts des T T2 → lifts ({d, e} @ des) T1 T2
 .
 
 interpretation "generic relocation (term)"
@@ -37,7 +37,7 @@ lemma lifts_inv_nil: ∀T1,T2. ⇧*[⟠] T1 ≡ T2 → T1 = T2.
 /2 width=3/ qed-.
 
 fact lifts_inv_cons_aux: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 →
-                         ∀d,e,tl. des = {d, e} :: tl →
+                         ∀d,e,tl. des = {d, e} @ tl →
                          ∃∃T. ⇧[d, e] T1 ≡ T & ⇧*[tl] T ≡ T2.
 #T1 #T2 #des * -T1 -T2 -des
 [ #T #d #e #tl #H destruct
@@ -45,7 +45,7 @@ fact lifts_inv_cons_aux: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 →
   /2 width=3/
 qed.
 
-lemma lifts_inv_cons: ∀T1,T2,d,e,des. ⇧*[{d, e} :: des] T1 ≡ T2 →
+lemma lifts_inv_cons: ∀T1,T2,d,e,des. ⇧*[{d, e} @ des] T1 ≡ T2 →
                       ∃∃T. ⇧[d, e] T1 ≡ T & ⇧*[des] T ≡ T2.
 /2 width=3/ qed-.
 
diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_lifts.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_lifts.ma
index 0ea0a2186..72948f04b 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_lifts.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_lifts.ma
@@ -20,6 +20,6 @@ include "basic_2/unfold/lifts_lift.ma".
 
 (* Basic_1: was: lift1_lift1 (left to right) *)
 theorem lifts_trans: ∀T1,T,des1. ⇧*[des1] T1 ≡ T → ∀T2:term. ∀des2. ⇧*[des2] T ≡ T2 →
-                     ⇧*[des1 @ des2] T1 ≡ T2.
+                     ⇧*[des1 @@ des2] T1 ≡ T2.
 #T1 #T #des1 #H elim H -T1 -T -des1 // /3 width=3/
 qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_vector.ma
index 1690c9f66..9ea173a56 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_vector.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_vector.ma
@@ -21,7 +21,7 @@ inductive liftsv (des:list2 nat nat) : relation (list term) ≝
 | liftsv_nil : liftsv des ◊ ◊
 | liftsv_cons: ∀T1s,T2s,T1,T2.
                ⇧*[des] T1 ≡ T2 → liftsv des T1s T2s →
-               liftsv des (T1 :: T1s) (T2 :: T2s)
+               liftsv des (T1 @ T1s) (T2 @ T2s)
 .
 
 interpretation "generic relocation (vector)"
diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/thin.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/thin.ma
index 39d4d12c4..d3eb56c8e 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/thin.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/thin.ma
@@ -14,12 +14,12 @@
 
 include "basic_2/unfold/ltpss.ma".
 
-(* LOCAL ENVIRONMENT THINNING ***********************************************)
+(* BASIC LOCAL ENVIRONMENT THINNING *****************************************)
 
 definition thin: nat → nat → relation lenv ≝
                  λd,e,L1,L2. ∃∃L. L1 [d, e] ▶* L & ⇩[d, e] L ≡ L2.
 
-interpretation "thinning (local environment)"
+interpretation "basic thinning (local environment)"
    'TSubst L1 d e L2 = (thin d e L1 L2).
 
 (* Basic properties *********************************************************)
diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/thin_delift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/thin_delift.ma
index a28bf53e8..0653266ee 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/thin_delift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/thin_delift.ma
@@ -16,9 +16,21 @@ include "basic_2/unfold/delift_tpss.ma".
 include "basic_2/unfold/delift_ltpss.ma".
 include "basic_2/unfold/thin.ma".
 
-(* DELIFT ON LOCAL ENVIRONMENTS *********************************************)
+(* BASIC DELIFT ON LOCAL ENVIRONMENTS ***************************************)
 
-(* Properties on inverse term relocation ************************************)
+(* Inversion lemmas on inverse basic term relocation ************************)
+
+lemma thin_inv_delift1: ∀I,K1,V1,L2,d,e. K1. ⓑ{I} V1 [d, e] ≡ L2 → 0 < d →
+                        ∃∃K2,V2. K1 [d - 1, e] ≡ K2 &
+                                 K1 ⊢ V1 [d - 1, e] ≡ V2 &
+                                 L2 = K2. ⓑ{I} V2.
+#I #K1 #V1 #L2 #d #e * #X #HK1 #HL2 #e
+elim (ltpss_inv_tpss11 … HK1 ?) -HK1 // #K #V #HK1 #HV1 #H destruct
+elim (ldrop_inv_skip1 … HL2 ?) -HL2 // #K2 #V2 #HK2 #HV2 #H destruct
+lapply (ltpss_tpss_trans_eq … HV1 … HK1) -HV1 /3 width=5/
+qed-.
+
+(* Properties on inverse basic term relocation ******************************)
 
 lemma thin_delift1: ∀L1,L2,d,e. L1 [d, e] ≡ L2 → ∀V1,V2. L1 ⊢ V1 [d, e] ≡ V2 →
                     ∀I. L1.ⓑ{I}V1 [d + 1, e] ≡ L2.ⓑ{I}V2.
@@ -29,6 +41,48 @@ lapply (tpss_inv_refl_O2 … H1) -H1 #H destruct
 lapply (lift_mono … H2 … HV2) -H2 #H destruct /3 width=5/
 qed.
 
+lemma thin_delift_tpss_conf_le: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶* U2 →
+                                ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
+                                ∀K. L [dd, ee] ≡ K → d + e ≤ dd →
+                                ∃∃T2. K ⊢ T1 [d, e] ▶* T2 &
+                                      L ⊢ U2 [dd, ee] ≡ T2.
+#L #U1 #U2 #d #e #HU12 #T1 #dd #ee #HUT1 #K * #Y #HLY #HYK #Hdedd
+lapply (delift_ltpss_conf_eq … HUT1 … HLY) -HUT1 #HUT1
+elim (ltpss_tpss_conf … HU12 … HLY) -HU12 #U #HU1 #HU2
+elim (delift_tpss_conf_le … HU1 … HUT1 … HYK ?) -HU1 -HUT1 // -Hdedd #T #HT1 #HUT
+lapply (tpss_delift_trans_eq … HU2 … HUT) -U #HU2T
+lapply (ltpss_delift_trans_eq … HLY … HU2T) -Y /2 width=3/
+qed.
+
+lemma thin_delift_tps_conf_le: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶ U2 →
+                               ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
+                               ∀K. L [dd, ee] ≡ K → d + e ≤ dd →
+                               ∃∃T2. K ⊢ T1 [d, e] ▶* T2 &
+                                     L ⊢ U2 [dd, ee] ≡ T2.
+/3 width=3/ qed.
+
+lemma thin_delift_tpss_conf_le_up: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶* U2 →
+                                   ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
+                                   ∀K. L [dd, ee] ≡ K →
+                                   d ≤ dd → dd ≤ d + e → d + e ≤ dd + ee →
+                                   ∃∃T2. K ⊢ T1 [d, dd - d] ▶* T2 &
+                                         L ⊢ U2 [dd, ee] ≡ T2.
+#L #U1 #U2 #d #e #HU12 #T1 #dd #ee #HUT1 #K * #Y #HLY #HYK #Hdd #Hdde #Hddee
+lapply (delift_ltpss_conf_eq … HUT1 … HLY) -HUT1 #HUT1
+elim (ltpss_tpss_conf … HU12 … HLY) -HU12 #U #HU1 #HU2
+elim (delift_tpss_conf_le_up … HU1 … HUT1 … HYK ? ? ?) -HU1 -HUT1 // -Hdd -Hdde -Hddee #T #HT1 #HUT
+lapply (tpss_delift_trans_eq … HU2 … HUT) -U #HU2T
+lapply (ltpss_delift_trans_eq … HLY … HU2T) -Y /2 width=3/
+qed.
+
+lemma thin_delift_tps_conf_le_up: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶ U2 →
+                                  ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
+                                  ∀K. L [dd, ee] ≡ K →
+                                  d ≤ dd → dd ≤ d + e → d + e ≤ dd + ee →
+                                  ∃∃T2. K ⊢ T1 [d, dd - d] ▶* T2 &
+                                        L ⊢ U2 [dd, ee] ≡ T2.
+/3 width=6 by thin_delift_tpss_conf_le_up, tpss_strap/ qed. (**) (* too slow without trace *)
+
 lemma thin_delift_tpss_conf_be: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶* U2 →
                                 ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
                                 ∀K. L [dd, ee] ≡ K → d ≤ dd → dd + ee ≤ d + e →
diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/thin_ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/thin_ldrop.ma
index ef0f9f8c9..971031a5e 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/thin_ldrop.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/thin_ldrop.ma
@@ -16,7 +16,7 @@ include "basic_2/substitution/ldrop_ldrop.ma".
 include "basic_2/unfold/ltpss_ldrop.ma".
 include "basic_2/unfold/thin.ma".
 
-(* LOCAL ENVIRONMENT THINNING ***********************************************)
+(* BASIC LOCAL ENVIRONMENT THINNING *****************************************)
 
 (* Properties on local environment slicing **********************************)
 
diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_lift.ma
index b54a68e7c..b52444300 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_lift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_lift.ma
@@ -50,7 +50,7 @@ lemma tpss_inv_atom1: ∀L,T2,I,d,e. L ⊢ ⓪{I} [d, e] ▶* T2 →
     elim (tps_inv_atom1 … HT2) -HT2 [ /2 width=1/ | * /3 width=10/ ]
   | * #K #V1 #V #i #Hdi #Hide #HLK #HV1 #HVT #HI
     lapply (ldrop_fwd_ldrop2 … HLK) #H
-    elim (tps_inv_lift1_up … HT2 … H … HVT ? ? ?) normalize -HT2 -H -HVT [2,3,4: /2 width=1/ ] #V2 <minus_plus #HV2 #HVT2
+    elim (tps_inv_lift1_ge_up … HT2 … H … HVT ? ? ?) normalize -HT2 -H -HVT [2,3,4: /2 width=1/ ] #V2 <minus_plus #HV2 #HVT2
     @or_intror @(ex6_4_intro … Hdi Hide HLK … HVT2 HI) /2 width=3/ (**) (* /4 width=10/ is too slow *)
   ]
 ]
@@ -161,6 +161,18 @@ lemma tpss_inv_lift1_eq: ∀L,U1,U2,d,e.
 <(tps_inv_lift1_eq … HU2 … HTU1) -HU2 -HTU1 //
 qed.
 
+lemma tpss_inv_lift1_ge_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶* U2 →
+                            ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
+                            d ≤ dt → dt ≤ d + e → d + e ≤ dt + et →
+                            ∃∃T2. K ⊢ T1 [d, dt + et - (d + e)] ▶* T2 &
+                                 ⇧[d, e] T2 ≡ U2.
+#L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet @(tpss_ind … H) -U2
+[ /2 width=3/
+| -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
+  elim (tps_inv_lift1_ge_up … HU2 … HLK … HTU ? ? ?) -HU2 -HLK -HTU // /3 width=3/
+]
+qed.
+
 lemma tpss_inv_lift1_be_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶* U2 →
                             ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
                             dt ≤ d → dt + et ≤ d + e →
@@ -171,3 +183,14 @@ lemma tpss_inv_lift1_be_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶* U2 →
   elim (tps_inv_lift1_be_up … HU2 … HLK … HTU ? ?) -HU2 -HLK -HTU // /3 width=3/
 ]
 qed.
+
+lemma tpss_inv_lift1_le_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶* U2 →
+                            ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
+                            dt ≤ d → d ≤ dt + et → dt + et ≤ d + e →
+                            ∃∃T2. K ⊢ T1 [dt, d - dt] ▶* T2 & ⇧[d, e] T2 ≡ U2.
+#L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdtd #Hddet #Hdetde @(tpss_ind … H) -U2
+[ /2 width=3/
+| -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
+  elim (tps_inv_lift1_le_up … HU2 … HLK … HTU ? ? ?) -HU2 -HLK -HTU // /3 width=3/
+]
+qed.
diff --git a/matita/matita/contribs/lambda_delta/ground_2/list.ma b/matita/matita/contribs/lambda_delta/ground_2/list.ma
index 010c49f2b..0d15cfe4f 100644
--- a/matita/matita/contribs/lambda_delta/ground_2/list.ma
+++ b/matita/matita/contribs/lambda_delta/ground_2/list.ma
@@ -40,7 +40,7 @@ interpretation "cons (list of pairs)" 'Cons hd1 hd2 tl = (cons2 ? ? hd1 hd2 tl).
 
 let rec append2 (A1,A2:Type[0]) (l1,l2:list2 A1 A2) on l1 ≝ match l1 with
 [ nil2           ⇒ l2
-| cons2 a1 a2 tl ⇒ {a1, a2} :: append2 A1 A2 tl l2
+| cons2 a1 a2 tl ⇒ {a1, a2} @ append2 A1 A2 tl l2
 ].
 
 interpretation "append (list of pairs)"
diff --git a/matita/matita/contribs/lambda_delta/ground_2/notation.ma b/matita/matita/contribs/lambda_delta/ground_2/notation.ma
index 71fbbe0c2..574bd3c59 100644
--- a/matita/matita/contribs/lambda_delta/ground_2/notation.ma
+++ b/matita/matita/contribs/lambda_delta/ground_2/notation.ma
@@ -20,11 +20,11 @@ notation "hvbox( ◊ )"
   non associative with precedence 90
   for @{'Nil}.
 
-notation "hvbox( hd :: break tl )"
+notation "hvbox( hd @ break tl )"
   right associative with precedence 47
   for @{'Cons $hd $tl}.
 
-notation "hvbox( l1 @ break l2 )"
+notation "hvbox( l1 @@ break l2 )"
   right associative with precedence 47
   for @{'Append $l1 $l2 }.
 
@@ -32,6 +32,6 @@ notation "hvbox( ⟠ )"
   non associative with precedence 90
   for @{'Nil2}.
 
-notation "hvbox( { hd1 , break hd2 } :: break tl )"
+notation "hvbox( { hd1 , break hd2 } @ break tl )"
   non associative with precedence 47
   for @{'Cons $hd1 $hd2 $tl}.
diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma
index b937c077f..81d6c9310 100644
--- a/matita/matita/lib/arithmetics/nat.ma
+++ b/matita/matita/lib/arithmetics/nat.ma
@@ -450,6 +450,10 @@ lemma lt_or_ge: ∀m,n. m < n ∨ n ≤ m.
 #m #n elim (decidable_lt m n) /2 width=1/ /3 width=1/
 qed-.
 
+lemma le_or_ge: ∀m,n. m ≤ n ∨ n ≤ m.
+#m #n elim (decidable_le m n) /2 width=1/ /4 width=2/
+qed-.
+
 (* More general conclusion **************************************************)
 
 theorem nat_ind_plus: ∀R:predicate nat.
diff --git a/matita/matita/lib/basics/star.ma b/matita/matita/lib/basics/star.ma
index 04d2d7317..a80ccbea0 100644
--- a/matita/matita/lib/basics/star.ma
+++ b/matita/matita/lib/basics/star.ma
@@ -223,23 +223,35 @@ lemma TC_dx_to_TC: ∀A. ∀R: relation A.
 #A #R #a1 #a2 #Ha12 elim Ha12 -a1 -a2 /2 width=3/
 qed.
 
-fact TC_star_ind_dx_aux: ∀A,R. reflexive A R →
-                         ∀a2. ∀P:predicate A. P a2 →
-                         (∀a1,a. R a1 a → TC … R a a2 → P a → P a1) →
-                         ∀a1,a. TC … R a1 a → a = a2 → P a1.
-#A #R #HR #a2 #P #Ha2 #H #a1 #a #Ha1
+fact TC_ind_dx_aux: ∀A,R,a2. ∀P:predicate A.
+                    (∀a1. R a1 a2 → P a1) →
+                    (∀a1,a. R a1 a → TC … R a a2 → P a → P a1) →
+                    ∀a1,a. TC … R a1 a → a = a2 → P a1.
+#A #R #a2 #P #H1 #H2 #a1 #a #Ha1
 elim (TC_to_TC_dx ???? Ha1) -a1 -a
-[ #a #c #Hac #H destruct /3 width=4/
+[ #a #c #Hac #H destruct /2 width=1/
 | #a #b #c #Hab #Hbc #IH #H destruct /3 width=4/
 ]
 qed-.
 
+lemma TC_ind_dx: ∀A,R,a2. ∀P:predicate A.
+                 (∀a1. R a1 a2 → P a1) →
+                 (∀a1,a. R a1 a → TC … R a a2 → P a → P a1) →
+                 ∀a1. TC … R a1 a2 → P a1.
+#A #R #a2 #P #H1 #H2 #a1 #Ha12
+@(TC_ind_dx_aux … H1 H2 … Ha12) //
+qed-.
+
+lemma TC_symmetric: ∀A,R. symmetric A R → symmetric A (TC … R).
+#A #R #HR #x #y #H @(TC_ind_dx ??????? H) -x /3 width=1/ /3 width=3/
+qed.
+
 lemma TC_star_ind_dx: ∀A,R. reflexive A R →
                       ∀a2. ∀P:predicate A. P a2 →
                       (∀a1,a. R a1 a → TC … R a a2 → P a → P a1) →
                       ∀a1. TC … R a1 a2 → P a1.
 #A #R #HR #a2 #P #Ha2 #H #a1 #Ha12
-@(TC_star_ind_dx_aux … HR … Ha2 H … Ha12) //
+@(TC_ind_dx … P ? H … Ha12) /3 width=4/
 qed-.
 
 definition Conf3: ∀A,B. relation2 A B → relation A → Prop ≝ λA,B,S,R.
-- 
2.39.2