From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 10 Apr 2014 20:50:46 +0000 (+0000)
Subject: - some work on extensions:
X-Git-Tag: make_still_working~939
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=890a19d326338d96879dedce1eadc7c91a3beac2;p=helm.git

- some work on extensions:
  the alternative definition of lpx_sn and llpx_sn is useless since it is recursive
  llor seems to contain a bug in the referred components
- some work pointwise extended reduction:
  we restore the "full" version and use it for the normaliztion of extended reduction
  we still use "lazy" version for the "big-tree" theorem
---

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma
index e52104665..9e6cfcd24 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basic_2/reduction/lpx_ldrop.ma".
 include "basic_2/computation/cpxs_lift.ma".
 
 (* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************)
@@ -92,47 +93,36 @@ qed-.
 
 (* Properties on sn extended parallel reduction for local environments ******)
 
-lemma llpx_cpx_trans: ∀h,g,G. s_r_transitive … (cpx h g G) (llpx h g G 0).
+lemma lpx_cpx_trans: ∀h,g,G. s_r_transitive … (cpx h g G) (λ_.lpx h g G).
 #h #g #G #L2 #T1 #T2 #HT12 elim HT12 -G -L2 -T1 -T2
 [ /2 width=3 by/
 | /3 width=2 by cpx_cpxs, cpx_sort/
 | #I #G #L2 #K2 #V0 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV02 #L1 #HL12
-  elim (llpx_inv_lref_ge_dx … HL12 … HLK2) -L2
-  /5 width=8 by cpxs_delta, cpxs_strap2, llpx_cpx_conf/
-| #a #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #HL12
-  elim (llpx_inv_bind_O … HL12) -HL12 /4 width=1 by cpxs_bind/
-| #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #HL12
-  elim (llpx_inv_flat … HL12) -HL12 /3 width=1 by cpxs_flat/
-| #G #L2 #V2 #T1 #T #T2 #_ #HT2 #IHT1 #L1 #HL12
-  elim (llpx_inv_bind_O … HL12) /3 width=3 by cpxs_zeta/
-| #G #L2 #V2 #T1 #T2 #HT12 #IHT12 #L1 #HL12
-  elim (llpx_inv_flat … HL12) /3 width=1 by cpxs_tau/
-| #G #L2 #V1 #V2 #T2 #HV12 #IHV12 #L1 #HL12
-  elim (llpx_inv_flat … HL12) /3 width=1 by cpxs_ti/
-| #a #G #L2 #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L1 #HL12
-  elim (llpx_inv_flat … HL12) -HL12 #HV1 #HL12
-  elim (llpx_inv_bind_O … HL12) /3 width=3 by cpxs_beta/
-| #a #G #L2 #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L1 #HL12
-  elim (llpx_inv_flat … HL12) -HL12 #HV1 #HL12
-  elim (llpx_inv_bind_O … HL12) /3 width=3 by cpxs_theta/
+  elim (lpx_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H
+  elim (lpx_inv_pair2 … H) -H #K1 #V1 #HK12 #HV10 #H destruct
+  /4 width=7 by cpxs_delta, cpxs_strap2/
+|4,9: /4 width=1 by cpxs_beta, cpxs_bind, lpx_pair/
+|5,7,8: /3 width=1 by cpxs_flat, cpxs_ti, cpxs_tau/
+| /4 width=3 by cpxs_zeta, lpx_pair/
+| /4 width=3 by cpxs_theta, cpxs_strap1, lpx_pair/
 ]
 qed-.
 
 lemma cpx_bind2: ∀h,g,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡[h, g] V2 →
                  ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ➡[h, g] T2 →
                  ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡*[h, g] ⓑ{a,I}V2.T2.
-/4 width=9 by llpx_cpx_trans, cpxs_bind_dx, llpx_bind_repl_O/ qed.
+/4 width=5 by lpx_cpx_trans, cpxs_bind_dx, lpx_pair/ qed.
 
 (* Advanced properties ******************************************************)
 
-lemma cpxs_llpx_trans: ∀h,g,G. s_rs_transitive … (cpx h g G) (llpx h g G 0).
-#h #g #G @s_r_trans_LTC1 /2 width=3 by llpx_cpx_trans, llpx_cpx_conf/ (**) (* full auto fails here but works in cprs_cprs *)
+lemma lpx_cpxs_trans: ∀h,g,G. s_rs_transitive … (cpx h g G) (λ_.lpx h g G).
+#h #g #G @s_r_trans_LTC1 /2 width=3 by lpx_cpx_trans/ (**) (* full auto fails *)
 qed-.
 
 lemma cpxs_bind2_dx: ∀h,g,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡[h, g] V2 →
                      ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ➡*[h, g] T2 →
                      ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡*[h, g] ⓑ{a,I}V2.T2.
-/4 width=9 by cpxs_llpx_trans, cpxs_bind_dx, llpx_bind_repl_O/ qed.
+/4 width=5 by lpx_cpxs_trans, cpxs_bind_dx, lpx_pair/ qed.
 
 (* Properties on supclosure *************************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma
index 92b694f91..de9a897b9 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma
@@ -14,7 +14,7 @@
 
 include "basic_2/substitution/fqus_fqus.ma".
 include "basic_2/unfold/lsstas_lift.ma".
-include "basic_2/reduction/llpx_ldrop.ma".
+include "basic_2/reduction/cpx_lift.ma".
 include "basic_2/computation/cpxs.ma".
 
 (* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************)
@@ -42,9 +42,6 @@ lemma cpxs_delta: ∀h,g,I,G,L,K,V,V2,i.
 ]
 qed.
 
-lemma cpxs_llpx_conf: ∀h,g,G. s_r_confluent1 … (cpxs h g G) (llpx h g G 0).
-/3 width=5 by llpx_cpx_conf, s_r_conf1_LTC1/ qed-.
-
 (* Advanced inversion lemmas ************************************************)
 
 lemma cpxs_inv_lref1: ∀h,g,G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡*[h, g] T2 →
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_fpbs.ma
index eabda3146..53fe83271 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_fpbs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_fpbs.ma
@@ -13,6 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/computation/fpbs.ma".
+include "basic_2/computation/csx_lift.ma". (* added *)
 include "basic_2/computation/csx_llpx.ma".
 
 (* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_llpx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_llpx.ma
index b21b7bf51..c14492f21 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_llpx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_llpx.ma
@@ -12,128 +12,15 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/grammar/tstc_tstc.ma".
-include "basic_2/computation/cpxs_cpxs.ma".
+include "basic_2/computation/cpxs_llpx.ma".
 include "basic_2/computation/csx_alt.ma".
-include "basic_2/computation/csx_lift.ma".
 
 (* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************)
 
-(* Advanced properties ******************************************************)
+(* Properties on lazy sn extended reduction for local environments **********)
 
 lemma csx_llpx_conf: ∀h,g,G,L1,T. ⦃G, L1⦄ ⊢ ⬊*[h, g] T →
                      ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g, T, 0] L2 → ⦃G, L2⦄ ⊢ ⬊*[h, g] T.
 #h #g #G #L1 #T #H @(csx_ind_alt … H) -T
-/5 width=3 by csx_intro_cpxs, cpxs_llpx_trans, cpxs_llpx_conf/ (* 2 cpxs_llpx_trans *)
+/5 width=3 by csx_intro_cpxs, llpx_cpxs_trans, cpxs_llpx_conf/ (* 2 cpxs_llpx_trans *)
 qed-.
-
-lemma csx_abst: ∀h,g,a,G,L,W. ⦃G, L⦄ ⊢ ⬊*[h, g] W →
-                ∀T. ⦃G, L.ⓛW⦄ ⊢ ⬊*[h, g] T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓛ{a}W.T.
-#h #g #a #G #L #W #HW @(csx_ind … HW) -W #W #_ #IHW #T #HT @(csx_ind … HT) -T #T #HT #IHT
-@csx_intro #X #H1 #H2
-elim (cpx_inv_abst1 … H1) -H1
-#W0 #T0 #HLW0 #HLT0 #H destruct
-elim (eq_false_inv_tpair_sn … H2) -H2
-[ -IHT #H lapply (csx_cpx_trans … HLT0) // -HT
-  #HT0 lapply (csx_llpx_conf … HT0 (L.ⓛW0)) -HT0 
-  /4 width=4 by llpx_bind_repl_O/
-| -IHW -HLW0 -HT * #H destruct /3 width=1 by/
-]
-qed.
-
-lemma csx_abbr: ∀h,g,a,G,L,V. ⦃G, L⦄ ⊢ ⬊*[h, g] V →
-                ∀T. ⦃G, L.ⓓV⦄ ⊢ ⬊*[h, g] T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}V. T.
-#h #g #a #G #L #V #HV elim HV -V #V #_ #IHV #T #HT @(csx_ind_alt … HT) -T #T #HT #IHT
-@csx_intro #X #H1 #H2
-elim (cpx_inv_abbr1 … H1) -H1 *
-[ #V1 #T1 #HLV1 #HLT1 #H destruct
-  elim (eq_false_inv_tpair_sn … H2) -H2
-  [ /4 width=9 by csx_cpx_trans, csx_llpx_conf, llpx_bind_repl_O/
-  | -IHV -HLV1 * #H destruct /3 width=1 by cpx_cpxs/
-  ]
-| -IHV -IHT -H2
-  /3 width=8 by csx_cpx_trans, csx_inv_lift, ldrop_drop/
-]
-qed.
-
-fact csx_appl_beta_aux: ∀h,g,a,G,L,U1. ⦃G, L⦄ ⊢ ⬊*[h, g] U1 →
-                        ∀V,W,T1. U1 = ⓓ{a}ⓝW.V.T1 → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.ⓛ{a}W.T1.
-#h #g #a #G #L #X #H @(csx_ind … H) -X
-#X #HT1 #IHT1 #V #W #T1 #H1 destruct
-@csx_intro #X #H1 #H2
-elim (cpx_inv_appl1 … H1) -H1 *
-[ -HT1 #V0 #Y #HLV0 #H #H0 destruct
-  elim (cpx_inv_abst1 … H) -H #W0 #T0 #HLW0 #HLT0 #H destruct
-  @IHT1 -IHT1 [4: // | skip |3: #H destruct /2 width=1 by/ ] -H2
-  lapply (lsubr_cpx_trans … HLT0 (L.ⓓⓝW.V) ?) -HLT0 /3 width=1 by cpx_bind, cpx_flat, lsubr_abst/
-| -IHT1 -H2 #b #V0 #W0 #W2 #T0 #T2 #HLV0 #HLW02 #HLT02 #H1 #H3 destruct
-  lapply (lsubr_cpx_trans … HLT02 (L.ⓓⓝW0.V) ?) -HLT02
-  /4 width=5 by csx_cpx_trans, cpx_bind, cpx_flat, lsubr_abst/
-| -HT1 -IHT1 -H2 #b #V0 #V1 #W0 #W1 #T0 #T3 #_ #_ #_ #_ #H destruct
-]
-qed-.
-
-(* Basic_1: was just: sn3_beta *)
-lemma csx_appl_beta: ∀h,g,a,G,L,V,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}ⓝW.V.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.ⓛ{a}W.T.
-/2 width=3 by csx_appl_beta_aux/ qed.
-
-fact csx_appl_theta_aux: ∀h,g,a,G,L,U. ⦃G, L⦄ ⊢ ⬊*[h, g] U → ∀V1,V2. ⇧[0, 1] V1 ≡ V2 →
-                         ∀V,T. U = ⓓ{a}V.ⓐV2.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV1.ⓓ{a}V.T.
-#h #g #a #G #L #X #H @(csx_ind_alt … H) -X #X #HVT #IHVT #V1 #V2 #HV12 #V #T #H destruct
-lapply (csx_fwd_pair_sn … HVT) #HV
-lapply (csx_fwd_bind_dx … HVT) -HVT #HVT
-@csx_intro #X #HL #H
-elim (cpx_inv_appl1 … HL) -HL *
-[ -HV #V0 #Y #HLV10 #HL #H0 destruct
-  elim (cpx_inv_abbr1 … HL) -HL *
-  [ #V3 #T3 #HV3 #HLT3 #H0 destruct
-    elim (lift_total V0 0 1) #V4 #HV04
-    elim (eq_term_dec (ⓓ{a}V.ⓐV2.T) (ⓓ{a}V3.ⓐV4.T3))
-    [ -IHVT #H0 destruct
-      elim (eq_false_inv_tpair_sn … H) -H
-      [ -HLV10 -HV3 -HLT3 -HVT
-        >(lift_inj … HV12 … HV04) -V4
-        #H elim H //
-      | * #_ #H elim H //
-      ]
-    | -H -HVT #H
-      lapply (cpx_lift … HLV10 (L.ⓓV) (Ⓣ) … HV12 … HV04) -HLV10 -HV12 /2 width=1 by ldrop_drop/ #HV24
-      @(IHVT … H … HV04) -IHVT /4 width=1 by cpx_cpxs, cpx_bind, cpx_flat/
-    ]
-  | -H -IHVT #T0 #HLT0 #HT0 #H0 destruct
-    lapply (csx_cpx_trans … HVT (ⓐV2.T0) ?) /2 width=1 by cpx_flat/ -T #HVT0
-    lapply (csx_inv_lift … L … (Ⓣ) … 1 HVT0 ? ? ?) -HVT0
-    /3 width=5 by csx_cpx_trans, cpx_pair_sn, ldrop_drop, lift_flat/
-  ]
-| -HV -HV12 -HVT -IHVT -H #b #V0 #W0 #W1 #T0 #T1 #_ #_ #_ #H destruct
-| -IHVT -H #b #V0 #V3 #W0 #W1 #T0 #T1 #HLV10 #HV03 #HLW01 #HLT01 #H1 #H2 destruct
-  lapply (cpx_lift … HLV10 (L. ⓓW0) … HV12 … HV03) -HLV10 -HV12 -HV03 /2 width=2 by ldrop_drop/ #HLV23
-  @csx_abbr /2 width=3 by csx_cpx_trans/ -HV
-  @(csx_llpx_conf … (L.ⓓW0)) /2 width=4 by llpx_bind_repl_O/ -W1
-  /4 width=5 by csx_cpxs_trans, cpx_cpxs, cpx_flat/
-]
-qed-.
-
-lemma csx_appl_theta: ∀h,g,a,V1,V2. ⇧[0, 1] V1 ≡ V2 →
-                      ∀G,L,V,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}V.ⓐV2.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV1.ⓓ{a}V.T.
-/2 width=5 by csx_appl_theta_aux/ qed.
-
-(* Basic_1: was just: sn3_appl_appl *)
-lemma csx_appl_simple_tstc: ∀h,g,G,L,V. ⦃G, L⦄ ⊢ ⬊*[h, g] V → ∀T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 →
-                            (∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → (T1 ≃ T2 → ⊥) → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.T2) →
-                            𝐒⦃T1⦄ → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.T1.
-#h #g #G #L #V #H @(csx_ind … H) -V #V #_ #IHV #T1 #H @(csx_ind … H) -T1 #T1 #H1T1 #IHT1 #H2T1 #H3T1
-@csx_intro #X #HL #H
-elim (cpx_inv_appl1_simple … HL) -HL //
-#V0 #T0 #HLV0 #HLT10 #H0 destruct
-elim (eq_false_inv_tpair_sn … H) -H
-[ -IHT1 #HV0
-  @(csx_cpx_trans … (ⓐV0.T1)) /2 width=1 by cpx_flat/ -HLT10
-  @IHV -IHV /4 width=3 by csx_cpx_trans, cpx_pair_sn/
-| -IHV -H1T1 -HLV0 * #H #H1T10 destruct
-  elim (tstc_dec T1 T0) #H2T10
-  [ @IHT1 -IHT1 /4 width=3 by cpxs_strap2, cpxs_strap1, tstc_canc_sn, simple_tstc_repl_dx/
-  | -IHT1 -H3T1 -H1T10 /3 width=1 by cpx_cpxs/
-  ]
-]
-qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma
new file mode 100644
index 000000000..f8bf3c475
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma
@@ -0,0 +1,138 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/grammar/tstc_tstc.ma".
+include "basic_2/computation/cpxs_cpxs.ma".
+include "basic_2/computation/csx_alt.ma".
+include "basic_2/computation/csx_lift.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************)
+
+(* Advanced properties ******************************************************)
+
+lemma csx_lpx_conf: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 →
+                    ∀T. ⦃G, L1⦄ ⊢ ⬊*[h, g] T → ⦃G, L2⦄ ⊢ ⬊*[h, g] T.
+#h #g #G #L1 #L2 #HL12 #T #H @(csx_ind_alt … H) -T
+/4 width=3 by csx_intro, lpx_cpx_trans/
+qed-.
+
+lemma csx_abst: ∀h,g,a,G,L,W. ⦃G, L⦄ ⊢ ⬊*[h, g] W →
+                ∀T. ⦃G, L.ⓛW⦄ ⊢ ⬊*[h, g] T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓛ{a}W.T.
+#h #g #a #G #L #W #HW @(csx_ind … HW) -W #W #_ #IHW #T #HT @(csx_ind … HT) -T #T #HT #IHT
+@csx_intro #X #H1 #H2
+elim (cpx_inv_abst1 … H1) -H1
+#W0 #T0 #HLW0 #HLT0 #H destruct
+elim (eq_false_inv_tpair_sn … H2) -H2
+[ -IHT #H lapply (csx_cpx_trans … HLT0) // -HT
+  #HT0 lapply (csx_lpx_conf … (L.ⓛW0) … HT0) -HT0 /3 width=1 by lpx_pair/
+| -IHW -HLW0 -HT * #H destruct /3 width=1 by/
+]
+qed.
+
+lemma csx_abbr: ∀h,g,a,G,L,V. ⦃G, L⦄ ⊢ ⬊*[h, g] V →
+                ∀T. ⦃G, L.ⓓV⦄ ⊢ ⬊*[h, g] T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}V. T.
+#h #g #a #G #L #V #HV elim HV -V #V #_ #IHV #T #HT @(csx_ind_alt … HT) -T #T #HT #IHT
+@csx_intro #X #H1 #H2
+elim (cpx_inv_abbr1 … H1) -H1 *
+[ #V1 #T1 #HLV1 #HLT1 #H destruct
+  elim (eq_false_inv_tpair_sn … H2) -H2
+  [ /4 width=5 by csx_cpx_trans, csx_lpx_conf, lpx_pair/
+  | -IHV -HLV1 * #H destruct /3 width=1 by cpx_cpxs/
+  ]
+| -IHV -IHT -H2
+  /3 width=8 by csx_cpx_trans, csx_inv_lift, ldrop_drop/
+]
+qed.
+
+fact csx_appl_beta_aux: ∀h,g,a,G,L,U1. ⦃G, L⦄ ⊢ ⬊*[h, g] U1 →
+                        ∀V,W,T1. U1 = ⓓ{a}ⓝW.V.T1 → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.ⓛ{a}W.T1.
+#h #g #a #G #L #X #H @(csx_ind … H) -X
+#X #HT1 #IHT1 #V #W #T1 #H1 destruct
+@csx_intro #X #H1 #H2
+elim (cpx_inv_appl1 … H1) -H1 *
+[ -HT1 #V0 #Y #HLV0 #H #H0 destruct
+  elim (cpx_inv_abst1 … H) -H #W0 #T0 #HLW0 #HLT0 #H destruct
+  @IHT1 -IHT1 [4: // | skip |3: #H destruct /2 width=1 by/ ] -H2
+  lapply (lsubr_cpx_trans … HLT0 (L.ⓓⓝW.V) ?) -HLT0 /3 width=1 by cpx_bind, cpx_flat, lsubr_abst/
+| -IHT1 -H2 #b #V0 #W0 #W2 #T0 #T2 #HLV0 #HLW02 #HLT02 #H1 #H3 destruct
+  lapply (lsubr_cpx_trans … HLT02 (L.ⓓⓝW0.V) ?) -HLT02
+  /4 width=5 by csx_cpx_trans, cpx_bind, cpx_flat, lsubr_abst/
+| -HT1 -IHT1 -H2 #b #V0 #V1 #W0 #W1 #T0 #T3 #_ #_ #_ #_ #H destruct
+]
+qed-.
+
+(* Basic_1: was just: sn3_beta *)
+lemma csx_appl_beta: ∀h,g,a,G,L,V,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}ⓝW.V.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.ⓛ{a}W.T.
+/2 width=3 by csx_appl_beta_aux/ qed.
+
+fact csx_appl_theta_aux: ∀h,g,a,G,L,U. ⦃G, L⦄ ⊢ ⬊*[h, g] U → ∀V1,V2. ⇧[0, 1] V1 ≡ V2 →
+                         ∀V,T. U = ⓓ{a}V.ⓐV2.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV1.ⓓ{a}V.T.
+#h #g #a #G #L #X #H @(csx_ind_alt … H) -X #X #HVT #IHVT #V1 #V2 #HV12 #V #T #H destruct
+lapply (csx_fwd_pair_sn … HVT) #HV
+lapply (csx_fwd_bind_dx … HVT) -HVT #HVT
+@csx_intro #X #HL #H
+elim (cpx_inv_appl1 … HL) -HL *
+[ -HV #V0 #Y #HLV10 #HL #H0 destruct
+  elim (cpx_inv_abbr1 … HL) -HL *
+  [ #V3 #T3 #HV3 #HLT3 #H0 destruct
+    elim (lift_total V0 0 1) #V4 #HV04
+    elim (eq_term_dec (ⓓ{a}V.ⓐV2.T) (ⓓ{a}V3.ⓐV4.T3))
+    [ -IHVT #H0 destruct
+      elim (eq_false_inv_tpair_sn … H) -H
+      [ -HLV10 -HV3 -HLT3 -HVT
+        >(lift_inj … HV12 … HV04) -V4
+        #H elim H //
+      | * #_ #H elim H //
+      ]
+    | -H -HVT #H
+      lapply (cpx_lift … HLV10 (L.ⓓV) (Ⓣ) … HV12 … HV04) -HLV10 -HV12 /2 width=1 by ldrop_drop/ #HV24
+      @(IHVT … H … HV04) -IHVT /4 width=1 by cpx_cpxs, cpx_bind, cpx_flat/
+    ]
+  | -H -IHVT #T0 #HLT0 #HT0 #H0 destruct
+    lapply (csx_cpx_trans … HVT (ⓐV2.T0) ?) /2 width=1 by cpx_flat/ -T #HVT0
+    lapply (csx_inv_lift … L … (Ⓣ) … 1 HVT0 ? ? ?) -HVT0
+    /3 width=5 by csx_cpx_trans, cpx_pair_sn, ldrop_drop, lift_flat/
+  ]
+| -HV -HV12 -HVT -IHVT -H #b #V0 #W0 #W1 #T0 #T1 #_ #_ #_ #H destruct
+| -IHVT -H #b #V0 #V3 #W0 #W1 #T0 #T1 #HLV10 #HV03 #HLW01 #HLT01 #H1 #H2 destruct
+  lapply (cpx_lift … HLV10 (L. ⓓW0) … HV12 … HV03) -HLV10 -HV12 -HV03 /2 width=2 by ldrop_drop/ #HLV23
+  @csx_abbr /2 width=3 by csx_cpx_trans/ -HV
+  @(csx_lpx_conf … (L.ⓓW0)) /2 width=1 by lpx_pair/ -W1
+  /4 width=5 by csx_cpxs_trans, cpx_cpxs, cpx_flat/
+]
+qed-.
+
+lemma csx_appl_theta: ∀h,g,a,V1,V2. ⇧[0, 1] V1 ≡ V2 →
+                      ∀G,L,V,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}V.ⓐV2.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV1.ⓓ{a}V.T.
+/2 width=5 by csx_appl_theta_aux/ qed.
+
+(* Basic_1: was just: sn3_appl_appl *)
+lemma csx_appl_simple_tstc: ∀h,g,G,L,V. ⦃G, L⦄ ⊢ ⬊*[h, g] V → ∀T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 →
+                            (∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → (T1 ≃ T2 → ⊥) → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.T2) →
+                            𝐒⦃T1⦄ → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.T1.
+#h #g #G #L #V #H @(csx_ind … H) -V #V #_ #IHV #T1 #H @(csx_ind … H) -T1 #T1 #H1T1 #IHT1 #H2T1 #H3T1
+@csx_intro #X #HL #H
+elim (cpx_inv_appl1_simple … HL) -HL //
+#V0 #T0 #HLV0 #HLT10 #H0 destruct
+elim (eq_false_inv_tpair_sn … H) -H
+[ -IHT1 #HV0
+  @(csx_cpx_trans … (ⓐV0.T1)) /2 width=1 by cpx_flat/ -HLT10
+  @IHV -IHV /4 width=3 by csx_cpx_trans, cpx_pair_sn/
+| -IHV -H1T1 -HLV0 * #H #H1T10 destruct
+  elim (tstc_dec T1 T0) #H2T10
+  [ @IHT1 -IHT1 /4 width=3 by cpxs_strap2, cpxs_strap1, tstc_canc_sn, simple_tstc_repl_dx/
+  | -IHT1 -H3T1 -H1T10 /3 width=1 by cpx_cpxs/
+  ]
+]
+qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpxs.ma
new file mode 100644
index 000000000..d49b6e7ae
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpxs.ma
@@ -0,0 +1,25 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/computation/csx_lpx.ma".
+include "basic_2/computation/lpxs.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************)
+
+(* Properties on sn extended parallel computation for local environments ****)
+
+lemma csx_lpxs_conf: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 →
+                     ∀T. ⦃G, L1⦄ ⊢ ⬊*[h, g] T → ⦃G, L2⦄ ⊢ ⬊*[h, g] T.
+#h #g #G #L1 #L2 #H @(lpxs_ind … H) -L2 /3 by lpxs_strap1, csx_lpx_conf/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma
index a20455c9c..5e9ea06c7 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma
@@ -14,7 +14,7 @@
 
 include "basic_2/computation/acp_cr.ma".
 include "basic_2/computation/cpxs_tstc_vector.ma".
-include "basic_2/computation/csx_llpx.ma".
+include "basic_2/computation/csx_lpx.ma".
 include "basic_2/computation/csx_vector.ma".
 
 (* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERM VECTORS *************)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma
index bf05fb03c..cf39bffcc 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma
@@ -37,7 +37,7 @@ lemma fpb_fpbsa_trans: ∀h,g,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G, L
 [ elim (fquq_cpxs_trans … HT0 … HG1) -T
   /3 width=7 by fqus_strap2, ex3_2_intro/
 | /3 width=5 by cpxs_strap2, ex3_2_intro/
-| lapply (cpxs_llpx_trans … HT0 … HL1) -HT0 #HT10
+| lapply (llpx_cpxs_trans … HT0 … HL1) -HT0 #HT10
   lapply (cpxs_llpx_conf … HT10 … HL1) -HL1 #HL1
   elim (llpx_fqus_trans … HG2 … HL1) -L
   /3 width=7 by llpxs_strap2, cpxs_trans, ex3_2_intro/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lift.ma
index 8bcc50cd1..4895dccf5 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lift.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basic_2/reduction/fpb_lift.ma".
 include "basic_2/computation/cpxs_lift.ma".
 include "basic_2/computation/fpbs.ma".
 
@@ -23,8 +24,7 @@ lemma lsstas_fpbs: ∀h,g,G,L,T1,T2,l2. ⦃G, L⦄ ⊢ T1 •*[h, g, l2] T2 →
                    ∀l1. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ⦃G, L, T1⦄ ≥[h, g] ⦃G, L, T2⦄.
 /3 width=5 by cpxs_fpbs, lsstas_cpxs/ qed.
 
-(* Note: this should be moved *)
 lemma ssta_fpbs: ∀h,g,G,L,T,U,l.
                  ⦃G, L⦄ ⊢ T ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T •[h, g] U →
                  ⦃G, L, T⦄ ≥[h, g] ⦃G, L, U⦄.
-/3 width=5 by lsstas_fpbs, ssta_lsstas/ qed.
+/4 width=2 by fpb_fpbs, ssta_fpb/ qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/llpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/llpxs_cpxs.ma
index 1ac05bce3..35472d7e5 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/llpxs_cpxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/llpxs_cpxs.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/relocation/llpx_sn_tc.ma".
-include "basic_2/computation/cpxs_cpxs.ma".
+include "basic_2/computation/cpxs_llpx.ma".
 include "basic_2/computation/llpxs.ma".
 
 (* LAZY SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS **************)
@@ -27,11 +27,11 @@ lemma llpxs_pair_dx: ∀h,g,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 →
 (* Properties on context-sensitive extended parallel computation for terms **)
 
 lemma llpxs_cpx_trans: ∀h,g,G. s_r_transitive … (cpx h g G) (llpxs h g G 0).
-/3 width=5 by s_r_trans_LTC2, cpxs_llpx_trans/ qed-.
+/3 width=5 by s_r_trans_LTC2, llpx_cpxs_trans/ qed-.
 
 lemma llpxs_cpxs_trans: ∀h,g,G. s_rs_transitive … (cpx h g G) (llpxs h g G 0).
 #h #g #G @s_r_to_s_rs_trans @s_r_trans_LTC2
-/3 width=5 by cpxs_llpx_trans, s_rs_trans_TC1/ (**) (* full auto too slow *)
+/3 width=5 by llpx_cpxs_trans, s_rs_trans_TC1/ (**) (* full auto too slow *)
 qed-.
 
 (* Note: this is an instance of a general theorem *)
@@ -40,7 +40,7 @@ lemma llpxs_cpxs_conf_dx: ∀h,g,G2,L2,T2,U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] U2
 #h #g #G2 #L2 #T2 #U2 #HTU2 #L0 #H @(llpxs_ind_dx … H) -L0 //
 #L0 #L #HL0 #HL2 #IHL2 @(llpxs_strap2 … IHL2) -IHL2
 lapply (llpxs_cpxs_trans … HTU2 … HL2) -L2 #HTU2
-/3 width=3 by cpxs_llpx_trans, cpxs_llpx_conf/
+/3 width=3 by llpx_cpxs_trans, cpxs_llpx_conf/
 qed-.
 
 (* Note: this is an instance of a general theorem *)
@@ -49,7 +49,7 @@ lemma llpxs_cpx_conf_dx: ∀h,g,G2,L2,T2,U2. ⦃G2, L2⦄ ⊢ T2 ➡[h, g] U2 
 #h #g #G2 #L2 #T2 #U2 #HTU2 #L0 #H @(llpxs_ind_dx … H) -L0 //
 #L0 #L #HL0 #HL2 #IHL2 @(llpxs_strap2 … IHL2) -IHL2
 lapply (llpxs_cpx_trans … HTU2 … HL2) -L2 #HTU2
-/3 width=3 by cpxs_llpx_trans, cpxs_llpx_conf/
+/3 width=3 by llpx_cpxs_trans, cpxs_llpx_conf/
 qed-.
 
 lemma cpxs_bind2: ∀h,g,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 →
@@ -138,7 +138,7 @@ lemma llpxs_fquq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2,
 #h #g #G1 #G2 #L1 #L2 #T1 #T2 #HT12 #K1 #H @(llpxs_ind_dx … H) -K1
 [ /2 width=5 by ex3_2_intro/
 | #K1 #K #HK1 #_ * #L #T #HT1 #HT2 #HL2 -HT12
-  lapply (cpxs_llpx_trans … HT1 … HK1) -HT1 #HT1
+  lapply (llpx_cpxs_trans … HT1 … HK1) -HT1 #HT1
   lapply (cpxs_llpx_conf … HT1 … HK1) -HK1 #HK1
   elim (llpx_fquq_trans … HT2 … HK1) -K
   /3 width=7 by llpxs_strap2, cpxs_strap1, ex3_2_intro/
@@ -151,7 +151,7 @@ lemma llpxs_fqup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L
 #h #g #G1 #G2 #L1 #L2 #T1 #T2 #HT12 #K1 #H @(llpxs_ind_dx … H) -K1
 [ /2 width=5 by ex3_2_intro/
 | #K1 #K #HK1 #_ * #L #T #HT1 #HT2 #HL2 -HT12
-  lapply (cpxs_llpx_trans … HT1 … HK1) -HT1 #HT1
+  lapply (llpx_cpxs_trans … HT1 … HK1) -HT1 #HT1
   lapply (cpxs_llpx_conf … HT1 … HK1) -HK1 #HK1
   elim (llpx_fqup_trans … HT2 … HK1) -K
   /3 width=7 by llpxs_strap2, cpxs_trans, ex3_2_intro/
@@ -164,7 +164,7 @@ lemma llpxs_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L
 #h #g #G1 #G2 #L1 #L2 #T1 #T2 #HT12 #K1 #H @(llpxs_ind_dx … H) -K1
 [ /2 width=5 by ex3_2_intro/
 | #K1 #K #HK1 #_ * #L #T #HT1 #HT2 #HL2 -HT12
-  lapply (cpxs_llpx_trans … HT1 … HK1) -HT1 #HT1
+  lapply (llpx_cpxs_trans … HT1 … HK1) -HT1 #HT1
   lapply (cpxs_llpx_conf … HT1 … HK1) -HK1 #HK1
   elim (llpx_fqus_trans … HT2 … HK1) -K
   /3 width=7 by llpxs_strap2, cpxs_trans, ex3_2_intro/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/llsx_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/llsx_csx.ma
index 28a941508..33767f56c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/llsx_csx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/llsx_csx.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basic_2/computation/csx_lift.ma". (* added *)
 include "basic_2/computation/csx_llpxs.ma".
 include "basic_2/computation/llsx_ldrop.ma".
 include "basic_2/computation/llsx_llpx.ma".
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs.ma
new file mode 100644
index 000000000..ee557e438
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs.ma
@@ -0,0 +1,74 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/notation/relations/predsnstar_5.ma".
+include "basic_2/reduction/lpx.ma".
+include "basic_2/computation/lprs.ma".
+
+(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************)
+
+definition lpxs: ∀h. sd h → relation3 genv lenv lenv ≝
+                 λh,g,G. TC … (lpx h g G).
+
+interpretation "extended parallel computation (local environment, sn variant)"
+   'PRedSnStar h g G L1 L2 = (lpxs h g G L1 L2).
+
+(* Basic eliminators ********************************************************)
+
+lemma lpxs_ind: ∀h,g,G,L1. ∀R:predicate lenv. R L1 →
+                (∀L,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L → ⦃G, L⦄ ⊢ ➡[h, g] L2 → R L → R L2) →
+                ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → R L2.
+#h #g #G #L1 #R #HL1 #IHL1 #L2 #HL12
+@(TC_star_ind … HL1 IHL1 … HL12) //
+qed-.
+
+lemma lpxs_ind_dx: ∀h,g,G,L2. ∀R:predicate lenv. R L2 →
+                   (∀L1,L. ⦃G, L1⦄ ⊢ ➡[h, g] L → ⦃G, L⦄ ⊢ ➡*[h, g] L2 → R L → R L1) →
+                   ∀L1. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → R L1.
+#h #g #G #L2 #R #HL2 #IHL2 #L1 #HL12
+@(TC_star_ind_dx … HL2 IHL2 … HL12) //
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma lprs_lpxs: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2.
+/3 width=3 by lpr_lpx, monotonic_TC/ qed.
+
+lemma lpx_lpxs: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2.
+/2 width=1 by inj/ qed.
+
+lemma lpxs_refl: ∀h,g,G,L. ⦃G, L⦄ ⊢ ➡*[h, g] L.
+/2 width=1 by lprs_lpxs/ qed.
+
+lemma lpxs_strap1: ∀h,g,G,L1,L,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L → ⦃G, L⦄ ⊢ ➡[h, g] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2.
+/2 width=3 by step/ qed.
+
+lemma lpxs_strap2: ∀h,g,G,L1,L,L2. ⦃G, L1⦄ ⊢ ➡[h, g] L → ⦃G, L⦄ ⊢ ➡*[h, g] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2.
+/2 width=3 by TC_strap/ qed.
+
+lemma lpxs_pair_refl: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → ∀I,V. ⦃G, L1.ⓑ{I}V⦄ ⊢ ➡*[h, g] L2.ⓑ{I}V.
+/2 width=1 by TC_lpx_sn_pair_refl/ qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma lpxs_inv_atom1: ∀h,g,G,L2. ⦃G, ⋆⦄ ⊢ ➡*[h, g] L2 → L2 = ⋆.
+/2 width=2 by TC_lpx_sn_inv_atom1/ qed-.
+
+lemma lpxs_inv_atom2: ∀h,g,G,L1. ⦃G, L1⦄ ⊢ ➡*[h, g] ⋆ → L1 = ⋆.
+/2 width=2 by TC_lpx_sn_inv_atom2/ qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lpxs_fwd_length: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → |L1| = |L2|.
+/2 width=2 by TC_lpx_sn_fwd_length/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_aaa.ma
new file mode 100644
index 000000000..89122eb55
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_aaa.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/reduction/lpx_aaa.ma".
+include "basic_2/computation/lpxs.ma".
+
+(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************)
+
+(* Properties about atomic arity assignment on terms ************************)
+
+lemma aaa_lpxs_conf: ∀h,g,G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A →
+                     ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → ⦃G, L2⦄ ⊢ T ⁝ A.
+#h #g #G #L1 #T #A #HT #L2 #HL12
+@(TC_Conf3 … (λL,A. ⦃G, L⦄ ⊢ T ⁝ A) … HT ? HL12) /2 width=5 by aaa_lpx_conf/
+qed-.
+
+lemma aaa_lprs_conf: ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A →
+                     ∀L2. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L2⦄ ⊢ T ⁝ A.
+/3 width=5 by lprs_lpxs, aaa_lpxs_conf/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_alt.ma
new file mode 100644
index 000000000..8a6b30a57
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_alt.ma
@@ -0,0 +1,47 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/notation/relations/predsnstaralt_5.ma".
+include "basic_2/computation/cpxs_cpxs.ma".
+include "basic_2/computation/lpxs.ma".
+
+(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************)
+
+(* alternative definition *)
+definition lpxsa: ∀h. sd h → relation3 genv lenv lenv ≝
+                  λh,g,G. lpx_sn … (cpxs h g G).
+
+interpretation "extended parallel computation (local environment, sn variant) alternative"
+   'PRedSnStarAlt h g G L1 L2 = (lpxsa h g G L1 L2).
+
+(* Main properties on the alternative definition ****************************)
+
+theorem lpxsa_lpxs: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡➡*[h, g] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2.
+/2 width=1 by lpx_sn_LTC_TC_lpx_sn/ qed-.
+
+(* Main inversion lemmas on the alternative definition **********************)
+
+theorem lpxs_inv_lpxsa: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → ⦃G, L1⦄ ⊢ ➡➡*[h, g] L2.
+/3 width=3 by TC_lpx_sn_inv_lpx_sn_LTC, lpx_cpxs_trans/ qed-.
+
+(* Alternative eliminators **************************************************)
+
+lemma lpxs_ind_alt: ∀h,g,G. ∀R:relation lenv.
+                    R (⋆) (⋆) → (
+                       ∀I,K1,K2,V1,V2.
+                       ⦃G, K1⦄ ⊢ ➡*[h, g] K2 → ⦃G, K1⦄ ⊢ V1 ➡*[h, g] V2 →
+                       R K1 K2 → R (K1.ⓑ{I}V1) (K2.ⓑ{I}V2)
+                    ) →
+                    ∀L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → R L1 L2.
+/3 width=4 by TC_lpx_sn_ind, lpx_cpxs_trans/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma
new file mode 100644
index 000000000..1dfb297e7
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma
@@ -0,0 +1,150 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/computation/cpxs_cpxs.ma".
+include "basic_2/computation/lpxs.ma".
+
+(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************)
+
+(* Advanced properties ******************************************************)
+
+lemma lpxs_pair: ∀h,g,I,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 →
+                 ∀V1,V2. ⦃G, L1⦄ ⊢ V1 ➡*[h, g] V2 →
+                 ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡*[h, g] L2.ⓑ{I}V2.
+/2 width=1 by TC_lpx_sn_pair/ qed.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma lpxs_inv_pair1: ∀h,g,I,G,K1,L2,V1. ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡*[h, g] L2 →
+                      ∃∃K2,V2. ⦃G, K1⦄ ⊢ ➡*[h, g] K2 & ⦃G, K1⦄ ⊢ V1 ➡*[h, g] V2 & L2 = K2.ⓑ{I}V2.
+/3 width=3 by TC_lpx_sn_inv_pair1, lpx_cpxs_trans/ qed-.
+
+lemma lpxs_inv_pair2: ∀h,g,I,G,L1,K2,V2. ⦃G, L1⦄ ⊢ ➡*[h, g] K2.ⓑ{I}V2 →
+                      ∃∃K1,V1. ⦃G, K1⦄ ⊢ ➡*[h, g] K2 & ⦃G, K1⦄ ⊢ V1 ➡*[h, g] V2 & L1 = K1.ⓑ{I}V1.
+/3 width=3 by TC_lpx_sn_inv_pair2, lpx_cpxs_trans/ qed-.
+
+(* Properties on context-sensitive extended parallel computation for terms **)
+
+lemma lpxs_cpx_trans: ∀h,g,G. s_r_transitive … (cpx h g G) (λ_.lpxs h g G).
+/3 width=5 by s_r_trans_LTC2, lpx_cpxs_trans/ qed-.
+
+(* Note: alternative proof: /3 width=5 by s_r_trans_TC1, lpxs_cpx_trans/ *)
+lemma lpxs_cpxs_trans: ∀h,g,G. s_rs_transitive … (cpx h g G) (λ_.lpxs h g G).
+#h #g #G @s_r_to_s_rs_trans @s_r_trans_LTC2
+@s_rs_trans_TC1 /2 width=3 by lpx_cpxs_trans/ (**) (* full auto too slow *)
+qed-.
+
+lemma cpxs_bind2: ∀h,g,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 →
+                  ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ➡*[h, g] T2 →
+                  ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡*[h, g] ⓑ{a,I}V2.T2.
+/4 width=5 by lpxs_cpxs_trans, lpxs_pair, cpxs_bind/ qed.
+
+(* Inversion lemmas on context-sensitive ext parallel computation for terms *)
+
+lemma cpxs_inv_abst1: ∀h,g,a,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{a}V1.T1 ➡*[h, g] U2 →
+                      ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 & ⦃G, L.ⓛV1⦄ ⊢ T1 ➡*[h, g] T2 &
+                               U2 = ⓛ{a}V2.T2.
+#h #g #a #G #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 /2 width=5 by ex3_2_intro/
+#U0 #U2 #_ #HU02 * #V0 #T0 #HV10 #HT10 #H destruct
+elim (cpx_inv_abst1 … HU02) -HU02 #V2 #T2 #HV02 #HT02 #H destruct
+lapply (lpxs_cpx_trans … HT02 (L.ⓛV1) ?)
+/3 width=5 by lpxs_pair, cpxs_trans, cpxs_strap1, ex3_2_intro/
+qed-.
+
+lemma cpxs_inv_abbr1: ∀h,g,a,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{a}V1.T1 ➡*[h, g] U2 → (
+                      ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 & ⦃G, L.ⓓV1⦄ ⊢ T1 ➡*[h, g] T2 &
+                               U2 = ⓓ{a}V2.T2
+                      ) ∨
+                      ∃∃T2. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡*[h, g] T2 & ⇧[0, 1] U2 ≡ T2 & a = true.
+#h #g #a #G #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 /3 width=5 by ex3_2_intro, or_introl/
+#U0 #U2 #_ #HU02 * *
+[ #V0 #T0 #HV10 #HT10 #H destruct
+  elim (cpx_inv_abbr1 … HU02) -HU02 *
+  [ #V2 #T2 #HV02 #HT02 #H destruct
+    lapply (lpxs_cpx_trans … HT02 (L.ⓓV1) ?)
+    /4 width=5 by lpxs_pair, cpxs_trans, cpxs_strap1, ex3_2_intro, or_introl/
+  | #T2 #HT02 #HUT2
+    lapply (lpxs_cpx_trans … HT02 (L.ⓓV1) ?) -HT02
+    /4 width=3 by lpxs_pair, cpxs_trans, ex3_intro, or_intror/
+  ]
+| #U1 #HTU1 #HU01
+  elim (lift_total U2 0 1) #U #HU2
+  /6 width=12 by cpxs_strap1, cpx_lift, ldrop_drop, ex3_intro, or_intror/
+]
+qed-.
+
+(* More advanced properties *************************************************)
+
+lemma lpxs_pair2: ∀h,g,I,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 →
+                  ∀V1,V2. ⦃G, L2⦄ ⊢ V1 ➡*[h, g] V2 → ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡*[h, g] L2.ⓑ{I}V2.
+/3 width=3 by lpxs_pair, lpxs_cpxs_trans/ qed.
+
+(* Properties on supclosure *************************************************)
+
+lemma lpx_fqup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ →
+                      ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 →
+                      ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
+[ #G2 #L2 #T2 #H12 #K1 #HKL1 elim (lpx_fqu_trans … H12 … HKL1) -L1
+  /3 width=5 by cpx_cpxs, fqu_fqup, ex3_2_intro/
+| #G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1
+  #L0 #T0 #HT10 #HT0 #HL0 elim (lpx_fqu_trans … H2 … HL0) -L
+  #L #T3 #HT3 #HT32 #HL2 elim (fqup_cpx_trans … HT0 … HT3) -T
+  /3 width=7 by cpxs_strap1, fqup_strap1, ex3_2_intro/
+]
+qed-.
+
+lemma lpx_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
+                      ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 →
+                      ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -G2 -L2 -T2 /2 width=5 by ex3_2_intro/
+#G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1
+#L0 #T0 #HT10 #HT0 #HL0 elim (lpx_fquq_trans … H2 … HL0) -L
+#L #T3 #HT3 #HT32 #HL2 elim (fqus_cpx_trans … HT0 … HT3) -T
+/3 width=7 by cpxs_strap1, fqus_strap1, ex3_2_intro/
+qed-.
+
+lemma lpxs_fquq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
+                       ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 →
+                       ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #HT12 #K1 #H @(lpxs_ind_dx … H) -K1
+[ /2 width=5 by ex3_2_intro/
+| #K1 #K #HK1 #_ * #L #T #HT1 #HT2 #HL2 -HT12
+  lapply (lpx_cpxs_trans … HT1 … HK1) -HT1
+  elim (lpx_fquq_trans … HT2 … HK1) -K
+  /3 width=7 by lpxs_strap2, cpxs_strap1, ex3_2_intro/
+]
+qed-.
+
+lemma lpxs_fqup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ →
+                       ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 →
+                       ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #HT12 #K1 #H @(lpxs_ind_dx … H) -K1
+[ /2 width=5 by ex3_2_intro/
+| #K1 #K #HK1 #_ * #L #T #HT1 #HT2 #HL2 -HT12
+  lapply (lpx_cpxs_trans … HT1 … HK1) -HT1
+  elim (lpx_fqup_trans … HT2 … HK1) -K
+  /3 width=7 by lpxs_strap2, cpxs_trans, ex3_2_intro/
+]
+qed-.
+
+lemma lpxs_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
+                       ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 →
+                       ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -G2 -L2 -T2 /2 width=5 by ex3_2_intro/
+#G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1
+#L0 #T0 #HT10 #HT0 #HL0 elim (lpxs_fquq_trans … H2 … HL0) -L
+#L #T3 #HT3 #HT32 #HL2 elim (fqus_cpxs_trans … HT3 … HT0) -T
+/3 width=7 by cpxs_trans, fqus_strap1, ex3_2_intro/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_ldrop.ma
new file mode 100644
index 000000000..d8c489017
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_ldrop.ma
@@ -0,0 +1,29 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/reduction/lpx_ldrop.ma".
+include "basic_2/computation/lpxs.ma".
+
+(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************)
+
+(* Properies on local environment slicing ***********************************)
+
+lemma lpxs_ldrop_conf: ∀h,g,G. dropable_sn (lpxs h g G).
+/3 width=3 by dropable_sn_TC, lpx_ldrop_conf/ qed-.
+
+lemma ldrop_lpxs_trans: ∀h,g,G. dedropable_sn (lpxs h g G).
+/3 width=3 by dedropable_sn_TC, ldrop_lpx_trans/ qed-.
+
+lemma lpxs_ldrop_trans_O1: ∀h,g,G. dropable_dx (lpxs h g G).
+/3 width=3 by dropable_dx_TC, lpx_ldrop_trans_O1/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma
new file mode 100644
index 000000000..2f9b322db
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma
@@ -0,0 +1,125 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/substitution/lleq_leq.ma".
+include "basic_2/reduction/lpx_lleq.ma".
+include "basic_2/computation/cpxs_leq.ma".
+include "basic_2/computation/lpxs_ldrop.ma".
+include "basic_2/computation/lpxs_cpxs.ma".
+
+(* SN EXTENDED PARALLEL COMPUTATION FOR LOCAL ENVIRONMENTS ******************)
+
+(* Properties on lazy equivalence for local environments ********************)
+
+lemma lleq_lpxs_trans: ∀h,g,G,L2,K2. ⦃G, L2⦄ ⊢ ➡*[h, g] K2 →
+                       ∀L1,T,d. L1 ⋕[T, d] L2 →
+                       ∃∃K1. ⦃G, L1⦄ ⊢ ➡*[h, g] K1 & K1 ⋕[T, d] K2.
+#h #g #G #L2 #K2 #H @(lpxs_ind … H) -K2 /2 width=3 by ex2_intro/
+#K #K2 #_ #HK2 #IH #L1 #T #d #HT elim (IH … HT) -L2
+#L #HL1 #HT elim (lleq_lpx_trans … HK2 … HT) -K
+/3 width=3 by lpxs_strap1, ex2_intro/
+qed-.
+
+lemma lpxs_lleq_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
+                           ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ⋕[T1, 0] L1 →
+                           ∃∃K2. ⦃G1, K1, T1⦄ ⊃ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ⋕[T2, 0] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
+[ #I #G1 #L1 #V1 #X #H1 #H2 elim (lpxs_inv_pair2 … H1) -H1
+  #K0 #V0 #H1KL1 #_ #H destruct
+  elim (lleq_inv_lref_ge_dx … H2 ? I L1 V1) -H2 //
+  #K1 #H #H2KL1 lapply (ldrop_inv_O2 … H) -H #H destruct
+  /2 width=4 by fqu_lref_O, ex3_intro/
+| * [ #a ] #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H
+  [ elim (lleq_inv_bind … H)
+  | elim (lleq_inv_flat … H)
+  ] -H /2 width=4 by fqu_pair_sn, ex3_intro/
+| #a #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_bind_O … H) -H
+  /3 width=4 by lpxs_pair, fqu_bind_dx, ex3_intro/
+| #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_flat … H) -H
+  /2 width=4 by fqu_flat_dx, ex3_intro/
+| #G1 #L1 #L #T1 #U1 #e #HL1 #HTU1 #K1 #H1KL1 #H2KL1
+  elim (ldrop_O1_le (e+1) K1)
+  [ #K #HK1 lapply (lleq_inv_lift_le … H2KL1 … HK1 HL1 … HTU1 ?) -H2KL1 //
+    #H2KL elim (lpxs_ldrop_trans_O1 … H1KL1 … HL1) -L1
+    #K0 #HK10 #H1KL lapply (ldrop_mono … HK10 … HK1) -HK10 #H destruct
+    /3 width=4 by fqu_drop, ex3_intro/
+  | lapply (ldrop_fwd_length_le2 … HL1) -L -T1 -g
+    lapply (lleq_fwd_length … H2KL1) //
+  ]
+]
+qed-.
+
+lemma lpxs_lleq_fquq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
+                            ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ⋕[T1, 0] L1 →
+                            ∃∃K2. ⦃G1, K1, T1⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ⋕[T2, 0] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1
+elim (fquq_inv_gen … H) -H
+[ #H elim (lpxs_lleq_fqu_trans … H … H1KL1 H2KL1) -L1
+  /3 width=4 by fqu_fquq, ex3_intro/
+| * #HG #HL #HT destruct /2 width=4 by ex3_intro/
+]
+qed-.
+
+lemma lpxs_lleq_fqup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ →
+                            ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ⋕[T1, 0] L1 →
+                            ∃∃K2. ⦃G1, K1, T1⦄ ⊃+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ⋕[T2, 0] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
+[ #G2 #L2 #T2 #H #K1 #H1KL1 #H2KL1 elim (lpxs_lleq_fqu_trans … H … H1KL1 H2KL1) -L1
+  /3 width=4 by fqu_fqup, ex3_intro/
+| #G #G2 #L #L2 #T #T2 #_ #HT2 #IHT1 #K1 #H1KL1 #H2KL1 elim (IHT1 … H2KL1) // -L1
+  #K #HT1 #H1KL #H2KL elim (lpxs_lleq_fqu_trans … HT2 … H1KL H2KL) -L
+  /3 width=5 by fqup_strap1, ex3_intro/
+]
+qed-.
+
+lemma lpxs_lleq_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
+                            ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ⋕[T1, 0] L1 →
+                            ∃∃K2. ⦃G1, K1, T1⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ⋕[T2, 0] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1
+elim (fqus_inv_gen … H) -H
+[ #H elim (lpxs_lleq_fqup_trans … H … H1KL1 H2KL1) -L1
+  /3 width=4 by fqup_fqus, ex3_intro/
+| * #HG #HL #HT destruct /2 width=4 by ex3_intro/
+]
+qed-.
+
+fact leq_lpxs_trans_lleq_aux: ∀h,g,G,L1,L0,d,e. L1 ≃[d, e] L0 → e = ∞ →
+                              ∀L2. ⦃G, L0⦄ ⊢ ➡*[h, g] L2 →
+                              ∃∃L. L ≃[d, e] L2 & ⦃G, L1⦄ ⊢ ➡*[h, g] L &
+                                   (∀T. L0 ⋕[T, d] L2 ↔ L1 ⋕[T, d] L).
+#h #g #G #L1 #L0 #d #e #H elim H -L1 -L0 -d -e
+[ #d #e #_ #L2 #H >(lpxs_inv_atom1 … H) -H
+  /3 width=5 by ex3_intro, conj/
+| #I1 #I0 #L1 #L0 #V1 #V0 #_ #_ #He destruct
+| #I #L1 #L0 #V1 #e #HL10 #IHL10 #He #Y #H
+  elim (lpxs_inv_pair1 … H) -H #L2 #V2 #HL02 #HV02 #H destruct
+  lapply (ysucc_inv_Y_dx … He) -He #He
+  elim (IHL10 … HL02) // -IHL10 -HL02 #L #HL2 #HL1 #IH
+  @(ex3_intro … (L.ⓑ{I}V2)) /3 width=3 by lpxs_pair, leq_cpxs_trans, leq_pair/
+  #T elim (IH T) #HL0dx #HL0sn
+  @conj #H @(lleq_leq_repl … H) -H /3 width=1 by leq_sym, leq_pair_O_Y/
+| #I1 #I0 #L1 #L0 #V1 #V0 #d #e #HL10 #IHL10 #He #Y #H
+  elim (lpxs_inv_pair1 … H) -H #L2 #V2 #HL02 #HV02 #H destruct
+  elim (IHL10 … HL02) // -IHL10 -HL02 #L #HL2 #HL1 #IH
+  @(ex3_intro … (L.ⓑ{I1}V1)) /3 width=1 by lpxs_pair, leq_succ/
+  #T elim (IH T) #HL0dx #HL0sn
+  @conj #H @(lleq_leq_repl … H) -H /3 width=1 by leq_sym, leq_succ/
+]
+qed-.
+
+lemma leq_lpxs_trans_lleq: ∀h,g,G,L1,L0,d. L1 ≃[d, ∞] L0 →
+                           ∀L2. ⦃G, L0⦄ ⊢ ➡*[h, g] L2 →
+                           ∃∃L. L ≃[d, ∞] L2 & ⦃G, L1⦄ ⊢ ➡*[h, g] L &
+                                (∀T. L0 ⋕[T, d] L2 ↔ L1 ⋕[T, d] L).
+/2 width=1 by leq_lpxs_trans_lleq_aux/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lpxs.ma
new file mode 100644
index 000000000..1d287d368
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lpxs.ma
@@ -0,0 +1,22 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/computation/lpxs.ma".
+
+(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************)
+
+(* Main properties **********************************************************)
+
+theorem lpxs_trans: ∀h,g,G. Transitive … (lpxs h g G).
+/2 width=3 by trans_TC/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/csx_lpx.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/csx_lpx.etc
deleted file mode 100644
index f8bf3c475..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/csx_lpx.etc
+++ /dev/null
@@ -1,138 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/grammar/tstc_tstc.ma".
-include "basic_2/computation/cpxs_cpxs.ma".
-include "basic_2/computation/csx_alt.ma".
-include "basic_2/computation/csx_lift.ma".
-
-(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************)
-
-(* Advanced properties ******************************************************)
-
-lemma csx_lpx_conf: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 →
-                    ∀T. ⦃G, L1⦄ ⊢ ⬊*[h, g] T → ⦃G, L2⦄ ⊢ ⬊*[h, g] T.
-#h #g #G #L1 #L2 #HL12 #T #H @(csx_ind_alt … H) -T
-/4 width=3 by csx_intro, lpx_cpx_trans/
-qed-.
-
-lemma csx_abst: ∀h,g,a,G,L,W. ⦃G, L⦄ ⊢ ⬊*[h, g] W →
-                ∀T. ⦃G, L.ⓛW⦄ ⊢ ⬊*[h, g] T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓛ{a}W.T.
-#h #g #a #G #L #W #HW @(csx_ind … HW) -W #W #_ #IHW #T #HT @(csx_ind … HT) -T #T #HT #IHT
-@csx_intro #X #H1 #H2
-elim (cpx_inv_abst1 … H1) -H1
-#W0 #T0 #HLW0 #HLT0 #H destruct
-elim (eq_false_inv_tpair_sn … H2) -H2
-[ -IHT #H lapply (csx_cpx_trans … HLT0) // -HT
-  #HT0 lapply (csx_lpx_conf … (L.ⓛW0) … HT0) -HT0 /3 width=1 by lpx_pair/
-| -IHW -HLW0 -HT * #H destruct /3 width=1 by/
-]
-qed.
-
-lemma csx_abbr: ∀h,g,a,G,L,V. ⦃G, L⦄ ⊢ ⬊*[h, g] V →
-                ∀T. ⦃G, L.ⓓV⦄ ⊢ ⬊*[h, g] T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}V. T.
-#h #g #a #G #L #V #HV elim HV -V #V #_ #IHV #T #HT @(csx_ind_alt … HT) -T #T #HT #IHT
-@csx_intro #X #H1 #H2
-elim (cpx_inv_abbr1 … H1) -H1 *
-[ #V1 #T1 #HLV1 #HLT1 #H destruct
-  elim (eq_false_inv_tpair_sn … H2) -H2
-  [ /4 width=5 by csx_cpx_trans, csx_lpx_conf, lpx_pair/
-  | -IHV -HLV1 * #H destruct /3 width=1 by cpx_cpxs/
-  ]
-| -IHV -IHT -H2
-  /3 width=8 by csx_cpx_trans, csx_inv_lift, ldrop_drop/
-]
-qed.
-
-fact csx_appl_beta_aux: ∀h,g,a,G,L,U1. ⦃G, L⦄ ⊢ ⬊*[h, g] U1 →
-                        ∀V,W,T1. U1 = ⓓ{a}ⓝW.V.T1 → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.ⓛ{a}W.T1.
-#h #g #a #G #L #X #H @(csx_ind … H) -X
-#X #HT1 #IHT1 #V #W #T1 #H1 destruct
-@csx_intro #X #H1 #H2
-elim (cpx_inv_appl1 … H1) -H1 *
-[ -HT1 #V0 #Y #HLV0 #H #H0 destruct
-  elim (cpx_inv_abst1 … H) -H #W0 #T0 #HLW0 #HLT0 #H destruct
-  @IHT1 -IHT1 [4: // | skip |3: #H destruct /2 width=1 by/ ] -H2
-  lapply (lsubr_cpx_trans … HLT0 (L.ⓓⓝW.V) ?) -HLT0 /3 width=1 by cpx_bind, cpx_flat, lsubr_abst/
-| -IHT1 -H2 #b #V0 #W0 #W2 #T0 #T2 #HLV0 #HLW02 #HLT02 #H1 #H3 destruct
-  lapply (lsubr_cpx_trans … HLT02 (L.ⓓⓝW0.V) ?) -HLT02
-  /4 width=5 by csx_cpx_trans, cpx_bind, cpx_flat, lsubr_abst/
-| -HT1 -IHT1 -H2 #b #V0 #V1 #W0 #W1 #T0 #T3 #_ #_ #_ #_ #H destruct
-]
-qed-.
-
-(* Basic_1: was just: sn3_beta *)
-lemma csx_appl_beta: ∀h,g,a,G,L,V,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}ⓝW.V.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.ⓛ{a}W.T.
-/2 width=3 by csx_appl_beta_aux/ qed.
-
-fact csx_appl_theta_aux: ∀h,g,a,G,L,U. ⦃G, L⦄ ⊢ ⬊*[h, g] U → ∀V1,V2. ⇧[0, 1] V1 ≡ V2 →
-                         ∀V,T. U = ⓓ{a}V.ⓐV2.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV1.ⓓ{a}V.T.
-#h #g #a #G #L #X #H @(csx_ind_alt … H) -X #X #HVT #IHVT #V1 #V2 #HV12 #V #T #H destruct
-lapply (csx_fwd_pair_sn … HVT) #HV
-lapply (csx_fwd_bind_dx … HVT) -HVT #HVT
-@csx_intro #X #HL #H
-elim (cpx_inv_appl1 … HL) -HL *
-[ -HV #V0 #Y #HLV10 #HL #H0 destruct
-  elim (cpx_inv_abbr1 … HL) -HL *
-  [ #V3 #T3 #HV3 #HLT3 #H0 destruct
-    elim (lift_total V0 0 1) #V4 #HV04
-    elim (eq_term_dec (ⓓ{a}V.ⓐV2.T) (ⓓ{a}V3.ⓐV4.T3))
-    [ -IHVT #H0 destruct
-      elim (eq_false_inv_tpair_sn … H) -H
-      [ -HLV10 -HV3 -HLT3 -HVT
-        >(lift_inj … HV12 … HV04) -V4
-        #H elim H //
-      | * #_ #H elim H //
-      ]
-    | -H -HVT #H
-      lapply (cpx_lift … HLV10 (L.ⓓV) (Ⓣ) … HV12 … HV04) -HLV10 -HV12 /2 width=1 by ldrop_drop/ #HV24
-      @(IHVT … H … HV04) -IHVT /4 width=1 by cpx_cpxs, cpx_bind, cpx_flat/
-    ]
-  | -H -IHVT #T0 #HLT0 #HT0 #H0 destruct
-    lapply (csx_cpx_trans … HVT (ⓐV2.T0) ?) /2 width=1 by cpx_flat/ -T #HVT0
-    lapply (csx_inv_lift … L … (Ⓣ) … 1 HVT0 ? ? ?) -HVT0
-    /3 width=5 by csx_cpx_trans, cpx_pair_sn, ldrop_drop, lift_flat/
-  ]
-| -HV -HV12 -HVT -IHVT -H #b #V0 #W0 #W1 #T0 #T1 #_ #_ #_ #H destruct
-| -IHVT -H #b #V0 #V3 #W0 #W1 #T0 #T1 #HLV10 #HV03 #HLW01 #HLT01 #H1 #H2 destruct
-  lapply (cpx_lift … HLV10 (L. ⓓW0) … HV12 … HV03) -HLV10 -HV12 -HV03 /2 width=2 by ldrop_drop/ #HLV23
-  @csx_abbr /2 width=3 by csx_cpx_trans/ -HV
-  @(csx_lpx_conf … (L.ⓓW0)) /2 width=1 by lpx_pair/ -W1
-  /4 width=5 by csx_cpxs_trans, cpx_cpxs, cpx_flat/
-]
-qed-.
-
-lemma csx_appl_theta: ∀h,g,a,V1,V2. ⇧[0, 1] V1 ≡ V2 →
-                      ∀G,L,V,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}V.ⓐV2.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV1.ⓓ{a}V.T.
-/2 width=5 by csx_appl_theta_aux/ qed.
-
-(* Basic_1: was just: sn3_appl_appl *)
-lemma csx_appl_simple_tstc: ∀h,g,G,L,V. ⦃G, L⦄ ⊢ ⬊*[h, g] V → ∀T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 →
-                            (∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → (T1 ≃ T2 → ⊥) → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.T2) →
-                            𝐒⦃T1⦄ → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.T1.
-#h #g #G #L #V #H @(csx_ind … H) -V #V #_ #IHV #T1 #H @(csx_ind … H) -T1 #T1 #H1T1 #IHT1 #H2T1 #H3T1
-@csx_intro #X #HL #H
-elim (cpx_inv_appl1_simple … HL) -HL //
-#V0 #T0 #HLV0 #HLT10 #H0 destruct
-elim (eq_false_inv_tpair_sn … H) -H
-[ -IHT1 #HV0
-  @(csx_cpx_trans … (ⓐV0.T1)) /2 width=1 by cpx_flat/ -HLT10
-  @IHV -IHV /4 width=3 by csx_cpx_trans, cpx_pair_sn/
-| -IHV -H1T1 -HLV0 * #H #H1T10 destruct
-  elim (tstc_dec T1 T0) #H2T10
-  [ @IHT1 -IHT1 /4 width=3 by cpxs_strap2, cpxs_strap1, tstc_canc_sn, simple_tstc_repl_dx/
-  | -IHT1 -H3T1 -H1T10 /3 width=1 by cpx_cpxs/
-  ]
-]
-qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/csx_lpxs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/csx_lpxs.etc
deleted file mode 100644
index d49b6e7ae..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/csx_lpxs.etc
+++ /dev/null
@@ -1,25 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/computation/csx_lpx.ma".
-include "basic_2/computation/lpxs.ma".
-
-(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************)
-
-(* Properties on sn extended parallel computation for local environments ****)
-
-lemma csx_lpxs_conf: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 →
-                     ∀T. ⦃G, L1⦄ ⊢ ⬊*[h, g] T → ⦃G, L2⦄ ⊢ ⬊*[h, g] T.
-#h #g #G #L1 #L2 #H @(lpxs_ind … H) -L2 /3 by lpxs_strap1, csx_lpx_conf/
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lazycosn_5.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lazycosn_5.etc
deleted file mode 100644
index 55c37a8fd..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lazycosn_5.etc
+++ /dev/null
@@ -1,19 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( G ⊢ ⧤ ⬊ * break [ term 46 h , break term 46 g , break term 46 d ] break term 46 L )"
-   non associative with precedence 45
-   for @{ 'LazyCoSN $h $g $d $G $L }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx.etc
deleted file mode 100644
index b10b13a28..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx.etc
+++ /dev/null
@@ -1,65 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/notation/relations/predsn_5.ma".
-include "basic_2/reduction/lpr.ma".
-include "basic_2/reduction/cpx.ma".
-
-(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
-
-definition lpx: ∀h. sd h → relation3 genv lenv lenv ≝
-                λh,g,G. lpx_sn (cpx h g G).
-
-interpretation "extended parallel reduction (local environment, sn variant)"
-   'PRedSn h g G L1 L2 = (lpx h g G L1 L2).
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma lpx_inv_atom1: ∀h,g,G,L2. ⦃G, ⋆⦄ ⊢ ➡[h, g] L2 → L2 = ⋆.
-/2 width=4 by lpx_sn_inv_atom1_aux/ qed-.
-
-lemma lpx_inv_pair1: ∀h,g,I,G,K1,V1,L2. ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡[h, g] L2 →
-                     ∃∃K2,V2. ⦃G, K1⦄ ⊢ ➡[h, g] K2 & ⦃G, K1⦄ ⊢ V1 ➡[h, g] V2 &
-                              L2 = K2. ⓑ{I} V2.
-/2 width=3 by lpx_sn_inv_pair1_aux/ qed-.
-
-lemma lpx_inv_atom2: ∀h,g,G,L1.  ⦃G, L1⦄ ⊢ ➡[h, g] ⋆ → L1 = ⋆.
-/2 width=4 by lpx_sn_inv_atom2_aux/ qed-.
-
-lemma lpx_inv_pair2: ∀h,g,I,G,L1,K2,V2.  ⦃G, L1⦄ ⊢ ➡[h, g] K2.ⓑ{I}V2 →
-                     ∃∃K1,V1. ⦃G, K1⦄ ⊢ ➡[h, g] K2 & ⦃G, K1⦄ ⊢ V1 ➡[h, g] V2 &
-                             L1 = K1. ⓑ{I} V1.
-/2 width=3 by lpx_sn_inv_pair2_aux/ qed-.
-
-lemma lpx_inv_pair: ∀h,g,I1,I2,G,L1,L2,V1,V2.  ⦃G, L1.ⓑ{I1}V1⦄ ⊢ ➡[h, g] L2.ⓑ{I2}V2 →
-                    ∧∧ ⦃G, L1⦄ ⊢ ➡[h, g] L2 & ⦃G, L1⦄ ⊢ V1 ➡[h, g] V2 & I1 = I2.
-/2 width=1 by lpx_sn_inv_pair/ qed-.
-
-(* Basic properties *********************************************************)
-
-lemma lpx_refl: ∀h,g,G,L.  ⦃G, L⦄ ⊢ ➡[h, g] L.
-/2 width=1 by lpx_sn_refl/ qed.
-
-lemma lpx_pair: ∀h,g,I,G,K1,K2,V1,V2. ⦃G, K1⦄ ⊢ ➡[h, g] K2 → ⦃G, K1⦄ ⊢ V1 ➡[h, g] V2 →
-                ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡[h, g] K2.ⓑ{I}V2.
-/2 width=1 by lpx_sn_pair/ qed.
-
-lemma lpr_lpx: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L1⦄ ⊢ ➡[h, g] L2.
-#h #g #G #L1 #L2 #H elim H -L1 -L2 /3 width=1 by lpx_pair, cpr_cpx/
-qed.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma lpx_fwd_length: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → |L1| = |L2|.
-/2 width=2 by lpx_sn_fwd_length/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_aaa.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_aaa.etc
deleted file mode 100644
index f9c2374c2..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_aaa.etc
+++ /dev/null
@@ -1,83 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/static/aaa_lift.ma".
-include "basic_2/static/lsuba_aaa.ma".
-include "basic_2/reduction/lpx_ldrop.ma".
-
-(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
-
-(* Properties on atomic arity assignment for terms **************************)
-
-(* Note: lemma 500 *)
-lemma aaa_cpx_lpx_conf: ∀h,g,G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A →
-                        ∀T2. ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2 →
-                        ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → ⦃G, L2⦄ ⊢ T2 ⁝ A.
-#h #g #G #L1 #T1 #A #H elim H -G -L1 -T1 -A
-[ #g #L1 #k #X #H
-  elim (cpx_inv_sort1 … H) -H // * //
-| #I #G #L1 #K1 #V1 #B #i #HLK1 #_ #IHV1 #X #H #L2 #HL12
-  elim (cpx_inv_lref1 … H) -H
-  [ #H destruct
-    elim (lpx_ldrop_conf … HLK1 … HL12) -L1 #X #H #HLK2
-    elim (lpx_inv_pair1 … H) -H
-    #K2 #V2 #HK12 #HV12 #H destruct /3 width=6 by aaa_lref/
-  | * #J #Y #Z #V2 #H #HV12 #HV2
-    lapply (ldrop_mono … H … HLK1) -H #H destruct
-    elim (lpx_ldrop_conf … HLK1 … HL12) -L1 #Z #H #HLK2
-    elim (lpx_inv_pair1 … H) -H #K2 #V0 #HK12 #_ #H destruct
-    /3 width=8 by aaa_lift, ldrop_fwd_drop2/
-  ]
-| #a #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12
-  elim (cpx_inv_abbr1 … H) -H *
-  [ #V2 #T2 #HV12 #HT12 #H destruct /4 width=2 by lpx_pair, aaa_abbr/
-  | #T2 #HT12 #HT2 #H destruct -IHV1
-    /4 width=8 by lpx_pair, aaa_inv_lift, ldrop_drop/
-  ]
-| #a #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12
-  elim (cpx_inv_abst1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
-  /4 width=1 by lpx_pair, aaa_abst/
-| #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12
-  elim (cpx_inv_appl1 … H) -H *
-  [ #V2 #T2 #HV12 #HT12 #H destruct /3 width=3 by aaa_appl/
-  | #b #V2 #W1 #W2 #U1 #U2 #HV12 #HW12 #HU12 #H1 #H2 destruct
-    lapply (IHV1 … HV12 … HL12) -IHV1 -HV12 #HV2
-    lapply (IHT1 (ⓛ{b}W2.U2) … HL12) -IHT1 /2 width=1 by cpx_bind/ -L1 #H
-    elim (aaa_inv_abst … H) -H #B0 #A0 #HW1 #HU2 #H destruct
-    /5 width=6 by lsuba_aaa_trans, lsuba_abbr, aaa_abbr, aaa_cast/
-  | #b #V #V2 #W1 #W2 #U1 #U2 #HV1 #HV2 #HW12 #HU12 #H1 #H2 destruct
-    lapply (aaa_lift G L2 … B … (L2.ⓓW2) … HV2) -HV2 /2 width=2 by ldrop_drop/ #HV2
-    lapply (IHT1 (ⓓ{b}W2.U2) … HL12) -IHT1 /2 width=1 by cpx_bind/ -L1 #H
-    elim (aaa_inv_abbr … H) -H /3 width=3 by aaa_abbr, aaa_appl/
-  ]
-| #G #L1 #V1 #T1 #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12
-  elim (cpx_inv_cast1 … H) -H
-  [ * #V2 #T2 #HV12 #HT12 #H destruct /3 width=1 by aaa_cast/
-  | -IHV1 /2 width=1 by/
-  | -IHT1 /2 width=1 by/
-  ]
-]
-qed-.
-
-lemma aaa_cpx_conf: ∀h,g,G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A → ∀T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → ⦃G, L⦄ ⊢ T2 ⁝ A.
-/2 width=7 by aaa_cpx_lpx_conf/ qed-.
-
-lemma aaa_lpx_conf: ∀h,g,G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → ⦃G, L2⦄ ⊢ T ⁝ A.
-/2 width=7 by aaa_cpx_lpx_conf/ qed-.
-
-lemma aaa_cpr_conf: ∀G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A → ∀T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ⦃G, L⦄ ⊢ T2 ⁝ A.
-/3 width=5 by aaa_cpx_conf, cpr_cpx/ qed-.
-
-lemma aaa_lpr_conf: ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T ⁝ A.
-/3 width=5 by aaa_lpx_conf, lpr_lpx/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_ldrop.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_ldrop.etc
deleted file mode 100644
index 188e8d11b..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_ldrop.etc
+++ /dev/null
@@ -1,78 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/relocation/ldrop_lpx_sn.ma".
-include "basic_2/reduction/cpx_lift.ma".
-include "basic_2/reduction/lpx.ma".
-
-(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
-
-(* Properies on local environment slicing ***********************************)
-
-lemma lpx_ldrop_conf: ∀h,g,G. dropable_sn (lpx h g G).
-/3 width=6 by lpx_sn_deliftable_dropable, cpx_inv_lift1/ qed-.
-
-lemma ldrop_lpx_trans: ∀h,g,G. dedropable_sn (lpx h g G).
-/3 width=10 by lpx_sn_liftable_dedropable, cpx_lift/ qed-.
-
-lemma lpx_ldrop_trans_O1: ∀h,g,G. dropable_dx (lpx h g G).
-/2 width=3 by lpx_sn_dropable/ qed-.
-
-(* Properties on supclosure *************************************************)
-
-lemma fqu_lpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
-                     ∀K2. ⦃G2, L2⦄ ⊢ ➡[h, g] K2 →
-                     ∃∃K1,T. ⦃G1, L1⦄ ⊢ ➡[h, g] K1 & ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃ ⦃G2, K2, T2⦄.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
-/3 width=5 by fqu_lref_O, fqu_pair_sn, fqu_flat_dx, lpx_pair, ex3_2_intro/
-[ #a #I #G2 #L2 #V2 #T2 #X #H elim (lpx_inv_pair1 … H) -H
-  #K2 #W2 #HLK2 #HVW2 #H destruct
-  /3 width=5 by fqu_fquq, cpx_pair_sn, fqu_bind_dx, ex3_2_intro/
-| #G #L1 #K1 #T1 #U1 #e #HLK1 #HTU1 #K2 #HK12
-  elim (ldrop_lpx_trans … HLK1 … HK12) -HK12
-  /3 width=7 by fqu_drop, ex3_2_intro/
-]
-qed-.
-
-lemma fquq_lpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
-                      ∀K2. ⦃G2, L2⦄ ⊢ ➡[h, g] K2 →
-                      ∃∃K1,T. ⦃G1, L1⦄ ⊢ ➡[h, g] K1 & ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K2 #HLK2 elim (fquq_inv_gen … H) -H
-[ #HT12 elim (fqu_lpx_trans … HT12 … HLK2) /3 width=5 by fqu_fquq, ex3_2_intro/
-| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/
-]
-qed-.
-
-lemma lpx_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
-                     ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 →
-                     ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
-/3 width=7 by fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, lpx_pair, ex3_2_intro/
-[ #I #G1 #L1 #V1 #X #H elim (lpx_inv_pair2 … H) -H
-  #K1 #W1 #HKL1 #HWV1 #H destruct elim (lift_total V1 0 1)
-  /4 width=7 by cpx_delta, fqu_drop, ldrop_drop, ex3_2_intro/
-| #G #L1 #K1 #T1 #U1 #e #HLK1 #HTU1 #L0 #HL01
-  elim (lpx_ldrop_trans_O1 … HL01 … HLK1) -L1
-  /3 width=5 by fqu_drop, ex3_2_intro/
-]
-qed-.
-
-lemma lpx_fquq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
-                      ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 →
-                      ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #HKL1 elim (fquq_inv_gen … H) -H
-[ #HT12 elim (lpx_fqu_trans … HT12 … HKL1) /3 width=5 by fqu_fquq, ex3_2_intro/
-| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/
-]
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_lleq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_lleq.etc
deleted file mode 100644
index 353f810c3..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_lleq.etc
+++ /dev/null
@@ -1,108 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/relocation/lleq_ldrop.ma".
-include "basic_2/reduction/lpx_ldrop.ma".
-
-(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
-
-(* Properties on lazy equivalence for local environments ********************)
-(*
-lamma pippo: ∀h,g,G,L2,K2. ⦃G, L2⦄ ⊢ ➡[h, g] K2 → ∀L1. |L1| = |L2| →
-             ∃∃K1. ⦃G, L1⦄ ⊢ ➡[h, g] K1 & |K1| = |K2| &
-                   (∀T,d. L1 ⋕[T, d] L2 ↔ K1 ⋕[T, d] K2).
-#h #g #G #L2 #K2 #H elim H -L2 -K2
-[ #L1 #H >(length_inv_zero_dx … H) -L1 /3 width=5 by ex3_intro, conj/
-| #I2 #L2 #K2 #V2 #W2 #_ #HVW2 #IHLK2 #Y #H
-  elim (length_inv_pos_dx … H) -H #I #L1 #V1 #HL12 #H destruct
-  elim (IHLK2 … HL12) -IHLK2 #K1 #HLK1 #HK12 #IH
-  elim (eq_term_dec V1 V2) #H destruct
-  [ @(ex3_intro … (K1.ⓑ{I}W2)) normalize /2 width=1 by /
-*)
-axiom lleq_lpx_trans: ∀h,g,G,L2,K2. ⦃G, L2⦄ ⊢ ➡[h, g] K2 →
-                      ∀L1,T,d. L1 ⋕[T, d] L2 →
-                      ∃∃K1. ⦃G, L1⦄ ⊢ ➡[h, g] K1 & K1 ⋕[T, d] K2.
-(*
-#h #g #G #L2 #K2 #H elim H -L2 -K2
-[ #L1 #T #d #H lapply (lleq_fwd_length … H) -H
-  #H >(length_inv_zero_dx … H) -L1 /2 width=3 by ex2_intro/
-| #I2 #L2 #K2 #V2 #W2 #HLK2 #HVW2 #IHLK2 #Y #T #d #HT
-  lapply (lleq_fwd_length … HT) #H
-  elim (length_inv_pos_dx … H) -H #I1 #L1 #V1 #HL12 #H destruct
-  elim (eq_term_dec V1 V2) #H destruct
-  [ @ex2_intro …
-*)
-
-lemma lpx_lleq_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
-                          ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1, 0] L1 →
-                          ∃∃K2. ⦃G1, K1, T1⦄ ⊃ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2, 0] L2.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
-[ #I #G1 #L1 #V1 #X #H1 #H2 elim (lpx_inv_pair2 … H1) -H1
-  #K0 #V0 #H1KL1 #_ #H destruct
-  elim (lleq_inv_lref_ge_dx … H2 ? I L1 V1) -H2 //
-  #K1 #H #H2KL1 lapply (ldrop_inv_O2 … H) -H #H destruct
-  /2 width=4 by fqu_lref_O, ex3_intro/
-| * [ #a ] #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H
-  [ elim (lleq_inv_bind … H)
-  | elim (lleq_inv_flat … H)
-  ] -H /2 width=4 by fqu_pair_sn, ex3_intro/
-| #a #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_bind_O … H) -H
-  /3 width=4 by lpx_pair, fqu_bind_dx, ex3_intro/
-| #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_flat … H) -H
-  /2 width=4 by fqu_flat_dx, ex3_intro/
-| #G1 #L1 #L #T1 #U1 #e #HL1 #HTU1 #K1 #H1KL1 #H2KL1
-  elim (ldrop_O1_le (e+1) K1)
-  [ #K #HK1 lapply (lleq_inv_lift_le … H2KL1 … HK1 HL1 … HTU1 ?) -H2KL1 //
-    #H2KL elim (lpx_ldrop_trans_O1 … H1KL1 … HL1) -L1
-    #K0 #HK10 #H1KL lapply (ldrop_mono … HK10 … HK1) -HK10 #H destruct
-    /3 width=4 by fqu_drop, ex3_intro/
-  | lapply (ldrop_fwd_length_le2 … HL1) -L -T1 -g
-    lapply (lleq_fwd_length … H2KL1) //
-  ]
-]
-qed-.
-
-lemma lpx_lleq_fquq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
-                           ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1, 0] L1 →
-                           ∃∃K2. ⦃G1, K1, T1⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2, 0] L2.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1
-elim (fquq_inv_gen … H) -H
-[ #H elim (lpx_lleq_fqu_trans … H … H1KL1 H2KL1) -L1
-  /3 width=4 by fqu_fquq, ex3_intro/
-| * #HG #HL #HT destruct /2 width=4 by ex3_intro/
-]
-qed-.
-
-lemma lpx_lleq_fqup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ →
-                           ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1, 0] L1 →
-                           ∃∃K2. ⦃G1, K1, T1⦄ ⊃+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2, 0] L2.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
-[ #G2 #L2 #T2 #H #K1 #H1KL1 #H2KL1 elim (lpx_lleq_fqu_trans … H … H1KL1 H2KL1) -L1
-  /3 width=4 by fqu_fqup, ex3_intro/
-| #G #G2 #L #L2 #T #T2 #_ #HT2 #IHT1 #K1 #H1KL1 #H2KL1 elim (IHT1 … H2KL1) // -L1
-  #K #HT1 #H1KL #H2KL elim (lpx_lleq_fqu_trans … HT2 … H1KL H2KL) -L
-  /3 width=5 by fqup_strap1, ex3_intro/
-]
-qed-.
-
-lemma lpx_lleq_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
-                           ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1, 0] L1 →
-                           ∃∃K2. ⦃G1, K1, T1⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2, 0] L2.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1
-elim (fqus_inv_gen … H) -H
-[ #H elim (lpx_lleq_fqup_trans … H … H1KL1 H2KL1) -L1
-  /3 width=4 by fqup_fqus, ex3_intro/
-| * #HG #HL #HT destruct /2 width=4 by ex3_intro/
-]
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs.etc
deleted file mode 100644
index 35a8cb482..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs.etc
+++ /dev/null
@@ -1,74 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/notation/relations/predsnstar_5.ma".
-include "basic_2/reduction/lpx.ma".
-include "basic_2/computation/lprs.ma".
-
-(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************)
-
-definition lpxs: ∀h. sd h → relation3 genv lenv lenv ≝
-                 λh,g,G. TC … (lpx h g G).
-
-interpretation "extended parallel computation (local environment, sn variant)"
-   'PRedSnStar h g G L1 L2 = (lpxs h g G L1 L2).
-
-(* Basic eliminators ********************************************************)
-
-lemma lpxs_ind: ∀h,g,G,L1. ∀R:predicate lenv. R L1 →
-                (∀L,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L → ⦃G, L⦄ ⊢ ➡[h, g] L2 → R L → R L2) →
-                ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → R L2.
-#h #g #G #L1 #R #HL1 #IHL1 #L2 #HL12
-@(TC_star_ind … HL1 IHL1 … HL12) //
-qed-.
-
-lemma lpxs_ind_dx: ∀h,g,G,L2. ∀R:predicate lenv. R L2 →
-                   (∀L1,L. ⦃G, L1⦄ ⊢ ➡[h, g] L → ⦃G, L⦄ ⊢ ➡*[h, g] L2 → R L → R L1) →
-                   ∀L1. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → R L1.
-#h #g #G #L2 #R #HL2 #IHL2 #L1 #HL12
-@(TC_star_ind_dx … HL2 IHL2 … HL12) //
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma lprs_lpxs: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2.
-/3 width=3/ qed.
-
-lemma lpx_lpxs: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2.
-/2 width=1/ qed.
-
-lemma lpxs_refl: ∀h,g,G,L. ⦃G, L⦄ ⊢ ➡*[h, g] L.
-/2 width=1/ qed.
-
-lemma lpxs_strap1: ∀h,g,G,L1,L,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L → ⦃G, L⦄ ⊢ ➡[h, g] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2.
-/2 width=3/ qed.
-
-lemma lpxs_strap2: ∀h,g,G,L1,L,L2. ⦃G, L1⦄ ⊢ ➡[h, g] L → ⦃G, L⦄ ⊢ ➡*[h, g] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2.
-/2 width=3/ qed.
-
-lemma lpxs_pair_refl: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → ∀I,V. ⦃G, L1.ⓑ{I}V⦄ ⊢ ➡*[h, g] L2.ⓑ{I}V.
-/2 width=1 by TC_lpx_sn_pair_refl/ qed.
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma lpxs_inv_atom1: ∀h,g,G,L2. ⦃G, ⋆⦄ ⊢ ➡*[h, g] L2 → L2 = ⋆.
-/2 width=2 by TC_lpx_sn_inv_atom1/ qed-.
-
-lemma lpxs_inv_atom2: ∀h,g,G,L1. ⦃G, L1⦄ ⊢ ➡*[h, g] ⋆ → L1 = ⋆.
-/2 width=2 by TC_lpx_sn_inv_atom2/ qed-.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma lpxs_fwd_length: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → |L1| = |L2|.
-/2 width=2 by TC_lpx_sn_fwd_length/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_aaa.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_aaa.etc
deleted file mode 100644
index 80c43c731..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_aaa.etc
+++ /dev/null
@@ -1,32 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/reduction/lpx_aaa.ma".
-include "basic_2/computation/lpxs.ma".
-
-(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************)
-
-(* Properties about atomic arity assignment on terms ************************)
-
-lemma aaa_lpxs_conf: ∀h,g,G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A →
-                     ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → ⦃G, L2⦄ ⊢ T ⁝ A.
-#h #g #G #L1 #T #A #HT #L2 #HL12
-@(TC_Conf3 … (λL,A. ⦃G, L⦄ ⊢ T ⁝ A) … HT ? HL12) /2 width=5 by aaa_lpx_conf/
-qed-.
-
-lemma aaa_lprs_conf: ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A →
-                     ∀L2. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L2⦄ ⊢ T ⁝ A.
-#G #L1 #T #A #HT #L2 #HL12
-@(aaa_lpxs_conf … HT) -A -T /2 width=3/
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_alt.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_alt.etc
deleted file mode 100644
index 8a6b30a57..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_alt.etc
+++ /dev/null
@@ -1,47 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/notation/relations/predsnstaralt_5.ma".
-include "basic_2/computation/cpxs_cpxs.ma".
-include "basic_2/computation/lpxs.ma".
-
-(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************)
-
-(* alternative definition *)
-definition lpxsa: ∀h. sd h → relation3 genv lenv lenv ≝
-                  λh,g,G. lpx_sn … (cpxs h g G).
-
-interpretation "extended parallel computation (local environment, sn variant) alternative"
-   'PRedSnStarAlt h g G L1 L2 = (lpxsa h g G L1 L2).
-
-(* Main properties on the alternative definition ****************************)
-
-theorem lpxsa_lpxs: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡➡*[h, g] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2.
-/2 width=1 by lpx_sn_LTC_TC_lpx_sn/ qed-.
-
-(* Main inversion lemmas on the alternative definition **********************)
-
-theorem lpxs_inv_lpxsa: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → ⦃G, L1⦄ ⊢ ➡➡*[h, g] L2.
-/3 width=3 by TC_lpx_sn_inv_lpx_sn_LTC, lpx_cpxs_trans/ qed-.
-
-(* Alternative eliminators **************************************************)
-
-lemma lpxs_ind_alt: ∀h,g,G. ∀R:relation lenv.
-                    R (⋆) (⋆) → (
-                       ∀I,K1,K2,V1,V2.
-                       ⦃G, K1⦄ ⊢ ➡*[h, g] K2 → ⦃G, K1⦄ ⊢ V1 ➡*[h, g] V2 →
-                       R K1 K2 → R (K1.ⓑ{I}V1) (K2.ⓑ{I}V2)
-                    ) →
-                    ∀L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → R L1 L2.
-/3 width=4 by TC_lpx_sn_ind, lpx_cpxs_trans/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_cpxs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_cpxs.etc
deleted file mode 100644
index 2f21a8d70..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_cpxs.etc
+++ /dev/null
@@ -1,147 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/computation/cpxs_cpxs.ma".
-include "basic_2/computation/lpxs.ma".
-
-(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************)
-
-(* Advanced properties ******************************************************)
-
-lemma lpxs_pair: ∀h,g,I,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 →
-                 ∀V1,V2. ⦃G, L1⦄ ⊢ V1 ➡*[h, g] V2 →
-                 ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡*[h, g] L2.ⓑ{I}V2.
-/2 width=1 by TC_lpx_sn_pair/ qed.
-
-(* Advanced inversion lemmas ************************************************)
-
-lemma lpxs_inv_pair1: ∀h,g,I,G,K1,L2,V1. ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡*[h, g] L2 →
-                      ∃∃K2,V2. ⦃G, K1⦄ ⊢ ➡*[h, g] K2 & ⦃G, K1⦄ ⊢ V1 ➡*[h, g] V2 & L2 = K2.ⓑ{I}V2.
-/3 width=3 by TC_lpx_sn_inv_pair1, lpx_cpxs_trans/ qed-.
-
-lemma lpxs_inv_pair2: ∀h,g,I,G,L1,K2,V2. ⦃G, L1⦄ ⊢ ➡*[h, g] K2.ⓑ{I}V2 →
-                      ∃∃K1,V1. ⦃G, K1⦄ ⊢ ➡*[h, g] K2 & ⦃G, K1⦄ ⊢ V1 ➡*[h, g] V2 & L1 = K1.ⓑ{I}V1.
-/3 width=3 by TC_lpx_sn_inv_pair2, lpx_cpxs_trans/ qed-.
-
-(* Properties on context-sensitive extended parallel computation for terms **)
-
-lemma lpxs_cpx_trans: ∀h,g,G. s_r_trans … (cpx h g G) (lpxs h g G).
-/3 width=5 by s_r_trans_TC2, lpx_cpxs_trans/ qed-.
-
-lemma lpxs_cpxs_trans: ∀h,g,G. s_rs_trans … (cpx h g G) (lpxs h g G).
-/3 width=5 by s_r_trans_TC1, lpxs_cpx_trans/ qed-.
-
-lemma cpxs_bind2: ∀h,g,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 →
-                  ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ➡*[h, g] T2 →
-                  ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡*[h, g] ⓑ{a,I}V2.T2.
-/4 width=5 by lpxs_cpxs_trans, lpxs_pair, cpxs_bind/ qed.
-
-(* Inversion lemmas on context-sensitive ext parallel computation for terms *)
-
-lemma cpxs_inv_abst1: ∀h,g,a,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{a}V1.T1 ➡*[h, g] U2 →
-                      ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 & ⦃G, L.ⓛV1⦄ ⊢ T1 ➡*[h, g] T2 &
-                               U2 = ⓛ{a}V2.T2.
-#h #g #a #G #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 /2 width=5 by ex3_2_intro/
-#U0 #U2 #_ #HU02 * #V0 #T0 #HV10 #HT10 #H destruct
-elim (cpx_inv_abst1 … HU02) -HU02 #V2 #T2 #HV02 #HT02 #H destruct
-lapply (lpxs_cpx_trans … HT02 (L.ⓛV1) ?)
-/3 width=5 by lpxs_pair, cpxs_trans, cpxs_strap1, ex3_2_intro/
-qed-.
-
-lemma cpxs_inv_abbr1: ∀h,g,a,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{a}V1.T1 ➡*[h, g] U2 → (
-                      ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 & ⦃G, L.ⓓV1⦄ ⊢ T1 ➡*[h, g] T2 &
-                               U2 = ⓓ{a}V2.T2
-                      ) ∨
-                      ∃∃T2. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡*[h, g] T2 & ⇧[0, 1] U2 ≡ T2 & a = true.
-#h #g #a #G #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 /3 width=5 by ex3_2_intro, or_introl/
-#U0 #U2 #_ #HU02 * *
-[ #V0 #T0 #HV10 #HT10 #H destruct
-  elim (cpx_inv_abbr1 … HU02) -HU02 *
-  [ #V2 #T2 #HV02 #HT02 #H destruct
-    lapply (lpxs_cpx_trans … HT02 (L.ⓓV1) ?)
-    /4 width=5 by lpxs_pair, cpxs_trans, cpxs_strap1, ex3_2_intro, or_introl/
-  | #T2 #HT02 #HUT2
-    lapply (lpxs_cpx_trans … HT02 (L.ⓓV1) ?) -HT02
-    /4 width=3 by lpxs_pair, cpxs_trans, ex3_intro, or_intror/
-  ]
-| #U1 #HTU1 #HU01
-  elim (lift_total U2 0 1) #U #HU2
-  /6 width=12 by cpxs_strap1, cpx_lift, ldrop_drop, ex3_intro, or_intror/
-]
-qed-.
-
-(* More advanced properties *************************************************)
-
-lemma lpxs_pair2: ∀h,g,I,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 →
-                  ∀V1,V2. ⦃G, L2⦄ ⊢ V1 ➡*[h, g] V2 → ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡*[h, g] L2.ⓑ{I}V2.
-/3 width=3 by lpxs_pair, lpxs_cpxs_trans/ qed.
-
-(* Properties on supclosure *************************************************)
-
-lemma lpx_fqup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ →
-                      ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 →
-                      ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
-[ #G2 #L2 #T2 #H12 #K1 #HKL1 elim (lpx_fqu_trans … H12 … HKL1) -L1
-  /3 width=5 by cpx_cpxs, fqu_fqup, ex3_2_intro/
-| #G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1
-  #L0 #T0 #HT10 #HT0 #HL0 elim (lpx_fqu_trans … H2 … HL0) -L
-  #L #T3 #HT3 #HT32 #HL2 elim (fqup_cpx_trans … HT0 … HT3) -T
-  /3 width=7 by cpxs_strap1, fqup_strap1, ex3_2_intro/
-]
-qed-.
-
-lemma lpx_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
-                      ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 →
-                      ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -G2 -L2 -T2 /2 width=5 by ex3_2_intro/
-#G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1
-#L0 #T0 #HT10 #HT0 #HL0 elim (lpx_fquq_trans … H2 … HL0) -L
-#L #T3 #HT3 #HT32 #HL2 elim (fqus_cpx_trans … HT0 … HT3) -T
-/3 width=7 by cpxs_strap1, fqus_strap1, ex3_2_intro/
-qed-.
-
-lemma lpxs_fquq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
-                       ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 →
-                       ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #HT12 #K1 #H @(lpxs_ind_dx … H) -K1
-[ /2 width=5 by ex3_2_intro/
-| #K1 #K #HK1 #_ * #L #T #HT1 #HT2 #HL2 -HT12
-  lapply (lpx_cpxs_trans … HT1 … HK1) -HT1
-  elim (lpx_fquq_trans … HT2 … HK1) -K
-  /3 width=7 by lpxs_strap2, cpxs_strap1, ex3_2_intro/
-]
-qed-.
-
-lemma lpxs_fqup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ →
-                       ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 →
-                       ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #HT12 #K1 #H @(lpxs_ind_dx … H) -K1
-[ /2 width=5 by ex3_2_intro/
-| #K1 #K #HK1 #_ * #L #T #HT1 #HT2 #HL2 -HT12
-  lapply (lpx_cpxs_trans … HT1 … HK1) -HT1
-  elim (lpx_fqup_trans … HT2 … HK1) -K
-  /3 width=7 by lpxs_strap2, cpxs_trans, ex3_2_intro/
-]
-qed-.
-
-lemma lpxs_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
-                       ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 →
-                       ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -G2 -L2 -T2 /2 width=5 by ex3_2_intro/
-#G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1
-#L0 #T0 #HT10 #HT0 #HL0 elim (lpxs_fquq_trans … H2 … HL0) -L
-#L #T3 #HT3 #HT32 #HL2 elim (fqus_cpxs_trans … HT3 … HT0) -T
-/3 width=7 by cpxs_trans, fqus_strap1, ex3_2_intro/
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_ldrop.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_ldrop.etc
deleted file mode 100644
index d8c489017..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_ldrop.etc
+++ /dev/null
@@ -1,29 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/reduction/lpx_ldrop.ma".
-include "basic_2/computation/lpxs.ma".
-
-(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************)
-
-(* Properies on local environment slicing ***********************************)
-
-lemma lpxs_ldrop_conf: ∀h,g,G. dropable_sn (lpxs h g G).
-/3 width=3 by dropable_sn_TC, lpx_ldrop_conf/ qed-.
-
-lemma ldrop_lpxs_trans: ∀h,g,G. dedropable_sn (lpxs h g G).
-/3 width=3 by dedropable_sn_TC, ldrop_lpx_trans/ qed-.
-
-lemma lpxs_ldrop_trans_O1: ∀h,g,G. dropable_dx (lpxs h g G).
-/3 width=3 by dropable_dx_TC, lpx_ldrop_trans_O1/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_lleq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_lleq.etc
deleted file mode 100644
index e21c79912..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_lleq.etc
+++ /dev/null
@@ -1,125 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/relocation/lleq_leq.ma".
-include "basic_2/reduction/lpx_lleq.ma".
-include "basic_2/computation/cpxs_leq.ma".
-include "basic_2/computation/lpxs_ldrop.ma".
-include "basic_2/computation/lpxs_cpxs.ma".
-
-(* SN EXTENDED PARALLEL COMPUTATION FOR LOCAL ENVIRONMENTS ******************)
-
-(* Properties on lazy equivalence for local environments ********************)
-
-lemma lleq_lpxs_trans: ∀h,g,G,L2,K2. ⦃G, L2⦄ ⊢ ➡*[h, g] K2 →
-                       ∀L1,T,d. L1 ⋕[T, d] L2 →
-                       ∃∃K1. ⦃G, L1⦄ ⊢ ➡*[h, g] K1 & K1 ⋕[T, d] K2.
-#h #g #G #L2 #K2 #H @(lpxs_ind … H) -K2 /2 width=3 by ex2_intro/
-#K #K2 #_ #HK2 #IH #L1 #T #d #HT elim (IH … HT) -L2
-#L #HL1 #HT elim (lleq_lpx_trans … HK2 … HT) -K
-/3 width=3 by lpxs_strap1, ex2_intro/
-qed-.
-
-lemma lpxs_lleq_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
-                           ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ⋕[T1, 0] L1 →
-                           ∃∃K2. ⦃G1, K1, T1⦄ ⊃ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ⋕[T2, 0] L2.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
-[ #I #G1 #L1 #V1 #X #H1 #H2 elim (lpxs_inv_pair2 … H1) -H1
-  #K0 #V0 #H1KL1 #_ #H destruct
-  elim (lleq_inv_lref_ge_dx … H2 ? I L1 V1) -H2 //
-  #K1 #H #H2KL1 lapply (ldrop_inv_O2 … H) -H #H destruct
-  /2 width=4 by fqu_lref_O, ex3_intro/
-| * [ #a ] #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H
-  [ elim (lleq_inv_bind … H)
-  | elim (lleq_inv_flat … H)
-  ] -H /2 width=4 by fqu_pair_sn, ex3_intro/
-| #a #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_bind_O … H) -H
-  /3 width=4 by lpxs_pair, fqu_bind_dx, ex3_intro/
-| #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_flat … H) -H
-  /2 width=4 by fqu_flat_dx, ex3_intro/
-| #G1 #L1 #L #T1 #U1 #e #HL1 #HTU1 #K1 #H1KL1 #H2KL1
-  elim (ldrop_O1_le (e+1) K1)
-  [ #K #HK1 lapply (lleq_inv_lift_le … H2KL1 … HK1 HL1 … HTU1 ?) -H2KL1 //
-    #H2KL elim (lpxs_ldrop_trans_O1 … H1KL1 … HL1) -L1
-    #K0 #HK10 #H1KL lapply (ldrop_mono … HK10 … HK1) -HK10 #H destruct
-    /3 width=4 by fqu_drop, ex3_intro/
-  | lapply (ldrop_fwd_length_le2 … HL1) -L -T1 -g
-    lapply (lleq_fwd_length … H2KL1) //
-  ]
-]
-qed-.
-
-lemma lpxs_lleq_fquq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
-                            ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ⋕[T1, 0] L1 →
-                            ∃∃K2. ⦃G1, K1, T1⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ⋕[T2, 0] L2.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1
-elim (fquq_inv_gen … H) -H
-[ #H elim (lpxs_lleq_fqu_trans … H … H1KL1 H2KL1) -L1
-  /3 width=4 by fqu_fquq, ex3_intro/
-| * #HG #HL #HT destruct /2 width=4 by ex3_intro/
-]
-qed-.
-
-lemma lpxs_lleq_fqup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ →
-                            ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ⋕[T1, 0] L1 →
-                            ∃∃K2. ⦃G1, K1, T1⦄ ⊃+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ⋕[T2, 0] L2.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
-[ #G2 #L2 #T2 #H #K1 #H1KL1 #H2KL1 elim (lpxs_lleq_fqu_trans … H … H1KL1 H2KL1) -L1
-  /3 width=4 by fqu_fqup, ex3_intro/
-| #G #G2 #L #L2 #T #T2 #_ #HT2 #IHT1 #K1 #H1KL1 #H2KL1 elim (IHT1 … H2KL1) // -L1
-  #K #HT1 #H1KL #H2KL elim (lpxs_lleq_fqu_trans … HT2 … H1KL H2KL) -L
-  /3 width=5 by fqup_strap1, ex3_intro/
-]
-qed-.
-
-lemma lpxs_lleq_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
-                            ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ⋕[T1, 0] L1 →
-                            ∃∃K2. ⦃G1, K1, T1⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ⋕[T2, 0] L2.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1
-elim (fqus_inv_gen … H) -H
-[ #H elim (lpxs_lleq_fqup_trans … H … H1KL1 H2KL1) -L1
-  /3 width=4 by fqup_fqus, ex3_intro/
-| * #HG #HL #HT destruct /2 width=4 by ex3_intro/
-]
-qed-.
-
-fact leq_lpxs_trans_lleq_aux: ∀h,g,G,L1,L0,d,e. L1 ≃[d, e] L0 → e = ∞ →
-                              ∀L2. ⦃G, L0⦄ ⊢ ➡*[h, g] L2 →
-                              ∃∃L. L ≃[d, e] L2 & ⦃G, L1⦄ ⊢ ➡*[h, g] L &
-                                   (∀T. L0 ⋕[T, d] L2 ↔ L1 ⋕[T, d] L).
-#h #g #G #L1 #L0 #d #e #H elim H -L1 -L0 -d -e
-[ #d #e #_ #L2 #H >(lpxs_inv_atom1 … H) -H
-  /3 width=5 by ex3_intro, conj/
-| #I1 #I0 #L1 #L0 #V1 #V0 #_ #_ #He destruct
-| #I #L1 #L0 #V1 #e #HL10 #IHL10 #He #Y #H
-  elim (lpxs_inv_pair1 … H) -H #L2 #V2 #HL02 #HV02 #H destruct
-  lapply (ysucc_inv_Y_dx … He) -He #He
-  elim (IHL10 … HL02) // -IHL10 -HL02 #L #HL2 #HL1 #IH
-  @(ex3_intro … (L.ⓑ{I}V2)) /3 width=3 by lpxs_pair, leq_cpxs_trans, leq_pair/
-  #T elim (IH T) #HL0dx #HL0sn
-  @conj #H @(lleq_leq_repl … H) -H /3 width=1 by leq_sym, leq_pair_O_Y/
-| #I1 #I0 #L1 #L0 #V1 #V0 #d #e #HL10 #IHL10 #He #Y #H
-  elim (lpxs_inv_pair1 … H) -H #L2 #V2 #HL02 #HV02 #H destruct
-  elim (IHL10 … HL02) // -IHL10 -HL02 #L #HL2 #HL1 #IH
-  @(ex3_intro … (L.ⓑ{I1}V1)) /3 width=1 by lpxs_pair, leq_succ/
-  #T elim (IH T) #HL0dx #HL0sn
-  @conj #H @(lleq_leq_repl … H) -H /3 width=1 by leq_sym, leq_succ/
-]
-qed-.
-
-lemma leq_lpxs_trans_lleq: ∀h,g,G,L1,L0,d. L1 ≃[d, ∞] L0 →
-                           ∀L2. ⦃G, L0⦄ ⊢ ➡*[h, g] L2 →
-                           ∃∃L. L ≃[d, ∞] L2 & ⦃G, L1⦄ ⊢ ➡*[h, g] L &
-                                (∀T. L0 ⋕[T, d] L2 ↔ L1 ⋕[T, d] L).
-/2 width=1 by leq_lpxs_trans_lleq_aux/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_lpxs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_lpxs.etc
deleted file mode 100644
index 998f89e14..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_lpxs.etc
+++ /dev/null
@@ -1,22 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/computation/lpxs.ma".
-
-(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************)
-
-(* Main properties **********************************************************)
-
-theorem lpxs_trans: ∀h,g,G. Transitive … (lpxs h g G).
-/2 width=3/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsn_5.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsn_5.etc
deleted file mode 100644
index 206566071..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsn_5.etc
+++ /dev/null
@@ -1,19 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡ break [ term 46 h , break term 46 g ] break term 46 L2 )"
-   non associative with precedence 45
-   for @{ 'PRedSn $h $g $G $L1 $L2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsnstar_5.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsnstar_5.etc
deleted file mode 100644
index aef4f2707..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsnstar_5.etc
+++ /dev/null
@@ -1,19 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡ * break [ term 46 h , break term 46 g ] break term 46 L2 )"
-   non associative with precedence 45
-   for @{ 'PRedSnStar $h $g $G $L1 $L2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsnstaralt_5.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsnstaralt_5.etc
deleted file mode 100644
index 9682647cd..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsnstaralt_5.etc
+++ /dev/null
@@ -1,19 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡ ➡ * break [ term 46 h , break term 46 g ] break term 46 L2 )"
-   non associative with precedence 45
-   for @{ 'PRedSnStarAlt $h $g $G $L1 $L2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazycosn_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazycosn_5.ma
new file mode 100644
index 000000000..55c37a8fd
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazycosn_5.ma
@@ -0,0 +1,19 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( G ⊢ ⧤ ⬊ * break [ term 46 h , break term 46 g , break term 46 d ] break term 46 L )"
+   non associative with precedence 45
+   for @{ 'LazyCoSN $h $g $d $G $L }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_5.ma
new file mode 100644
index 000000000..206566071
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_5.ma
@@ -0,0 +1,19 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡ break [ term 46 h , break term 46 g ] break term 46 L2 )"
+   non associative with precedence 45
+   for @{ 'PRedSn $h $g $G $L1 $L2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_5.ma
new file mode 100644
index 000000000..aef4f2707
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_5.ma
@@ -0,0 +1,19 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡ * break [ term 46 h , break term 46 g ] break term 46 L2 )"
+   non associative with precedence 45
+   for @{ 'PRedSnStar $h $g $G $L1 $L2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstaralt_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstaralt_5.ma
new file mode 100644
index 000000000..9682647cd
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstaralt_5.ma
@@ -0,0 +1,19 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡ ➡ * break [ term 46 h , break term 46 g ] break term 46 L2 )"
+   non associative with precedence 45
+   for @{ 'PRedSnStarAlt $h $g $G $L1 $L2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx.ma
new file mode 100644
index 000000000..b10b13a28
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx.ma
@@ -0,0 +1,65 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/notation/relations/predsn_5.ma".
+include "basic_2/reduction/lpr.ma".
+include "basic_2/reduction/cpx.ma".
+
+(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
+
+definition lpx: ∀h. sd h → relation3 genv lenv lenv ≝
+                λh,g,G. lpx_sn (cpx h g G).
+
+interpretation "extended parallel reduction (local environment, sn variant)"
+   'PRedSn h g G L1 L2 = (lpx h g G L1 L2).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma lpx_inv_atom1: ∀h,g,G,L2. ⦃G, ⋆⦄ ⊢ ➡[h, g] L2 → L2 = ⋆.
+/2 width=4 by lpx_sn_inv_atom1_aux/ qed-.
+
+lemma lpx_inv_pair1: ∀h,g,I,G,K1,V1,L2. ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡[h, g] L2 →
+                     ∃∃K2,V2. ⦃G, K1⦄ ⊢ ➡[h, g] K2 & ⦃G, K1⦄ ⊢ V1 ➡[h, g] V2 &
+                              L2 = K2. ⓑ{I} V2.
+/2 width=3 by lpx_sn_inv_pair1_aux/ qed-.
+
+lemma lpx_inv_atom2: ∀h,g,G,L1.  ⦃G, L1⦄ ⊢ ➡[h, g] ⋆ → L1 = ⋆.
+/2 width=4 by lpx_sn_inv_atom2_aux/ qed-.
+
+lemma lpx_inv_pair2: ∀h,g,I,G,L1,K2,V2.  ⦃G, L1⦄ ⊢ ➡[h, g] K2.ⓑ{I}V2 →
+                     ∃∃K1,V1. ⦃G, K1⦄ ⊢ ➡[h, g] K2 & ⦃G, K1⦄ ⊢ V1 ➡[h, g] V2 &
+                             L1 = K1. ⓑ{I} V1.
+/2 width=3 by lpx_sn_inv_pair2_aux/ qed-.
+
+lemma lpx_inv_pair: ∀h,g,I1,I2,G,L1,L2,V1,V2.  ⦃G, L1.ⓑ{I1}V1⦄ ⊢ ➡[h, g] L2.ⓑ{I2}V2 →
+                    ∧∧ ⦃G, L1⦄ ⊢ ➡[h, g] L2 & ⦃G, L1⦄ ⊢ V1 ➡[h, g] V2 & I1 = I2.
+/2 width=1 by lpx_sn_inv_pair/ qed-.
+
+(* Basic properties *********************************************************)
+
+lemma lpx_refl: ∀h,g,G,L.  ⦃G, L⦄ ⊢ ➡[h, g] L.
+/2 width=1 by lpx_sn_refl/ qed.
+
+lemma lpx_pair: ∀h,g,I,G,K1,K2,V1,V2. ⦃G, K1⦄ ⊢ ➡[h, g] K2 → ⦃G, K1⦄ ⊢ V1 ➡[h, g] V2 →
+                ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡[h, g] K2.ⓑ{I}V2.
+/2 width=1 by lpx_sn_pair/ qed.
+
+lemma lpr_lpx: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L1⦄ ⊢ ➡[h, g] L2.
+#h #g #G #L1 #L2 #H elim H -L1 -L2 /3 width=1 by lpx_pair, cpr_cpx/
+qed.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lpx_fwd_length: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → |L1| = |L2|.
+/2 width=2 by lpx_sn_fwd_length/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma
new file mode 100644
index 000000000..f9c2374c2
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma
@@ -0,0 +1,83 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/static/aaa_lift.ma".
+include "basic_2/static/lsuba_aaa.ma".
+include "basic_2/reduction/lpx_ldrop.ma".
+
+(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
+
+(* Properties on atomic arity assignment for terms **************************)
+
+(* Note: lemma 500 *)
+lemma aaa_cpx_lpx_conf: ∀h,g,G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A →
+                        ∀T2. ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2 →
+                        ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → ⦃G, L2⦄ ⊢ T2 ⁝ A.
+#h #g #G #L1 #T1 #A #H elim H -G -L1 -T1 -A
+[ #g #L1 #k #X #H
+  elim (cpx_inv_sort1 … H) -H // * //
+| #I #G #L1 #K1 #V1 #B #i #HLK1 #_ #IHV1 #X #H #L2 #HL12
+  elim (cpx_inv_lref1 … H) -H
+  [ #H destruct
+    elim (lpx_ldrop_conf … HLK1 … HL12) -L1 #X #H #HLK2
+    elim (lpx_inv_pair1 … H) -H
+    #K2 #V2 #HK12 #HV12 #H destruct /3 width=6 by aaa_lref/
+  | * #J #Y #Z #V2 #H #HV12 #HV2
+    lapply (ldrop_mono … H … HLK1) -H #H destruct
+    elim (lpx_ldrop_conf … HLK1 … HL12) -L1 #Z #H #HLK2
+    elim (lpx_inv_pair1 … H) -H #K2 #V0 #HK12 #_ #H destruct
+    /3 width=8 by aaa_lift, ldrop_fwd_drop2/
+  ]
+| #a #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12
+  elim (cpx_inv_abbr1 … H) -H *
+  [ #V2 #T2 #HV12 #HT12 #H destruct /4 width=2 by lpx_pair, aaa_abbr/
+  | #T2 #HT12 #HT2 #H destruct -IHV1
+    /4 width=8 by lpx_pair, aaa_inv_lift, ldrop_drop/
+  ]
+| #a #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12
+  elim (cpx_inv_abst1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
+  /4 width=1 by lpx_pair, aaa_abst/
+| #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12
+  elim (cpx_inv_appl1 … H) -H *
+  [ #V2 #T2 #HV12 #HT12 #H destruct /3 width=3 by aaa_appl/
+  | #b #V2 #W1 #W2 #U1 #U2 #HV12 #HW12 #HU12 #H1 #H2 destruct
+    lapply (IHV1 … HV12 … HL12) -IHV1 -HV12 #HV2
+    lapply (IHT1 (ⓛ{b}W2.U2) … HL12) -IHT1 /2 width=1 by cpx_bind/ -L1 #H
+    elim (aaa_inv_abst … H) -H #B0 #A0 #HW1 #HU2 #H destruct
+    /5 width=6 by lsuba_aaa_trans, lsuba_abbr, aaa_abbr, aaa_cast/
+  | #b #V #V2 #W1 #W2 #U1 #U2 #HV1 #HV2 #HW12 #HU12 #H1 #H2 destruct
+    lapply (aaa_lift G L2 … B … (L2.ⓓW2) … HV2) -HV2 /2 width=2 by ldrop_drop/ #HV2
+    lapply (IHT1 (ⓓ{b}W2.U2) … HL12) -IHT1 /2 width=1 by cpx_bind/ -L1 #H
+    elim (aaa_inv_abbr … H) -H /3 width=3 by aaa_abbr, aaa_appl/
+  ]
+| #G #L1 #V1 #T1 #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12
+  elim (cpx_inv_cast1 … H) -H
+  [ * #V2 #T2 #HV12 #HT12 #H destruct /3 width=1 by aaa_cast/
+  | -IHV1 /2 width=1 by/
+  | -IHT1 /2 width=1 by/
+  ]
+]
+qed-.
+
+lemma aaa_cpx_conf: ∀h,g,G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A → ∀T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → ⦃G, L⦄ ⊢ T2 ⁝ A.
+/2 width=7 by aaa_cpx_lpx_conf/ qed-.
+
+lemma aaa_lpx_conf: ∀h,g,G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → ⦃G, L2⦄ ⊢ T ⁝ A.
+/2 width=7 by aaa_cpx_lpx_conf/ qed-.
+
+lemma aaa_cpr_conf: ∀G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A → ∀T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ⦃G, L⦄ ⊢ T2 ⁝ A.
+/3 width=5 by aaa_cpx_conf, cpr_cpx/ qed-.
+
+lemma aaa_lpr_conf: ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T ⁝ A.
+/3 width=5 by aaa_lpx_conf, lpr_lpx/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma
new file mode 100644
index 000000000..e24b05283
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma
@@ -0,0 +1,78 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/relocation/lpx_sn_ldrop.ma".
+include "basic_2/reduction/cpx_lift.ma".
+include "basic_2/reduction/lpx.ma".
+
+(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
+
+(* Properies on local environment slicing ***********************************)
+
+lemma lpx_ldrop_conf: ∀h,g,G. dropable_sn (lpx h g G).
+/3 width=6 by lpx_sn_deliftable_dropable, cpx_inv_lift1/ qed-.
+
+lemma ldrop_lpx_trans: ∀h,g,G. dedropable_sn (lpx h g G).
+/3 width=10 by lpx_sn_liftable_dedropable, cpx_lift/ qed-.
+
+lemma lpx_ldrop_trans_O1: ∀h,g,G. dropable_dx (lpx h g G).
+/2 width=3 by lpx_sn_dropable/ qed-.
+
+(* Properties on supclosure *************************************************)
+
+lemma fqu_lpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
+                     ∀K2. ⦃G2, L2⦄ ⊢ ➡[h, g] K2 →
+                     ∃∃K1,T. ⦃G1, L1⦄ ⊢ ➡[h, g] K1 & ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃ ⦃G2, K2, T2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
+/3 width=5 by fqu_lref_O, fqu_pair_sn, fqu_flat_dx, lpx_pair, ex3_2_intro/
+[ #a #I #G2 #L2 #V2 #T2 #X #H elim (lpx_inv_pair1 … H) -H
+  #K2 #W2 #HLK2 #HVW2 #H destruct
+  /3 width=5 by fqu_fquq, cpx_pair_sn, fqu_bind_dx, ex3_2_intro/
+| #G #L1 #K1 #T1 #U1 #e #HLK1 #HTU1 #K2 #HK12
+  elim (ldrop_lpx_trans … HLK1 … HK12) -HK12
+  /3 width=7 by fqu_drop, ex3_2_intro/
+]
+qed-.
+
+lemma fquq_lpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
+                      ∀K2. ⦃G2, L2⦄ ⊢ ➡[h, g] K2 →
+                      ∃∃K1,T. ⦃G1, L1⦄ ⊢ ➡[h, g] K1 & ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K2 #HLK2 elim (fquq_inv_gen … H) -H
+[ #HT12 elim (fqu_lpx_trans … HT12 … HLK2) /3 width=5 by fqu_fquq, ex3_2_intro/
+| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/
+]
+qed-.
+
+lemma lpx_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
+                     ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 →
+                     ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
+/3 width=7 by fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, lpx_pair, ex3_2_intro/
+[ #I #G1 #L1 #V1 #X #H elim (lpx_inv_pair2 … H) -H
+  #K1 #W1 #HKL1 #HWV1 #H destruct elim (lift_total V1 0 1)
+  /4 width=7 by cpx_delta, fqu_drop, ldrop_drop, ex3_2_intro/
+| #G #L1 #K1 #T1 #U1 #e #HLK1 #HTU1 #L0 #HL01
+  elim (lpx_ldrop_trans_O1 … HL01 … HLK1) -L1
+  /3 width=5 by fqu_drop, ex3_2_intro/
+]
+qed-.
+
+lemma lpx_fquq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
+                      ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 →
+                      ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #HKL1 elim (fquq_inv_gen … H) -H
+[ #HT12 elim (lpx_fqu_trans … HT12 … HKL1) /3 width=5 by fqu_fquq, ex3_2_intro/
+| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma
new file mode 100644
index 000000000..d3f594317
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma
@@ -0,0 +1,87 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/substitution/lleq_ldrop.ma".
+include "basic_2/reduction/lpx_ldrop.ma".
+
+(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
+
+(* Properties on lazy equivalence for local environments ********************)
+
+axiom lleq_lpx_trans: ∀h,g,G,L2,K2. ⦃G, L2⦄ ⊢ ➡[h, g] K2 →
+                      ∀L1,T,d. L1 ⋕[T, d] L2 →
+                      ∃∃K1. ⦃G, L1⦄ ⊢ ➡[h, g] K1 & K1 ⋕[T, d] K2.
+
+lemma lpx_lleq_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
+                          ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1, 0] L1 →
+                          ∃∃K2. ⦃G1, K1, T1⦄ ⊃ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2, 0] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
+[ #I #G1 #L1 #V1 #X #H1 #H2 elim (lpx_inv_pair2 … H1) -H1
+  #K0 #V0 #H1KL1 #_ #H destruct
+  elim (lleq_inv_lref_ge_dx … H2 ? I L1 V1) -H2 //
+  #K1 #H #H2KL1 lapply (ldrop_inv_O2 … H) -H #H destruct
+  /2 width=4 by fqu_lref_O, ex3_intro/
+| * [ #a ] #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H
+  [ elim (lleq_inv_bind … H)
+  | elim (lleq_inv_flat … H)
+  ] -H /2 width=4 by fqu_pair_sn, ex3_intro/
+| #a #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_bind_O … H) -H
+  /3 width=4 by lpx_pair, fqu_bind_dx, ex3_intro/
+| #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_flat … H) -H
+  /2 width=4 by fqu_flat_dx, ex3_intro/
+| #G1 #L1 #L #T1 #U1 #e #HL1 #HTU1 #K1 #H1KL1 #H2KL1
+  elim (ldrop_O1_le (e+1) K1)
+  [ #K #HK1 lapply (lleq_inv_lift_le … H2KL1 … HK1 HL1 … HTU1 ?) -H2KL1 //
+    #H2KL elim (lpx_ldrop_trans_O1 … H1KL1 … HL1) -L1
+    #K0 #HK10 #H1KL lapply (ldrop_mono … HK10 … HK1) -HK10 #H destruct
+    /3 width=4 by fqu_drop, ex3_intro/
+  | lapply (ldrop_fwd_length_le2 … HL1) -L -T1 -g
+    lapply (lleq_fwd_length … H2KL1) //
+  ]
+]
+qed-.
+
+lemma lpx_lleq_fquq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
+                           ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1, 0] L1 →
+                           ∃∃K2. ⦃G1, K1, T1⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2, 0] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1
+elim (fquq_inv_gen … H) -H
+[ #H elim (lpx_lleq_fqu_trans … H … H1KL1 H2KL1) -L1
+  /3 width=4 by fqu_fquq, ex3_intro/
+| * #HG #HL #HT destruct /2 width=4 by ex3_intro/
+]
+qed-.
+
+lemma lpx_lleq_fqup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ →
+                           ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1, 0] L1 →
+                           ∃∃K2. ⦃G1, K1, T1⦄ ⊃+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2, 0] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
+[ #G2 #L2 #T2 #H #K1 #H1KL1 #H2KL1 elim (lpx_lleq_fqu_trans … H … H1KL1 H2KL1) -L1
+  /3 width=4 by fqu_fqup, ex3_intro/
+| #G #G2 #L #L2 #T #T2 #_ #HT2 #IHT1 #K1 #H1KL1 #H2KL1 elim (IHT1 … H2KL1) // -L1
+  #K #HT1 #H1KL #H2KL elim (lpx_lleq_fqu_trans … HT2 … H1KL H2KL) -L
+  /3 width=5 by fqup_strap1, ex3_intro/
+]
+qed-.
+
+lemma lpx_lleq_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
+                           ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1, 0] L1 →
+                           ∃∃K2. ⦃G1, K1, T1⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2, 0] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1
+elim (fqus_inv_gen … H) -H
+[ #H elim (lpx_lleq_fqup_trans … H … H1KL1 H2KL1) -L1
+  /3 width=4 by fqup_fqus, ex3_intro/
+| * #HG #HL #HT destruct /2 width=4 by ex3_intro/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/llor.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/llor.ma
index 7dec554c7..a2f332a69 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/llor.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/llor.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ground_2/xoa/xoa2.ma".
 include "basic_2/notation/relations/lazyor_4.ma".
 include "basic_2/relocation/lpx_sn_alt.ma".
 
@@ -56,45 +57,84 @@ qed-.
 
 (* Alternative definition ***************************************************)
 
-lemma llor_intro_alt_eq: ∀T,L2,L1,L. |L1| = |L2| → |L1| = |L| →
-                         (∀I1,I,K1,K,V1,V,U,i. ⇧[i, 1] U ≡ T →
-                            ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L ≡ K.ⓑ{I}V →
-                            ∧∧ I1 = I & V1 = V & K1 ⩖[T] L2 ≡ K
-                         ) →
-                         (∀I1,I2,I,K1,K2,K,V1,V2,V,i. (∀U. ⇧[i, 1] U ≡ T → ⊥) →
-                            ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
-                            ⇩[i] L ≡ K.ⓑ{I}V → ∧∧ I1 = I & V2 = V & K1 ⩖[T] L2 ≡ K
-                         ) → L1 ⩖[T] L2 ≡ L.
-#T #L2 #L1 #L #HL12 #HL1 #IH1 #IH2 @lpx_sn_intro_alt // -HL1
+(* Note: uses minus_minus_comm, minus_plus_m_m, commutative_plus, plus_minus *)
+lemma plus_minus_minus_be: ∀x,y,z. y ≤ z → z ≤ x → (x - z) + (z - y) = x - y.
+#x #z #y #Hzy #Hyx >plus_minus // >commutative_plus >plus_minus //
+qed-.
+
+fact plus_minus_minus_be_aux: ∀i,x,y,z. y ≤ z → z ≤ x → i = z - y → x - z + i = x - y.
+/2 width=1 by plus_minus_minus_be/ qed-.
+
+lemma llor_intro_alt: ∀T,L2,L1,L. |L1| ≤ |L2| → |L1| = |L| →
+                      (∀I1,I,K1,K,V1,V,i. ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L ≡ K.ⓑ{I}V →
+                         (∀U. ⇧[|L2|-|L1|+i, 1] U ≡ T →
+                              ∧∧ I1 = I & V1 = V & K1 ⩖[T] L2 ≡ K
+                         ) ∧
+                         (∀I2,K2,V2. (∀U. ⇧[|L2|-|L1|+i, 1] U ≡ T → ⊥) →
+                                     ⇩[|L2|-|L1|+i] L2 ≡ K2.ⓑ{I2}V2 →
+                                     ∧∧ I1 = I & V2 = V & K1 ⩖[T] L2 ≡ K
+                         )
+                      ) → L1 ⩖[T] L2 ≡ L.
+#T #L2 #L1 #L #HL12 #HL1 #IH @lpx_sn_intro_alt // -HL1
 #I1 #I #K1 #K #V1 #V #i #HLK1 #HLK
 lapply (ldrop_fwd_length_minus4 … HLK1)
 lapply (ldrop_fwd_length_le4 … HLK1)
-normalize >HL12 <minus_plus #HKL1 #Hi elim (is_lift_dec T i 1) -HL12
-[ * #U #HUT elim (IH1 … HUT HLK1 HLK) -IH1 -HLK1 -HLK #H1 #H2 #HT destruct
+normalize #HKL1 #H1i lapply (plus_minus_minus_be_aux … HL12 H1i) // #H2i
+lapply (transitive_le … HKL1 HL12) -HKL1 -HL12 #HKL1
+elim (IH … HLK1 HLK) -IH -HLK1 -HLK #IH1 #IH2
+elim (is_lift_dec T (|L2|-|L1|+i) 1)
+[ -IH2 * #U #HUT elim (IH1 … HUT) -IH1
   /3 width=2 by clor_sn, and3_intro/
-| #H elim (ldrop_O1_lt L2 i) destruct /2 width=1 by monotonic_lt_minus_l/
-  #I2 #K2 #V2 #HLK2 elim (IH2 … HLK1 HLK2 HLK) -HLK1 -HLK
+| -IH1 #H elim (ldrop_O1_lt L2 (|L2|-|L1|+i)) /2 width=1 by monotonic_lt_minus_l/
+  #I2 #K2 #V2 #HLK2 elim (IH2 … HLK2) -IH2
   /5 width=3 by clor_dx, ex_intro, and3_intro/
 ]
 qed.
 
-lemma llor_inv_gen_eq: ∀T,L2,L1,L. L1 ⩖[T] L2 ≡ L → |L1| = |L2| →
-                       |L1| = |L| ∧
-                       (∀I1,I,K1,K,V1,V,i.
+lemma llor_ind_alt: ∀T,L2. ∀S:relation lenv. (
+                       ∀L1,L. |L1| = |L| → (
+                          ∀I1,I,K1,K,V1,V,i.
                           ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L ≡ K.ⓑ{I}V →
-                          (∃∃U. ⇧[i, 1] U ≡ T &
-                                I1 = I & V1 = V & K1 ⩖[T] L2 ≡ K
+                          (∃∃U. ⇧[|L2|-|L1|+i, 1] U ≡ T &
+                                I1 = I & V1 = V & K1 ⩖[T] L2 ≡ K & S K1 K
                           ) ∨
-                          (∃∃I2,K2,V2. (∀U. ⇧[i, 1] U ≡ T → ⊥) &
-                                       ⇩[i] L2 ≡ K2.ⓑ{I2}V2 &
-                                       I1 = I & V2 = V & K1 ⩖[T] L2 ≡ K
+                          (∃∃I2,K2,V2. (∀U. ⇧[|L2|-|L1|+i, 1] U ≡ T → ⊥) &
+                                       ⇩[|L2|-|L1|+i] L2 ≡ K2.ⓑ{I2}V2 &
+                                       I1 = I & V2 = V & K1 ⩖[T] L2 ≡ K & S K1 K
                           )
-                       ).
-#T #L2 #L1 #L #H #HL12 elim (lpx_sn_inv_gen … H) -H
-#HL1 #IH @conj //
+                       ) → |L1| ≤ |L2| → S L1 L
+                    ) →
+                    ∀L1,L. L1 ⩖[T] L2 ≡ L → |L1| ≤ |L2| → S L1 L.
+#T #L2 #S #IH1 #L1 #L #H @(lpx_sn_ind_alt … H) -L1 -L
+#L1 #L #HL1 #IH2 #HL12 @IH1 // -IH1 -HL1
+#I1 #I #K1 #K #V1 #V #i #HLK1 #HLK
+lapply (ldrop_fwd_length_minus4 … HLK1)
+lapply (ldrop_fwd_length_le4 … HLK1)
+normalize #HKL1 #H1i lapply (plus_minus_minus_be_aux … HL12 H1i) //
+lapply (transitive_le … HKL1 HL12) -HKL1 -HL12
+elim (IH2 … HLK1 HLK) -IH2 #H *
+/5 width=5 by lt_to_le, ex6_3_intro, ex5_intro, or_intror, or_introl/
+qed-.
+
+lemma llor_inv_alt: ∀T,L2,L1,L. L1 ⩖[T] L2 ≡ L → |L1| ≤ |L2| →
+                    |L1| = |L| ∧
+                    (∀I1,I,K1,K,V1,V,i.
+                       ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L ≡ K.ⓑ{I}V →
+                       (∃∃U. ⇧[|L2|-|L1|+i, 1] U ≡ T &
+                             I1 = I & V1 = V & K1 ⩖[T] L2 ≡ K
+                       ) ∨
+                       (∃∃I2,K2,V2. (∀U. ⇧[|L2|-|L1|+i, 1] U ≡ T → ⊥) &
+                                    ⇩[|L2|-|L1|+i] L2 ≡ K2.ⓑ{I2}V2 &
+                                    I1 = I & V2 = V & K1 ⩖[T] L2 ≡ K
+                       )
+                    ).
+#T #L2 #L1 #L #H #HL12 elim (lpx_sn_inv_alt … H) -H
+#HL1 #IH @conj // -HL1
 #I1 #I #K1 #K #V1 #V #i #HLK1 #HLK
 lapply (ldrop_fwd_length_minus4 … HLK1)
 lapply (ldrop_fwd_length_le4 … HLK1)
-normalize >HL12 <minus_plus #HKL1 #Hi elim (IH … HLK1 HLK) -IH #H *
+normalize #HKL1 #H1i lapply (plus_minus_minus_be_aux … HL12 H1i) //
+lapply (transitive_le … HKL1 HL12) -HKL1 -HL12
+elim (IH … HLK1 HLK) -IH #H *
 /4 width=5 by ex5_3_intro, ex4_intro, or_intror, or_introl/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_alt.ma
index 1da11d013..bc8528408 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_alt.ma
@@ -18,7 +18,7 @@ include "basic_2/relocation/llpx_sn.ma".
 
 (* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****)
 
-(* alternative definition of llpx_sn_alt *)
+(* alternative definition of llpx_sn *)
 inductive llpx_sn_alt (R:relation3 lenv term term): relation4 ynat term lenv lenv ≝
 | llpx_sn_alt_intro: ∀L1,L2,T,d.
                      (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
@@ -29,40 +29,64 @@ inductive llpx_sn_alt (R:relation3 lenv term term): relation4 ynat term lenv len
                      ) → |L1| = |L2| → llpx_sn_alt R d T L1 L2
 .
 
-(* Basic inversion lemmas ****************************************************)
+(* Compact definition of llpx_sn_alt ****************************************)
 
-lemma llpx_sn_alt_inv_gen: ∀R,L1,L2,T,d. llpx_sn_alt R d T L1 L2 →
+lemma llpx_sn_alt_intro_alt: ∀R,L1,L2,T,d. |L1| = |L2| →
+                             (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
+                                ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
+                                ∧∧ I1 = I2 & R K1 V1 V2 & llpx_sn_alt R 0 V1 K1 K2
+                             ) → llpx_sn_alt R d T L1 L2.
+#R #L1 #L2 #T #d #HL12 #IH @llpx_sn_alt_intro // -HL12
+#I1 #I2 #K1 #K2 #V1 #V2 #i #Hid #HnT #HLK1 #HLK2
+elim (IH … HnT HLK1 HLK2) -IH -HnT -HLK1 -HLK2 /2 width=1 by conj/
+qed.
+
+lemma llpx_sn_alt_ind_alt: ∀R. ∀S:relation4 ynat term lenv lenv.
+                           (∀L1,L2,T,d. |L1| = |L2| → (
+                              ∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
+                              ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
+                              ∧∧ I1 = I2 & R K1 V1 V2 & llpx_sn_alt R 0 V1 K1 K2 & S 0 V1 K1 K2
+                           ) → S d T L1 L2) →
+                           ∀L1,L2,T,d. llpx_sn_alt R d T L1 L2 → S d T L1 L2.
+#R #S #IH #L1 #L2 #T #d #H elim H -L1 -L2 -T -d
+#L1 #L2 #T #d #H1 #H2 #HL12 #IH2 @IH -IH // -HL12
+#I1 #I2 #K1 #K2 #V1 #V2 #i #Hid #HnT #HLK1 #HLK2
+elim (H1 … HnT HLK1 HLK2) -H1 /4 width=8 by and4_intro/
+qed-.
+
+lemma llpx_sn_alt_inv_alt: ∀R,L1,L2,T,d. llpx_sn_alt R d T L1 L2 →
                            |L1| = |L2| ∧
                            ∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
                            ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
                            ∧∧ I1 = I2 & R K1 V1 V2 & llpx_sn_alt R 0 V1 K1 K2.
-#R #L1 #L2 #T #d * -L1 -L2 -T -d
-#L1 #L2 #T #d #IH1 #IH2 #HL12 @conj //
-#I1 #I2 #K1 #K2 #HLK1 #HLK2 #i #Hid #HnT #HLK1 #HLK2
-elim (IH1 … HnT HLK1 HLK2) -IH1 /4 width=8 by and3_intro/
+#R #L1 #L2 #T #d #H @(llpx_sn_alt_ind_alt … H) -L1 -L2 -T -d
+#L1 #L2 #T #d #HL12 #IH @conj // -HL12
+#I1 #I2 #K1 #K2 #V1 #V2 #i #Hid #HnT #HLK1 #HLK2
+elim (IH … HnT HLK1 HLK2) -IH -HnT -HLK1 -HLK2 /2 width=1 by and3_intro/
 qed-.
 
+(* Basic inversion lemmas ***************************************************)
+
 lemma llpx_sn_alt_inv_flat: ∀R,I,L1,L2,V,T,d. llpx_sn_alt R d (ⓕ{I}V.T) L1 L2 →
                             llpx_sn_alt R d V L1 L2 ∧ llpx_sn_alt R d T L1 L2.
-#R #I #L1 #L2 #V #T #d #H elim (llpx_sn_alt_inv_gen … H) -H
-#HL12 #IH @conj @llpx_sn_alt_intro // -HL12
+#R #I #L1 #L2 #V #T #d #H elim (llpx_sn_alt_inv_alt … H) -H
+#HL12 #IH @conj @llpx_sn_alt_intro_alt // -HL12
 #I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #H #HLK1 #HLK2
-elim (IH … HLK1 HLK2) -IH -HLK1 -HLK2
-/3 width=8 by nlift_flat_sn, nlift_flat_dx, conj/
+elim (IH … HLK1 HLK2) -IH -HLK1 -HLK2 //
+/3 width=8 by nlift_flat_sn, nlift_flat_dx, and3_intro/
 qed-.
 
 lemma llpx_sn_alt_inv_bind: ∀R,a,I,L1,L2,V,T,d. llpx_sn_alt R d (ⓑ{a,I}V.T) L1 L2 →
                             llpx_sn_alt R d V L1 L2 ∧ llpx_sn_alt R (⫯d) T (L1.ⓑ{I}V) (L2.ⓑ{I}V).
-#R #a #I #L1 #L2 #V #T #d #H elim (llpx_sn_alt_inv_gen … H) -H
-#HL12 #IH @conj @llpx_sn_alt_intro [3,6: normalize // ] -HL12
+#R #a #I #L1 #L2 #V #T #d #H elim (llpx_sn_alt_inv_alt … H) -H
+#HL12 #IH @conj @llpx_sn_alt_intro_alt [1,3: normalize // ] -HL12
 #I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #H #HLK1 #HLK2
-[1,2: elim (IH … HLK1 HLK2) -IH -HLK1 -HLK2
-  /3 width=9 by nlift_bind_sn, conj/
-|3,4: lapply (yle_inv_succ1 … Hdi) -Hdi * #Hdi #Hi
+[ elim (IH … HLK1 HLK2) -IH -HLK1 -HLK2
+  /3 width=9 by nlift_bind_sn, and3_intro/
+| lapply (yle_inv_succ1 … Hdi) -Hdi * #Hdi #Hi
   lapply (ldrop_inv_drop1_lt … HLK1 ?) -HLK1 /2 width=1 by ylt_O/ #HLK1
   lapply (ldrop_inv_drop1_lt … HLK2 ?) -HLK2 /2 width=1 by ylt_O/ #HLK2
-  elim (IH … HLK1 HLK2) -IH -HLK1 -HLK2
-  [1,3,4,6: /2 width=1 by conj/ ]
+  elim (IH … HLK1 HLK2) -IH -HLK1 -HLK2 /2 width=1 by and3_intro/
   @nlift_bind_dx <plus_minus_m_m /2 width=2 by ylt_O/
 ]
 qed-.
@@ -70,7 +94,7 @@ qed-.
 (* Basic forward lemmas ******************************************************)
 
 lemma llpx_sn_alt_fwd_length: ∀R,L1,L2,T,d. llpx_sn_alt R d T L1 L2 → |L1| = |L2|.
-#R #L1 #L2 #T #d * -L1 -L2 -T -d //
+#R #L1 #L2 #T #d #H elim (llpx_sn_alt_inv_alt … H) -H //
 qed-.
 
 lemma llpx_sn_alt_fwd_lref: ∀R,L1,L2,d,i. llpx_sn_alt R d (#i) L1 L2 →
@@ -80,7 +104,7 @@ lemma llpx_sn_alt_fwd_lref: ∀R,L1,L2,d,i. llpx_sn_alt R d (#i) L1 L2 →
                                                 ⇩[i] L2 ≡ K2.ⓑ{I}V2 &
                                                 llpx_sn_alt R (yinj 0) V1 K1 K2 &
                                                 R K1 V1 V2 & d ≤ yinj i.
-#R #L1 #L2 #d #i #H elim (llpx_sn_alt_inv_gen … H) -H
+#R #L1 #L2 #d #i #H elim (llpx_sn_alt_inv_alt … H) -H
 #HL12 #IH elim (lt_or_ge i (|L1|)) /3 width=1 by or3_intro0, conj/
 elim (ylt_split i d) /3 width=1 by or3_intro1/
 #Hdi #HL1 elim (ldrop_O1_lt … HL1)
@@ -91,16 +115,6 @@ qed-.
 
 (* Basic properties **********************************************************)
 
-lemma llpx_sn_alt_intro_alt: ∀R,L1,L2,T,d. |L1| = |L2| →
-                             (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
-                                ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
-                                ∧∧ I1 = I2 & R K1 V1 V2 & llpx_sn_alt R 0 V1 K1 K2
-                             ) → llpx_sn_alt R d T L1 L2.
-#R #L1 #L2 #T #d #HL12 #IH @llpx_sn_alt_intro // -HL12
-#I1 #I2 #K1 #K2 #V1 #V2 #i #Hid #HnT #HLK1 #HLK2
-elim (IH … HnT HLK1 HLK2) -IH -HnT -HLK1 -HLK2 /2 width=1 by conj/
-qed.
-
 lemma llpx_sn_alt_sort: ∀R,L1,L2,d,k. |L1| = |L2| → llpx_sn_alt R d (⋆k) L1 L2.
 #R #L1 #L2 #d #k #HL12 @llpx_sn_alt_intro_alt // -HL12
 #I1 #I2 #K1 #K2 #V1 #V2 #i #_ #H elim (H (⋆k)) //
@@ -146,8 +160,8 @@ lemma llpx_sn_alt_flat: ∀R,I,L1,L2,V,T,d.
                         llpx_sn_alt R d V L1 L2 → llpx_sn_alt R d T L1 L2 →
                         llpx_sn_alt R d (ⓕ{I}V.T) L1 L2.
 #R #I #L1 #L2 #V #T #d #HV #HT
-elim (llpx_sn_alt_inv_gen … HV) -HV #HL12 #IHV
-elim (llpx_sn_alt_inv_gen … HT) -HT #_ #IHT
+elim (llpx_sn_alt_inv_alt … HV) -HV #HL12 #IHV
+elim (llpx_sn_alt_inv_alt … HT) -HT #_ #IHT
 @llpx_sn_alt_intro_alt // -HL12
 #I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #HnVT #HLK1 #HLK2
 elim (nlift_inv_flat … HnVT) -HnVT #H
@@ -161,8 +175,8 @@ lemma llpx_sn_alt_bind: ∀R,a,I,L1,L2,V,T,d.
                         llpx_sn_alt R (⫯d) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) →
                         llpx_sn_alt R d (ⓑ{a,I}V.T) L1 L2.
 #R #a #I #L1 #L2 #V #T #d #HV #HT
-elim (llpx_sn_alt_inv_gen … HV) -HV #HL12 #IHV
-elim (llpx_sn_alt_inv_gen … HT) -HT #_ #IHT
+elim (llpx_sn_alt_inv_alt … HV) -HV #HL12 #IHV
+elim (llpx_sn_alt_inv_alt … HT) -HT #_ #IHT
 @llpx_sn_alt_intro_alt // -HL12
 #I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #HnVT #HLK1 #HLK2
 elim (nlift_inv_bind … HnVT) -HnVT #H
@@ -196,7 +210,7 @@ theorem llpx_sn_alt_inv_lpx_sn: ∀R,T,L1,L2,d. llpx_sn_alt R d T L1 L2 → llpx
 ]
 qed-.
 
-(* Advanced properties ******************************************************)
+(* Alternative definition of llpx_sn ****************************************)
 
 lemma llpx_sn_intro_alt: ∀R,L1,L2,T,d. |L1| = |L2| →
                          (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
@@ -209,15 +223,27 @@ lemma llpx_sn_intro_alt: ∀R,L1,L2,T,d. |L1| = |L2| →
 elim (IH … HnT HLK1 HLK2) -IH -HnT -HLK1 -HLK2 /3 width=1 by llpx_sn_lpx_sn_alt, and3_intro/
 qed.
 
-(* Advanced inversion lemmas ************************************************)
+lemma llpx_sn_ind_alt: ∀R. ∀S:relation4 ynat term lenv lenv.
+                       (∀L1,L2,T,d. |L1| = |L2| → (
+                          ∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
+                          ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
+                          ∧∧ I1 = I2 & R K1 V1 V2 & llpx_sn R 0 V1 K1 K2 & S 0 V1 K1 K2
+                       ) → S d T L1 L2) →
+                       ∀L1,L2,T,d. llpx_sn R d T L1 L2 → S d T L1 L2.
+#R #S #IH1 #L1 #L2 #T #d #H lapply (llpx_sn_lpx_sn_alt … H) -H
+#H @(llpx_sn_alt_ind_alt … H) -L1 -L2 -T -d
+#L1 #L2 #T #d #HL12 #IH2 @IH1 -IH1 // -HL12
+#I1 #I2 #K1 #K2 #V1 #V2 #i #Hid #HnT #HLK1 #HLK2
+elim (IH2 … HnT HLK1 HLK2) -IH2 -HnT -HLK1 -HLK2 /3 width=1 by llpx_sn_alt_inv_lpx_sn, and4_intro/
+qed-.
 
-lemma llpx_sn_inv_gen: ∀R,L1,L2,T,d. llpx_sn R d T L1 L2 →
+lemma llpx_sn_inv_alt: ∀R,L1,L2,T,d. llpx_sn R d T L1 L2 →
                        |L1| = |L2| ∧
                        ∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
                        ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
                        ∧∧ I1 = I2 & R K1 V1 V2 & llpx_sn R 0 V1 K1 K2.
 #R #L1 #L2 #T #d #H lapply (llpx_sn_lpx_sn_alt … H) -H
-#H elim (llpx_sn_alt_inv_gen … H) -H
+#H elim (llpx_sn_alt_inv_alt … H) -H
 #HL12 #IH @conj //
 #I1 #I2 #K1 #K2 #V1 #V2 #i #Hid #HnT #HLK1 #HLK2
 elim (IH … HnT HLK1 HLK2) -IH -HnT -HLK1 -HLK2 /3 width=1 by llpx_sn_alt_inv_lpx_sn, and3_intro/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn_alt.ma
index c9c381a32..1fb1858b5 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn_alt.ma
@@ -17,7 +17,7 @@ include "basic_2/relocation/lpx_sn.ma".
 
 (* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********)
 
-(* alternative definition of lpx_sn_alt *)
+(* alternative definition of lpx_sn *)
 inductive lpx_sn_alt (R:relation3 lenv term term): relation lenv ≝
 | lpx_sn_alt_intro: ∀L1,L2.
                     (∀I1,I2,K1,K2,V1,V2,i.
@@ -28,25 +28,50 @@ inductive lpx_sn_alt (R:relation3 lenv term term): relation lenv ≝
                     ) → |L1| = |L2| → lpx_sn_alt R L1 L2
 .
 
-(* Basic forward lemmas ******************************************************)
-
-lemma lpx_sn_alt_fwd_length: ∀R,L1,L2. lpx_sn_alt R L1 L2 → |L1| = |L2|.
-#R #L1 #L2 * -L1 -L2 //
+(* compact definition of lpx_sn_alt *****************************************)
+
+lemma lpx_sn_alt_ind_alt: ∀R. ∀S:relation lenv.
+                          (∀L1,L2. |L1| = |L2| → (
+                             ∀I1,I2,K1,K2,V1,V2,i.
+                             ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
+                             ∧∧ I1 = I2 & R K1 V1 V2 & lpx_sn_alt R K1 K2 & S K1 K2
+                          ) → S L1 L2) →
+                          ∀L1,L2. lpx_sn_alt R L1 L2 → S L1 L2.
+#R #S #IH #L1 #L2 #H elim H -L1 -L2
+#L1 #L2 #H1 #H2 #HL12 #IH2 @IH -IH // -HL12
+#I1 #I2 #K1 #K2 #V1 #V2 #i #HLK1 #HLK2 elim (H1 … HLK1 HLK2) -H1
+/3 width=7 by and4_intro/
 qed-.
 
-(* Basic inversion lemmas ***************************************************)
-
-lemma lpx_sn_alt_inv_gen: ∀R,L1,L2. lpx_sn_alt R L1 L2 →
+lemma lpx_sn_alt_inv_alt: ∀R,L1,L2. lpx_sn_alt R L1 L2 →
                           |L1| = |L2| ∧
                           ∀I1,I2,K1,K2,V1,V2,i.
                           ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
                           ∧∧ I1 = I2 & R K1 V1 V2 & lpx_sn_alt R K1 K2.
-#R #L1 #L2 * -L1 -L2
-#L1 #L2 #IH1 #IH2 #HL12 @conj //
-#I1 #I2 #K1 #K2 #HLK1 #HLK2 #i #HLK1 #HLK2
-elim (IH1 … HLK1 HLK2) -IH1 /3 width=7 by and3_intro/
+#R #L1 #L2 #H @(lpx_sn_alt_ind_alt … H) -L1 -L2
+#L1 #L2 #HL12 #IH @conj // -HL12
+#I1 #I2 #K1 #K2 #V1 #V2 #i #HLK1 #HLK2 elim (IH … HLK1 HLK2) -IH -HLK1 -HLK2
+/2 width=1 by and3_intro/
 qed-.
 
+lemma lpx_sn_alt_intro_alt: ∀R,L1,L2. |L1| = |L2| →
+                            (∀I1,I2,K1,K2,V1,V2,i.
+                               ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
+                               ∧∧ I1 = I2 & R K1 V1 V2 & lpx_sn_alt R K1 K2
+                            ) → lpx_sn_alt R L1 L2.
+#R #L1 #L2 #HL12 #IH @lpx_sn_alt_intro // -HL12
+#I1 #I2 #K1 #K2 #V1 #V2 #i #HLK1 #HLK2
+elim (IH … HLK1 HLK2) -IH -HLK1 -HLK2 /2 width=1 by conj/
+qed.
+
+(* Basic forward lemmas ******************************************************)
+
+lemma lpx_sn_alt_fwd_length: ∀R,L1,L2. lpx_sn_alt R L1 L2 → |L1| = |L2|.
+#R #L1 #L2 #H elim (lpx_sn_alt_inv_alt … H) //
+qed-.
+
+(* Basic inversion lemmas ***************************************************)
+
 lemma lpx_sn_alt_inv_atom1: ∀R,L2. lpx_sn_alt R (⋆) L2 → L2 = ⋆.
 #R #L2 #H lapply (lpx_sn_alt_fwd_length … H) -H
 normalize /2 width=1 by length_inv_zero_sn/
@@ -54,7 +79,7 @@ qed-.
 
 lemma lpx_sn_alt_inv_pair1: ∀R,I,L2,K1,V1. lpx_sn_alt R (K1.ⓑ{I}V1) L2 →
                             ∃∃K2,V2. lpx_sn_alt R K1 K2 & R K1 V1 V2 & L2 = K2.ⓑ{I}V2.
-#R #I1 #L2 #K1 #V1 #H elim (lpx_sn_alt_inv_gen … H) -H
+#R #I1 #L2 #K1 #V1 #H elim (lpx_sn_alt_inv_alt … H) -H
 #H #IH elim (length_inv_pos_sn … H) -H
 #I2 #K2 #V2 #HK12 #H destruct
 elim (IH I1 I2 K1 K2 V1 V2 0) -IH /2 width=5 by ex3_2_intro/
@@ -67,7 +92,7 @@ qed-.
 
 lemma lpx_sn_alt_inv_pair2: ∀R,I,L1,K2,V2. lpx_sn_alt R L1 (K2.ⓑ{I}V2) →
                             ∃∃K1,V1. lpx_sn_alt R K1 K2 & R K1 V1 V2 & L1 = K1.ⓑ{I}V1.
-#R #I2 #L1 #K2 #V2 #H elim (lpx_sn_alt_inv_gen … H) -H
+#R #I2 #L1 #K2 #V2 #H elim (lpx_sn_alt_inv_alt … H) -H
 #H #IH elim (length_inv_pos_dx … H) -H
 #I1 #K1 #V1 #HK12 #H destruct
 elim (IH I1 I2 K1 K2 V1 V2 0) -IH /2 width=5 by ex3_2_intro/
@@ -75,16 +100,6 @@ qed-.
 
 (* Basic properties *********************************************************)
 
-lemma lpx_sn_alt_intro_alt: ∀R,L1,L2. |L1| = |L2| →
-                            (∀I1,I2,K1,K2,V1,V2,i.
-                               ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
-                               ∧∧ I1 = I2 & R K1 V1 V2 & lpx_sn_alt R K1 K2
-                            ) → lpx_sn_alt R L1 L2.
-#R #L1 #L2 #HL12 #IH @lpx_sn_alt_intro // -HL12
-#I1 #I2 #K1 #K2 #V1 #V2 #i #HLK1 #HLK2
-elim (IH … HLK1 HLK2) -IH -HLK1 -HLK2 /2 width=1 by conj/
-qed.
-
 lemma lpx_sn_alt_atom: ∀R. lpx_sn_alt R (⋆) (⋆).
 #R @lpx_sn_alt_intro_alt //
 #I1 #I2 #K1 #K2 #V1 #V2 #i #HLK1 elim (ldrop_inv_atom1 … HLK1) -HLK1
@@ -94,7 +109,7 @@ qed.
 lemma lpx_sn_alt_pair: ∀R,I,L1,L2,V1,V2.
                        lpx_sn_alt R L1 L2 → R L1 V1 V2 →
                        lpx_sn_alt R (L1.ⓑ{I}V1) (L2.ⓑ{I}V2).
-#R #I #L1 #L2 #V1 #V2 #H #HV12 elim (lpx_sn_alt_inv_gen … H) -H
+#R #I #L1 #L2 #V1 #V2 #H #HV12 elim (lpx_sn_alt_inv_alt … H) -H
 #HL12 #IH @lpx_sn_alt_intro_alt normalize //
 #I1 #I2 #K1 #K2 #W1 #W2 #i @(nat_ind_plus … i) -i
 [ #HLK1 #HLK2
@@ -122,7 +137,7 @@ theorem lpx_sn_alt_inv_lpx_sn: ∀R,L1,L2. lpx_sn_alt R L1 L2 → lpx_sn R L1 L2
 ]
 qed-.
 
-(* Advanced properties ******************************************************)
+(* alternative definition of lpx_sn *****************************************)
 
 lemma lpx_sn_intro_alt: ∀R,L1,L2. |L1| = |L2| →
                         (∀I1,I2,K1,K2,V1,V2,i.
@@ -135,15 +150,27 @@ lemma lpx_sn_intro_alt: ∀R,L1,L2. |L1| = |L2| →
 elim (IH … HLK1 HLK2) -IH -HLK1 -HLK2 /3 width=1 by lpx_sn_lpx_sn_alt, and3_intro/
 qed.
 
-(* Advanced inversion lemmas ************************************************)
+lemma lpx_sn_ind_alt: ∀R. ∀S:relation lenv.
+                      (∀L1,L2. |L1| = |L2| → (
+                         ∀I1,I2,K1,K2,V1,V2,i.
+                         ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
+                         ∧∧ I1 = I2 & R K1 V1 V2 & lpx_sn R K1 K2 & S K1 K2
+                      ) → S L1 L2) →
+                      ∀L1,L2. lpx_sn R L1 L2 → S L1 L2.
+#R #S #IH1 #L1 #L2 #H lapply (lpx_sn_lpx_sn_alt … H) -H
+#H @(lpx_sn_alt_ind_alt … H) -L1 -L2
+#L1 #L2 #HL12 #IH2 @IH1 -IH1 // -HL12
+#I1 #I2 #K1 #K2 #V1 #V2 #i #HLK1 #HLK2 elim (IH2 … HLK1 HLK2) -IH2 -HLK1 -HLK2
+/3 width=1 by lpx_sn_alt_inv_lpx_sn, and4_intro/
+qed-.
 
-lemma lpx_sn_inv_gen: ∀R,L1,L2. lpx_sn R L1 L2 →
+lemma lpx_sn_inv_alt: ∀R,L1,L2. lpx_sn R L1 L2 →
                       |L1| = |L2| ∧
                       ∀I1,I2,K1,K2,V1,V2,i.
                       ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
                       ∧∧ I1 = I2 & R K1 V1 V2 & lpx_sn R K1 K2.
 #R #L1 #L2 #H lapply (lpx_sn_lpx_sn_alt … H) -H
-#H elim (lpx_sn_alt_inv_gen … H) -H
+#H elim (lpx_sn_alt_inv_alt … H) -H
 #HL12 #IH @conj //
 #I1 #I2 #K1 #K2 #V1 #V2 #i #HLK1 #HLK2
 elim (IH … HLK1 HLK2) -IH -HLK1 -HLK2 /3 width=1 by lpx_sn_alt_inv_lpx_sn, and3_intro/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma
index 470fa107f..dd97ea641 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma
@@ -29,12 +29,25 @@ theorem lleq_intro_alt: ∀L1,L2,T,d. |L1| = |L2| →
 elim (IH … HnT HLK1 HLK2) -IH -HnT -HLK1 -HLK2 /2 width=1 by and3_intro/
 qed.
 
-theorem lleq_inv_gen: ∀L1,L2,T,d. L1 ⋕[T, d] L2 →
+theorem lleq_ind_alt: ∀S:relation4 ynat term lenv lenv.
+                      (∀L1,L2,T,d. |L1| = |L2| → (
+                         ∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
+                         ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
+                         ∧∧ I1 = I2 & V1 = V2 & K1 ⋕[V1, 0] K2 & S 0 V1 K1 K2
+                      ) → S d T L1 L2) →
+                      ∀L1,L2,T,d. L1 ⋕[T, d] L2 → S d T L1 L2.
+#S #IH1 #L1 #L2 #T #d #H @(llpx_sn_ind_alt … H) -L1 -L2 -T -d
+#L1 #L2 #T #d #HL12 #IH2 @IH1 -IH1 // -HL12
+#I1 #I2 #K1 #K2 #V1 #V2 #i #Hid #HnT #HLK1 #HLK2
+elim (IH2 … HnT HLK1 HLK2) -IH2 -HnT -HLK1 -HLK2 /2 width=1 by and4_intro/
+qed-.
+
+theorem lleq_inv_alt: ∀L1,L2,T,d. L1 ⋕[T, d] L2 →
                       |L1| = |L2| ∧
                       ∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
                       ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
                       ∧∧ I1 = I2 & V1 = V2 & K1 ⋕[V1, 0] K2.
-#L1 #L2 #T #d #H elim (llpx_sn_inv_gen … H) -H
+#L1 #L2 #T #d #H elim (llpx_sn_inv_alt … H) -H
 #HL12 #IH @conj //
 #I1 #I2 #K1 #K2 #V1 #V2 #i #Hid #HnT #HLK1 #HLK2
 elim (IH … HnT HLK1 HLK2) -IH -HnT -HLK1 -HLK2 /2 width=1 by and3_intro/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
index e274719b7..0152a3d8a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
@@ -87,7 +87,7 @@ table {
 (*             [ "lcosx ( ? ⊢ ⧤⬊*[?,?,?] ? )" "lcosx_cpxs" * ] *)
              [ "llsx ( ? ⊢ ⋕⬊*[?,?,?,?] ? )" "llsx_alt ( ? ⊢ ⋕⬊⬊*[?,?,?,?] ? )" "llsx_ldrop" + "llsx_llpx" + "llsx_llpxs" + "llsx_csx" * ]
              [ "csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_tstc_vector" + "csx_aaa" * ]
-             [ "csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )" "csx_lift" + "csx_lpx" + "csx_lpxs" + "csx_fpbs" * ]
+             [ "csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )" "csx_lift" + "csx_lpx" + "csx_llpx" + "csx_lpxs" + "csx_llpxs" + "csx_fpbs" * ]
           }
         ]
         [ { "\"big tree\" parallel computation" * } {
@@ -103,8 +103,8 @@ table {
         ]
         [ { "context-sensitive extended computation" * } {
              [ "llpxs ( ⦃?,?⦄ ⊢ ➡*[?,?,?,?] ? )" "llpxs_lleq" + "llpxs_aaa" + "llpxs_lprs" "llpxs_cpxs" + "llpxs_llpxs" * ]
-(*             [ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )" "lpxs_alt ( ⦃?,?⦄ ⊢ ➡➡*[?,?] ? )" "lpxs_ldrop" + "lpxs_lleq" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ] *)
-             [ "cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpxs_tstc" + "cpxs_tstc_vector" + "cpxs_leq" + "cpxs_lift" + "cpxs_lleq" + "cpxs_aaa" + "cpxs_cpxs" * ]
+             [ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )" "lpxs_alt ( ⦃?,?⦄ ⊢ ➡➡*[?,?] ? )" "lpxs_ldrop" + "lpxs_lleq" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ]
+             [ "cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpxs_tstc" + "cpxs_tstc_vector" + "cpxs_leq" + "cpxs_lift" + "cpxs_lleq" + "cpxs_aaa" + "cpxs_llpx" + "cpxs_cpxs" * ]
           }
         ]
         [ { "context-sensitive computation" * } {
@@ -134,7 +134,7 @@ table {
         ]
         [ { "context-sensitive extended reduction" * } {
              [ "llpx ( ⦃?,?⦄ ⊢ ➡[?,?,?,?] ? )" "llpx_ldrop" + "llpx_lleq" + "llpx_aaa" + "llpx_lpr" * ]
-(*             [ "lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lpx_ldrop" + "lpx_lleq" + "lpx_aaa" * ] *)
+             [ "lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lpx_ldrop" + "lpx_lleq" + "lpx_aaa" * ]
              [ "cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpx_leq" + "cpx_lift" + "cpx_llpx_sn" + "cpx_lleq" + "cpx_cix" * ]
           }
         ]