From f21cc1fc7f776761926a7f017fda55735d63442e Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 2 Apr 2014 12:51:32 +0000
Subject: [PATCH] commit of the "computation" component with lazy pointwise
 extensions one conjecture is still open :(

---
 .../basic_2/computation/cpds_cpds.ma          |  15 +-
 .../basic_2/computation/cprs_cprs.ma          | 121 ++++++------
 .../basic_2/computation/cprs_lift.ma          |   5 +-
 .../basic_2/computation/cpxs_aaa.ma           |   2 +-
 .../basic_2/computation/cpxs_cpxs.ma          |  44 ++---
 .../basic_2/computation/cpxs_lift.ma          |   5 +-
 .../basic_2/computation/cpxs_tstc.ma          |   2 +-
 .../basic_2/computation/csx_alt.ma            |   2 +-
 .../basic_2/computation/csx_fpbs.ma           |   9 +-
 .../computation/{csx_lpx.ma => csx_llpx.ma}   |  15 +-
 .../computation/{csx_lpxs.ma => csx_llpxs.ma} |  12 +-
 .../basic_2/computation/csx_tstc_vector.ma    |   2 +-
 .../lambdadelta/basic_2/computation/fpbc.ma   |   4 +-
 .../basic_2/computation/fpbc_fleq.ma          |  34 ++++
 .../basic_2/computation/fpbc_fpbs.ma          |   4 +-
 .../basic_2/computation/fpbg_fleq.ma          |  78 ++++++++
 .../basic_2/computation/fpbg_fpbg.ma          |   6 +-
 .../lambdadelta/basic_2/computation/fpbs.ma   |  44 ++---
 .../basic_2/computation/fpbs_alt.ma           |  15 +-
 .../basic_2/computation/fpbs_ext.ma           |   8 +-
 .../basic_2/computation/fpbs_fleq.ma          |  26 +++
 .../basic_2/computation/fpbs_fpbs.ma          |  10 +-
 .../lambdadelta/basic_2/computation/fpbu.ma   |  16 +-
 .../{fpbu_fpns.ma => fpbu_fleq.ma}            |  32 ++--
 .../basic_2/computation/fpbu_lleq.ma          |  33 ++++
 .../lambdadelta/basic_2/computation/fpns.ma   |  39 ----
 .../lambdadelta/basic_2/computation/fsb.ma    |   2 +-
 .../basic_2/computation/fsb_csx.ma            |  12 +-
 .../lambdadelta/basic_2/computation/llprs.ma  |  61 +++++++
 .../basic_2/computation/llprs_cprs.ma         |  84 +++++++++
 .../{lpxs_lpxs.ma => llprs_llprs.ma}          |   8 +-
 .../lambdadelta/basic_2/computation/llpxs.ma  |  93 ++++++++++
 .../computation/{lpxs_aaa.ma => llpxs_aaa.ma} |  20 +-
 .../basic_2/computation/llpxs_cpxs.ma         | 172 ++++++++++++++++++
 .../basic_2/computation/llpxs_lleq.ma         |  66 +++++++
 .../{fpns_fpns.ma => llpxs_llpxs.ma}          |  13 +-
 .../lambdadelta/basic_2/computation/llsx.ma   |  57 ++++++
 .../basic_2/computation/llsx_alt.ma           | 107 +++++++++++
 .../basic_2/computation/llsx_csx.ma           |  95 ++++++++++
 .../{lprs_ldrop.ma => llsx_ldrop.ma}          |  25 +--
 .../{lprs_lprs.ma => llsx_llpx.ma}            |  22 +--
 .../basic_2/computation/llsx_llpxs.ma         |  66 +++++++
 .../lambdadelta/basic_2/computation/lprs.ma   |  71 --------
 .../basic_2/computation/lprs_alt.ma           |  47 -----
 .../basic_2/computation/lprs_cprs.ma          | 136 --------------
 .../lambdadelta/basic_2/computation/lpxs.ma   |  74 --------
 .../basic_2/computation/lpxs_alt.ma           |  47 -----
 .../basic_2/computation/lpxs_cpxs.ma          | 147 ---------------
 .../basic_2/computation/lpxs_ldrop.ma         |  29 ---
 .../basic_2/computation/lpxs_lleq.ma          | 125 -------------
 .../fpbc_fpns.ma => etc/lpx_sn/fpbc_fpns.etc} |   0
 .../fpbg_fpns.ma => etc/lpx_sn/fpbg_fpns.etc} |   0
 .../fpbs_fpns.ma => etc/lpx_sn/fpbs_fpns.etc} |   2 +-
 .../lpx_sn/lazycosn_5.etc}                    |   0
 .../lcosx.ma => etc/lpx_sn/lcosx.etc}         |   0
 .../lpx_sn/lcosx_cpxs.etc}                    |   0
 .../lsx.ma => etc/lpx_sn/lsx.etc}             |   0
 .../lsx_csx.ma => etc/lpx_sn/lsx_csx.etc}     |   0
 .../lsx_ldrop.ma => etc/lpx_sn/lsx_ldrop.etc} |   0
 .../lsx_lpxs.ma => etc/lpx_sn/lsx_lpxs.etc}   |   0
 .../basic_2/notation/relations/lazysnalt_6.ma |  19 ++
 .../lambdadelta/basic_2/reduction/cpx_lleq.ma |   4 +
 .../lambdadelta/basic_2/reduction/llpx.ma     |  15 ++
 63 files changed, 1238 insertions(+), 964 deletions(-)
 rename matita/matita/contribs/lambdadelta/basic_2/computation/{csx_lpx.ma => csx_llpx.ma} (92%)
 rename matita/matita/contribs/lambdadelta/basic_2/computation/{csx_lpxs.ma => csx_llpxs.ma} (72%)
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fleq.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fleq.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fleq.ma
 rename matita/matita/contribs/lambdadelta/basic_2/computation/{fpbu_fpns.ma => fpbu_fleq.ma} (70%)
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_lleq.ma
 delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/fpns.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/llprs.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/llprs_cprs.ma
 rename matita/matita/contribs/lambdadelta/basic_2/computation/{lpxs_lpxs.ma => llprs_llprs.ma} (84%)
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/llpxs.ma
 rename matita/matita/contribs/lambdadelta/basic_2/computation/{lpxs_aaa.ma => llpxs_aaa.ma} (69%)
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/llpxs_cpxs.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/llpxs_lleq.ma
 rename matita/matita/contribs/lambdadelta/basic_2/computation/{fpns_fpns.ma => llpxs_llpxs.ma} (74%)
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/llsx.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/llsx_alt.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/llsx_csx.ma
 rename matita/matita/contribs/lambdadelta/basic_2/computation/{lprs_ldrop.ma => llsx_ldrop.ma} (62%)
 rename matita/matita/contribs/lambdadelta/basic_2/computation/{lprs_lprs.ma => llsx_llpx.ma} (67%)
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/llsx_llpxs.ma
 delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/lprs.ma
 delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/lprs_alt.ma
 delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/lprs_cprs.ma
 delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/lpxs.ma
 delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_alt.ma
 delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma
 delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_ldrop.ma
 delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma
 rename matita/matita/contribs/lambdadelta/basic_2/{computation/fpbc_fpns.ma => etc/lpx_sn/fpbc_fpns.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{computation/fpbg_fpns.ma => etc/lpx_sn/fpbg_fpns.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{computation/fpbs_fpns.ma => etc/lpx_sn/fpbs_fpns.etc} (96%)
 rename matita/matita/contribs/lambdadelta/basic_2/{notation/relations/lazycosn_5.ma => etc/lpx_sn/lazycosn_5.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{computation/lcosx.ma => etc/lpx_sn/lcosx.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{computation/lcosx_cpxs.ma => etc/lpx_sn/lcosx_cpxs.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{computation/lsx.ma => etc/lpx_sn/lsx.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{computation/lsx_csx.ma => etc/lpx_sn/lsx_csx.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{computation/lsx_ldrop.ma => etc/lpx_sn/lsx_ldrop.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{computation/lsx_lpxs.ma => etc/lpx_sn/lsx_lpxs.etc} (100%)
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazysnalt_6.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpds_cpds.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpds_cpds.ma
index f66a63a9f..60b490393 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpds_cpds.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpds_cpds.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/unfold/lsstas_lsstas.ma".
-include "basic_2/computation/lprs_cprs.ma".
+include "basic_2/computation/llprs_cprs.ma".
 include "basic_2/computation/cpxs_cpxs.ma".
 include "basic_2/computation/cpds.ma".
 
@@ -26,13 +26,13 @@ lemma cpds_strap2: ∀h,g,G,L,T1,T,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 →
 #h #g #G #L #T1 #T #T2 #l #Hl #HT1 *
 #T0 #l0 #l1 #Hl10 #HT #HT0 #HT02
 lapply (ssta_da_conf … HT1 … Hl) <minus_plus_m_m #H0T
-lapply (da_mono … H0T … HT) -HT -H0T #H destruct /3 width=7/
+lapply (da_mono … H0T … HT) -HT -H0T #H destruct
+/3 width=7 by lsstas_step_sn, le_S_S, ex4_3_intro/
 qed.
 
 lemma cpds_cprs_trans: ∀h,g,G,L,T1,T,T2.
                        ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T → ⦃G, L⦄ ⊢ T ➡* T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2.
-#h #g #G #L #T1 #T #T2 * #T0 #l1 #l2 #Hl12 #Hl1 #HT10 #HT0 #HT2
-lapply (cprs_trans … HT0 … HT2) -T /2 width=7/
+#h #g #G #L #T1 #T #T2 * /3 width=9 by cprs_trans, ex4_3_intro/
 qed-.
 
 lemma lsstas_cpds_trans: ∀h,g,G,L,T1,T,T2,l1,l2.
@@ -42,7 +42,7 @@ lemma lsstas_cpds_trans: ∀h,g,G,L,T1,T,T2,l1,l2.
 lapply (lsstas_da_conf … HT1 … Hl1) #H0T
 lapply (da_mono … H0T … Hl3) -H0T -Hl3 #H destruct
 lapply (le_minus_to_plus_r … Hl21 Hl43) -Hl21 -Hl43
-lapply (lsstas_trans … HT1 … HT0) -T /2 width=7/
+/3 width=8 by lsstas_trans, ex4_3_intro/
 qed-.
 
 (* Advanced inversion lemmas ************************************************)
@@ -53,7 +53,8 @@ lemma cpds_inv_abst1: ∀h,g,a,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{a}V1.T1 •*➡*
 #h #g #a #G #L #V1 #T1 #U2 * #X #l1 #l2 #Hl21 #Hl1 #H1 #H2
 lapply (da_inv_bind … Hl1) -Hl1 #Hl1
 elim (lsstas_inv_bind1 … H1) -H1 #U #HTU1 #H destruct
-elim (cprs_inv_abst1 … H2) -H2 #V2 #T2 #HV12 #HUT2 #H destruct /3 width=7/
+elim (cprs_inv_abst1 … H2) -H2 #V2 #T2 #HV12 #HUT2 #H destruct
+/3 width=7 by ex4_3_intro, ex3_2_intro/
 qed-.
 
 lemma cpds_inv_abbr_abst: ∀h,g,a1,a2,G,L,V1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓓ{a1}V1.T1 •*➡*[h, g] ⓛ{a2}W2.T2 →
@@ -63,7 +64,7 @@ lapply (da_inv_bind … Hl1) -Hl1 #Hl1
 elim (lsstas_inv_bind1 … H1) -H1 #U1 #HTU1 #H destruct
 elim (cprs_inv_abbr1 … H2) -H2 *
 [ #V2 #U2 #HV12 #HU12 #H destruct
-| /3 width=7/
+| /3 width=7 by ex4_3_intro, ex3_intro/
 ]
 qed-.
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma
index 06b946111..a85488cdf 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/reduction/lpr_lpr.ma".
+include "basic_2/reduction/llpr_llpr.ma".
 include "basic_2/computation/cprs_lift.ma".
 
 (* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
@@ -22,58 +22,54 @@ include "basic_2/computation/cprs_lift.ma".
 (* Basic_1: was: pr3_t *)
 (* Basic_1: includes: pr1_t *)
 theorem cprs_trans: ∀G,L. Transitive … (cprs G L).
-#G #L #T1 #T #HT1 #T2 @trans_TC @HT1 qed-. (**) (* auto /3 width=3/ does not work because a δ-expansion gets in the way *)
+normalize /2 width=3 by trans_TC/ qed-. 
 
 (* Basic_1: was: pr3_confluence *)
 (* Basic_1: includes: pr1_confluence *)
 theorem cprs_conf: ∀G,L. confluent2 … (cprs G L) (cprs G L).
-#G #L @TC_confluent2 /2 width=3 by cpr_conf/ qed-. (**) (* auto /3 width=3/ does not work because a δ-expansion gets in the way *)
+normalize /3 width=3 by cpr_conf, TC_confluent2/ qed-.
 
 theorem cprs_bind: ∀a,I,G,L,V1,V2,T1,T2. ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ V1 ➡* V2 →
                    ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡* ⓑ{a,I}V2.T2.
-#a #I #G #L #V1 #V2 #T1 #T2 #HT12 #H @(cprs_ind … H) -V2 /2 width=1/
-#V #V2 #_ #HV2 #IHV1
-@(cprs_trans … IHV1) -V1 /2 width=1/
+#a #I #G #L #V1 #V2 #T1 #T2 #HT12 #H @(cprs_ind … H) -V2
+/3 width=5 by cprs_trans, cprs_bind_dx/
 qed.
 
 (* Basic_1: was: pr3_flat *)
 theorem cprs_flat: ∀I,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ V1 ➡* V2 →
                    ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ➡* ⓕ{I}V2.T2.
-#I #G #L #V1 #V2 #T1 #T2 #HT12 #H @(cprs_ind … H) -V2 /2 width=1/
-#V #V2 #_ #HV2 #IHV1
-@(cprs_trans … IHV1) -IHV1 /2 width=1/
+#I #G #L #V1 #V2 #T1 #T2 #HT12 #H @(cprs_ind … H) -V2
+/3 width=3 by cprs_flat_dx, cprs_strap1, cpr_pair_sn/
 qed.
 
 theorem cprs_beta_rc: ∀a,G,L,V1,V2,W1,W2,T1,T2.
                       ⦃G, L⦄ ⊢ V1 ➡ V2 → ⦃G, L.ⓛW1⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ W1 ➡* W2 →
                       ⦃G, L⦄ ⊢ ⓐV1.ⓛ{a}W1.T1 ➡* ⓓ{a}ⓝW2.V2.T2.
-#a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HT12 #H @(cprs_ind … H) -W2 /2 width=1/
-#W #W2 #_ #HW2 #IHW1
-@(cprs_trans … IHW1) -IHW1 /3 width=1/
+#a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HT12 #H @(cprs_ind … H) -W2 /2 width=1 by cprs_beta_dx/
+#W #W2 #_ #HW2 #IHW1 (**) (* fulla uto too slow 14s *)
+@(cprs_trans … IHW1) -IHW1 /3 width=1 by cprs_flat_dx, cprs_bind/
 qed.
 
 theorem cprs_beta: ∀a,G,L,V1,V2,W1,W2,T1,T2.
                    ⦃G, L.ⓛW1⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ W1 ➡* W2 → ⦃G, L⦄ ⊢ V1 ➡* V2 →
                    ⦃G, L⦄ ⊢ ⓐV1.ⓛ{a}W1.T1 ➡* ⓓ{a}ⓝW2.V2.T2.
-#a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HT12 #HW12 #H @(cprs_ind … H) -V2 /2 width=1/
+#a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HT12 #HW12 #H @(cprs_ind … H) -V2 /2 width=1 by cprs_beta_rc/
 #V #V2 #_ #HV2 #IHV1
-@(cprs_trans … IHV1) -IHV1 /3 width=1/
+@(cprs_trans … IHV1) -IHV1 /3 width=1 by cprs_flat_sn, cprs_bind/
 qed.
 
 theorem cprs_theta_rc: ∀a,G,L,V1,V,V2,W1,W2,T1,T2.
                        ⦃G, L⦄ ⊢ V1 ➡ V → ⇧[0, 1] V ≡ V2 → ⦃G, L.ⓓW1⦄ ⊢ T1 ➡* T2 →
                        ⦃G, L⦄ ⊢ W1 ➡* W2 → ⦃G, L⦄ ⊢ ⓐV1.ⓓ{a}W1.T1 ➡* ⓓ{a}W2.ⓐV2.T2.
-#a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HT12 #H elim H -W2 /2 width=3/
-#W #W2 #_ #HW2 #IHW1
-@(cprs_trans … IHW1) /2 width=1/
+#a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HT12 #H elim H -W2
+/3 width=5 by cprs_trans, cprs_theta_dx, cprs_bind_dx/
 qed.
 
 theorem cprs_theta: ∀a,G,L,V1,V,V2,W1,W2,T1,T2.
                     ⇧[0, 1] V ≡ V2 → ⦃G, L⦄ ⊢ W1 ➡* W2 → ⦃G, L.ⓓW1⦄ ⊢ T1 ➡* T2 →
                     ⦃G, L⦄ ⊢ V1 ➡* V → ⦃G, L⦄ ⊢ ⓐV1.ⓓ{a}W1.T1 ➡* ⓓ{a}W2.ⓐV2.T2.
-#a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV2 #HW12 #HT12 #H @(TC_ind_dx … V1 H) -V1 /2 width=3/
-#V1 #V0 #HV10 #_ #IHV0
-@(cprs_trans … IHV0) /2 width=1/
+#a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV2 #HW12 #HT12 #H @(TC_ind_dx … V1 H) -V1
+/3 width=3 by cprs_trans, cprs_theta_rc, cprs_flat_dx/
 qed.
 
 (* Advanced inversion lemmas ************************************************)
@@ -87,20 +83,20 @@ lemma cprs_inv_appl1: ∀G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓐV1.T1 ➡* U2 →
                        | ∃∃a,V0,V2,V,T. ⦃G, L⦄ ⊢ V1 ➡* V0 & ⇧[0,1] V0 ≡ V2 &
                                         ⦃G, L⦄ ⊢ T1 ➡* ⓓ{a}V.T &
                                         ⦃G, L⦄ ⊢ ⓓ{a}V.ⓐV2.T ➡* U2.
-#G #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 [ /3 width=5/ ]
+#G #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5 by or3_intro0, ex3_2_intro/
 #U #U2 #_ #HU2 * *
 [ #V0 #T0 #HV10 #HT10 #H destruct
   elim (cpr_inv_appl1 … HU2) -HU2 *
-  [ #V2 #T2 #HV02 #HT02 #H destruct /4 width=5/
+  [ #V2 #T2 #HV02 #HT02 #H destruct /4 width=5 by cprs_strap1, or3_intro0, ex3_2_intro/
   | #a #V2 #W #W2 #T #T2 #HV02 #HW2 #HT2 #H1 #H2 destruct
     lapply (cprs_strap1 … HV10 … HV02) -V0 #HV12
-    lapply (lsubr_cpr_trans … HT2 (L.ⓓⓝW.V1) ?) -HT2 /2 width=1/ #HT2
-    @or3_intro1 @(ex2_3_intro … HT10) -HT10 /3 width=1/ (**) (* explicit constructor. /5 width=8/ is too slow because TC_transitive gets in the way *)
+    lapply (lsubr_cpr_trans … HT2 (L.ⓓⓝW.V1) ?) -HT2
+    /5 width=5 by cprs_flat_dx, cpr_cprs, cprs_bind, lsubr_abst, ex2_3_intro, or3_intro1/
   | #a #V #V2 #W0 #W2 #T #T2 #HV0 #HV2 #HW02 #HT2 #H1 #H2 destruct
-    @or3_intro2 @(ex4_5_intro … HV2 HT10) /2 width=3/ /3 width=1/ (**) (* explicit constructor. /5 width=8/ is too slow because TC_transitive gets in the way *)
+    @or3_intro2 @(ex4_5_intro … HV2 HT10) /3 width=3 by cprs_flat_sn, cprs_strap1, cpr_cprs, cprs_bind/ (**) (* full auto is too slow 11s *)
   ]
-| /4 width=9/
-| /4 width=11/
+| /4 width=9 by cprs_strap1, or3_intro1, ex2_3_intro/
+| /4 width=11 by cprs_strap1, or3_intro2, ex4_5_intro/
 ]
 qed-.
 
@@ -108,68 +104,63 @@ qed-.
 
 (* Basic_1: was just: pr3_pr2_pr2_t *)
 (* Basic_1: includes: pr3_pr0_pr2_t *)
-lemma lpr_cpr_trans: ∀G. s_r_trans … (cpr G) (lpr G).
+lemma llpr_cpr_trans: ∀G. s_r_transitive … (cpr G) (llpr G 0).
 #G #L2 #T1 #T2 #HT12 elim HT12 -G -L2 -T1 -T2
-[ /2 width=3/
+[ /2 width=3 by/
 | #G #L2 #K2 #V0 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV02 #L1 #HL12
-  elim (lpr_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H
-  elim (lpr_inv_pair2 … H) -H #K1 #V1 #HK12 #HV10 #H destruct
-  lapply (IHV02 … HK12) -K2 #HV02
-  lapply (cprs_strap2 … HV10 … HV02) -V0 /2 width=6/
+  elim (llpr_inv_lref_ge_dx … HL12 … HLK2) -L2
+  /5 width=7 by cprs_delta, cprs_strap2, llpr_cpr_conf/
 | #a #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #HL12
-  lapply (IHT12 (L1.ⓑ{I}V1) ?) -IHT12 /2 width=1/ /3 width=1/
-|4,6: /3 width=1/
+  elim (llpr_inv_bind_O … HL12) -HL12 /4 width=1 by cprs_bind/
+| #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #HL12
+  elim (llpr_inv_flat … HL12) -HL12 /3 width=1 by cprs_flat/
 | #G #L2 #V2 #T1 #T #T2 #_ #HT2 #IHT1 #L1 #HL12
-  lapply (IHT1 (L1.ⓓV2) ?) -IHT1 /2 width=1/ /2 width=3/
+  elim (llpr_inv_bind_O … HL12) /3 width=3 by cprs_zeta/
+| #G #L2 #V2 #T1 #T2 #HT12 #IHT12 #L1 #HL12
+  elim (llpr_inv_flat … HL12) /3 width=1 by cprs_tau/
 | #a #G #L2 #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L1 #HL12
-  lapply (IHT12 (L1.ⓛW1) ?) -IHT12 /2 width=1/ /3 width=1/
+  elim (llpr_inv_flat … HL12) -HL12 #HV1 #HL12
+  elim (llpr_inv_bind_O … HL12) /3 width=3 by cprs_beta/
 | #a #G #L2 #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L1 #HL12
-  lapply (IHT12 (L1.ⓓW1) ?) -IHT12 /2 width=1/ /3 width=3/
+  elim (llpr_inv_flat … HL12) -HL12 #HV1 #HL12
+  elim (llpr_inv_bind_O … HL12) /3 width=3 by cprs_theta/
 ]
 qed-.
 
 lemma cpr_bind2: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡ V2 → ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ➡ T2 →
                  ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡* ⓑ{a,I}V2.T2.
-#G #L #V1 #V2 #HV12 #I #T1 #T2 #HT12
-lapply (lpr_cpr_trans … HT12 (L.ⓑ{I}V1) ?) /2 width=1/
-qed.
+/4 width=9 by llpr_cpr_trans, cprs_bind_dx, llpr_bind_repl_O/ qed.
 
 (* Advanced properties ******************************************************)
 
 (* Basic_1: was only: pr3_pr2_pr3_t pr3_wcpr0_t *)
-lemma lpr_cprs_trans: ∀G. s_rs_trans … (cpr G) (lpr G).
-/3 width=5 by s_r_trans_TC1, lpr_cpr_trans/ qed-.
+lemma cprs_llpr_trans: ∀G. s_rs_transitive … (cpr G) (llpr G 0).
+/3 width=6 by llpr_cpr_trans, llpr_cpr_conf, s_r_trans_LTC1/ qed-.
 
 (* Basic_1: was: pr3_strip *)
 (* Basic_1: includes: pr1_strip *)
 lemma cprs_strip: ∀G,L. confluent2 … (cprs G L) (cpr G L).
-#G #L @TC_strip1 /2 width=3 by cpr_conf/ qed-. (**) (* auto /3 width=3/ does not work because a δ-expansion gets in the way *)
-
-lemma cprs_lpr_conf_dx: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡* T1 → ∀L1. ⦃G, L0⦄ ⊢ ➡ L1 →
-                        ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡* T & ⦃G, L1⦄ ⊢ T0 ➡* T.
-#G #L0 #T0 #T1 #H elim H -T1
-[ #T1 #HT01 #L1 #HL01
-  elim (lpr_cpr_conf_dx … HT01 … HL01) -L0 /3 width=3/
-| #T #T1 #_ #HT1 #IHT0 #L1 #HL01
-  elim (IHT0 … HL01) #T2 #HT2 #HT02
-  elim (lpr_cpr_conf_dx … HT1 … HL01) -L0 #T3 #HT3 #HT13
-  elim (cprs_strip … HT2 … HT3) -T #T #HT2 #HT3
-  lapply (cprs_strap2 … HT13 … HT3) -T3
-  lapply (cprs_strap1 … HT02 … HT2) -T2 /2 width=3/
-]
+normalize /4 width=3 by cpr_conf, TC_strip1/ qed-.
+
+lemma cprs_llpr_conf_dx: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡* T1 → ∀L1. ⦃G, L0⦄ ⊢ ➡[T0, 0] L1 →
+                         ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡* T & ⦃G, L1⦄ ⊢ T0 ➡* T.
+#G #L0 #T0 #T1 #H @(cprs_ind_dx … T0 H) -T0 /2 width=3 by ex2_intro/
+#T0 #T #HT0 #_ #IHT1 #L1 #HL01
+elim (IHT1 … L1) /2 by llpr_cpr_conf/ -IHT1 #T2 #HT12 #HT2
+elim (llpr_cpr_conf_dx … HT0 … HL01) -L0 #T3 #HT03 #HT3
+elim (cprs_strip … HT2 … HT3) -T
+/4 width=5 by cprs_strap2, cprs_strap1, ex2_intro/
 qed-.
 
-lemma cprs_lpr_conf_sn: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡* T1 →
-                        ∀L1. ⦃G, L0⦄ ⊢ ➡ L1 →
-                        ∃∃T. ⦃G, L0⦄ ⊢ T1 ➡* T & ⦃G, L1⦄ ⊢ T0 ➡* T.
+lemma cprs_llpr_conf_sn: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡* T1 →
+                         ∀L1. ⦃G, L0⦄ ⊢ ➡[T0, 0] L1 →
+                         ∃∃T. ⦃G, L0⦄ ⊢ T1 ➡* T & ⦃G, L1⦄ ⊢ T0 ➡* T.
 #G #L0 #T0 #T1 #HT01 #L1 #HL01
-elim (cprs_lpr_conf_dx … HT01 … HL01) -HT01 #T #HT1
-lapply (lpr_cprs_trans … HT1 … HL01) -HT1 /2 width=3/
+elim (cprs_llpr_conf_dx … HT01 … HL01)
+/4 width=5 by cprs_llpr_trans, cprs_llpr_conf, ex2_intro/
 qed-.
 
 lemma cprs_bind2_dx: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡ V2 →
                      ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ➡* T2 →
                      ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡* ⓑ{a,I}V2.T2.
-#G #L #V1 #V2 #HV12 #I #T1 #T2 #HT12
-lapply (lpr_cprs_trans … HT12 (L.ⓑ{I}V1) ?) /2 width=1/
-qed.
+/4 width=9 by cprs_llpr_trans, cprs_bind_dx, llpr_bind_repl_O/ qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lift.ma
index ca1556a8e..27f0bb6e5 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lift.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/reduction/cpr_lift.ma".
+include "basic_2/reduction/llpr_ldrop.ma".
 include "basic_2/computation/cprs.ma".
 
 (* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
@@ -29,6 +29,9 @@ lapply (ldrop_fwd_drop2 … HLK) -HLK #HLK
 elim (lift_total V1 0 (i+1)) /4 width=12 by cpr_lift, cprs_strap1/
 qed.
 
+lemma cprs_llpr_conf: ∀G. s_r_confluent1 … (cprs G) (llpr G 0).
+/3 width=5 by llpr_cpr_conf, s_r_conf1_LTC1/ qed-.
+
 (* Advanced inversion lemmas ************************************************)
 
 (* Basic_1: was: pr3_gen_lref *)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_aaa.ma
index 4f054eac6..540d80d7e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_aaa.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/reduction/lpx_aaa.ma".
+include "basic_2/reduction/llpx_aaa.ma".
 include "basic_2/computation/cpxs.ma".
 
 (* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************)
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 21dd2a4cd..e52104665 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma
@@ -12,7 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/reduction/lpx_ldrop.ma".
 include "basic_2/computation/cpxs_lift.ma".
 
 (* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************)
@@ -20,8 +19,7 @@ include "basic_2/computation/cpxs_lift.ma".
 (* Main properties **********************************************************)
 
 theorem cpxs_trans: ∀h,g,G,L. Transitive … (cpxs h g G L).
-#h #g #G #L #T1 #T #HT1 #T2
-@trans_TC @HT1 qed-. (**) (* auto /3 width=3/ does not work because a δ-expansion gets in the way *)
+normalize /2 width=3 by trans_TC/ qed-.
 
 theorem cpxs_bind: ∀h,g,a,I,G,L,V1,V2,T1,T2. ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ➡*[h, g] T2 →
                    ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 →
@@ -94,45 +92,47 @@ qed-.
 
 (* Properties on sn extended parallel reduction for local environments ******)
 
-lemma lpx_cpx_trans: ∀h,g,G. s_r_trans … (cpx h g G) (lpx h g G).
+lemma llpx_cpx_trans: ∀h,g,G. s_r_transitive … (cpx h g G) (llpx h g G 0).
 #h #g #G #L2 #T1 #T2 #HT12 elim HT12 -G -L2 -T1 -T2
-[ /2 width=3 by /
+[ /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 (lpx_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H
-  elim (lpx_inv_pair2 … H) -H #K1 #V1 #HK12 #HV10 #H destruct
-  lapply (IHV02 … HK12) -K2 #HV02
-  lapply (cpxs_strap2 … HV10 … HV02) -V0 /2 width=7 by cpxs_delta/
+  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
-  lapply (IHT12 (L1.ⓑ{I}V1) ?) -IHT12 /3 width=1 by cpxs_bind, lpx_pair/
-|5,7,8: /3 width=1 by cpxs_flat, cpxs_ti, cpxs_tau/
+  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
-  lapply (IHT1 (L1.ⓓV2) ?) -IHT1 /2 width=3 by cpxs_zeta, lpx_pair/
+  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
-  lapply (IHT12 (L1.ⓛW1) ?) -IHT12 /3 width=1 by cpxs_beta, lpx_pair/
+  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
-  lapply (IHT12 (L1.ⓓW1) ?) -IHT12 /3 width=3 by cpxs_theta, cpxs_strap1, lpx_pair/
+  elim (llpx_inv_flat … HL12) -HL12 #HV1 #HL12
+  elim (llpx_inv_bind_O … HL12) /3 width=3 by cpxs_theta/
 ]
 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.
-#h #g #G #L #V1 #V2 #HV12 #I #T1 #T2 #HT12
-lapply (lpx_cpx_trans … HT12 (L.ⓑ{I}V1) ?) /2 width=1 by cpxs_bind_dx, lpx_pair/
-qed.
+/4 width=9 by llpx_cpx_trans, cpxs_bind_dx, llpx_bind_repl_O/ qed.
 
 (* Advanced properties ******************************************************)
 
-lemma lpx_cpxs_trans: ∀h,g,G. s_rs_trans … (cpx h g G) (lpx h g G).
-/3 width=5 by s_r_trans_TC1, lpx_cpx_trans/ qed-.
+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 *)
+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.
-#h #g #G #L #V1 #V2 #HV12 #I #T1 #T2 #HT12
-lapply (lpx_cpxs_trans … HT12 (L.ⓑ{I}V1) ?) /2 width=1 by cpxs_bind_dx, lpx_pair/
-qed.
+/4 width=9 by cpxs_llpx_trans, cpxs_bind_dx, llpx_bind_repl_O/ 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 de9a897b9..92b694f91 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/cpx_lift.ma".
+include "basic_2/reduction/llpx_ldrop.ma".
 include "basic_2/computation/cpxs.ma".
 
 (* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************)
@@ -42,6 +42,9 @@ 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/cpxs_tstc.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma
index eed76daea..76b8cc8ad 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/grammar/tstc.ma".
-include "basic_2/computation/lpxs_cpxs.ma".
+include "basic_2/computation/llpxs_cpxs.ma".
 
 (* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_alt.ma
index df23e1f2a..a6f46c787 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_alt.ma
@@ -38,7 +38,7 @@ qed-.
 
 (* Basic properties *********************************************************)
 
-lemma csx_intro_cprs: ∀h,g,G,L,T1.
+lemma csx_intro_cpxs: ∀h,g,G,L,T1.
                          (∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) → ⦃G, L⦄ ⊢ ⬊*[h, g] T2) →
                       ⦃G, L⦄ ⊢ ⬊*[h, g] T1.
 /4 width=1 by cpx_cpxs, csx_intro/ qed.
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 7d8882793..eabda3146 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_fpbs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_fpbs.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/computation/fpbs.ma".
-include "basic_2/computation/csx_lpx.ma".
+include "basic_2/computation/csx_llpx.ma".
 
 (* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************)
 
@@ -22,7 +22,7 @@ include "basic_2/computation/csx_lpx.ma".
 lemma csx_fpb_conf: ∀h,g,G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 →
                     ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ → ⦃G2, L2⦄ ⊢ ⬊*[h, g] T2.
 #h #g #G1 #L1 #T1 #HT1 #G2 #L2 #T2 *
-/2 width=5 by csx_cpx_trans, csx_fquq_conf, csx_lpx_conf/
+/2 width=5 by csx_cpx_trans, csx_fquq_conf, csx_llpx_conf/
 qed-.
 
 lemma csx_fpbs_conf: ∀h,g,G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 →
@@ -30,8 +30,3 @@ lemma csx_fpbs_conf: ∀h,g,G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 →
 #h #g #G1 #L1 #T1 #HT1 #G2 #L2 #T2 #H @(fpbs_ind … H) -G2 -L2 -T2
 /2 width=5 by csx_fpb_conf/
 qed-.
-
-lemma csx_lpxs_conf: ∀h,g,G,L1. ∀T:term. ⦃G, L1⦄ ⊢ ⬊*[h, g] T →
-                     ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → ⦃G, L2⦄ ⊢ ⬊*[h, g] T.
-/3 width=5 by csx_fpbs_conf, lpxs_fpbs/
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_llpx.ma
similarity index 92%
rename from matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma
rename to matita/matita/contribs/lambdadelta/basic_2/computation/csx_llpx.ma
index f8bf3c475..b21b7bf51 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_llpx.ma
@@ -21,10 +21,10 @@ include "basic_2/computation/csx_lift.ma".
 
 (* 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/
+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 *)
 qed-.
 
 lemma csx_abst: ∀h,g,a,G,L,W. ⦃G, L⦄ ⊢ ⬊*[h, g] W →
@@ -35,7 +35,8 @@ 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/
+  #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.
@@ -47,7 +48,7 @@ lemma csx_abbr: ∀h,g,a,G,L,V. ⦃G, L⦄ ⊢ ⬊*[h, g] V →
 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/
+  [ /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
@@ -108,7 +109,7 @@ elim (cpx_inv_appl1 … HL) -HL *
 | -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
+  @(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-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_llpxs.ma
similarity index 72%
rename from matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpxs.ma
rename to matita/matita/contribs/lambdadelta/basic_2/computation/csx_llpxs.ma
index d49b6e7ae..aad3e8bf0 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_llpxs.ma
@@ -12,14 +12,14 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/computation/csx_lpx.ma".
-include "basic_2/computation/lpxs.ma".
+include "basic_2/computation/csx_llpx.ma".
+include "basic_2/computation/llpxs.ma".
 
 (* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************)
 
-(* Properties on sn extended parallel computation for local environments ****)
+(* Properties on lazy sn extended 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/
+lemma csx_llpxs_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 #HT #L2 #H @(llpxs_ind … H) -L2 /3 by llpxs_strap1, csx_llpx_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 5e9ea06c7..a20455c9c 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_lpx.ma".
+include "basic_2/computation/csx_llpx.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/fpbc.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc.ma
index 3fc670868..4656f8431 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc.ma
@@ -13,14 +13,14 @@
 (**************************************************************************)
 
 include "basic_2/notation/relations/lazybtpredproper_8.ma".
-include "basic_2/computation/fpns.ma".
+include "basic_2/substitution/fleq.ma".
 include "basic_2/computation/fpbu.ma".
 
 (* SINGLE-STEP "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **********)
 
 definition fpbc: ∀h. sd h → tri_relation genv lenv term ≝
                  λh,g,G1,L1,T1,G2,L2,T2.
-                 ∃∃G,L,T.  ⦃G1, L1, T1⦄ ≻[h, g] ⦃G, L, T⦄ & ⦃G, L, T⦄ ⊢ ⋕➡*[h, g] ⦃G2, L2, T2⦄ .
+                 ∃∃G,L,T.  ⦃G1, L1, T1⦄ ≻[h, g] ⦃G, L, T⦄ & ⦃G, L, T⦄ ⋕[0] ⦃G2, L2, T2⦄ .
 
 interpretation
    "single-step 'big tree' proper parallel reduction (closure)"
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fleq.ma
new file mode 100644
index 000000000..9056ca4c7
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fleq.ma
@@ -0,0 +1,34 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/fleq_fleq.ma".
+include "basic_2/computation/fpbu_fleq.ma".
+include "basic_2/computation/fpbc.ma".
+
+(* SINGLE-STEP "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **********)
+
+(* Properties on lazy equivalence on closures *******************************)
+
+lemma fpbc_fleq_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≻⋕[h, g] ⦃G, L, T⦄ →
+                       ⦃G, L, T⦄ ⋕[0] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≻⋕[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 *
+/3 width=9 by fleq_trans, ex2_3_intro/
+qed-.
+
+lemma fleq_fpbc_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⋕[0] ⦃G, L, T⦄ →
+                       ⦃G, L, T⦄ ≻⋕[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≻⋕[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 *
+#G0 #L0 #T0 #H0 #H02 elim (fleq_fpbu_trans … H1 … H0) -G -L -T
+/3 width=9 by fleq_trans, ex2_3_intro/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fpbs.ma
index 28efb6e6b..7d81c812d 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fpbs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fpbs.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/computation/fpbs_fpns.ma".
+include "basic_2/computation/fpbs_fleq.ma".
 include "basic_2/computation/fpbs_fpbs.ma".
 include "basic_2/computation/fpbc.ma".
 
@@ -23,5 +23,5 @@ include "basic_2/computation/fpbc.ma".
 lemma fpbc_fwd_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻⋕[h, g] ⦃G2, L2, T2⦄ →
                      ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
 #h #g #G1 #G2 #L1 #L2 #T1 #T2 *
-/3 width=5 by fpbu_fwd_fpbs, fpbs_trans, fpns_fpbs/
+/3 width=5 by fpbu_fwd_fpbs, fpbs_trans, fleq_fpbs/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fleq.ma
new file mode 100644
index 000000000..bb79f4aab
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fleq.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/computation/fpbc_fleq.ma".
+include "basic_2/computation/fpbg.ma".
+
+(* GENEARAL "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES *************)
+
+(* Properties on lazy equivalence for closures ******************************)
+
+lemma fpbg_fleq_trans: ∀h,g,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G, L, T⦄ →
+                       ∀G2,L2,T2. ⦃G, L, T⦄ ⋕[0] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G #L1 #L #T1 #T #H @(fpbg_ind … H) -G -L -T
+[ /3 width=5 by fpbc_fpbg, fpbc_fleq_trans/
+| /4 width=9 by fpbg_strap1, fpbc_fleq_trans/
+]
+qed-.
+
+lemma fleq_fpbg_trans: ∀h,g,G,G2,L,L2,T,T2. ⦃G, L, T⦄ >⋕[h, g] ⦃G2, L2, T2⦄ →
+                       ∀G1,L1,T1. ⦃G1, L1, T1⦄ ⋕[0] ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄.
+#h #g #G #G2 #L #L2 #T #T2 #H @(fpbg_ind_dx … H) -G -L -T
+[ /3 width=5 by fpbc_fpbg, fleq_fpbc_trans/
+| /4 width=9 by fpbg_strap2, fleq_fpbc_trans/
+]
+qed-.
+
+lemma fpbs_fpbg: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ →
+                 ⦃G1, L1, T1⦄ ⋕[0] ⦃G2, L2, T2⦄ ∨
+                 ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbs_ind … H) -G2 -L2 -T2
+[ /2 width=1 by or_introl/
+| #G #G2 #L #L2 #T #T2 #_ #H2 * #H1 elim (fpb_fpbu … H2) -H2 #H2
+  [ /3 width=5 by fleq_trans, or_introl/
+  | /5 width=5 by fpbc_fpbg, fleq_fpbc_trans, fpbu_fpbc, or_intror/
+  | /3 width=5 by fpbg_fleq_trans, or_intror/
+  | /4 width=5 by fpbg_strap1, fpbu_fpbc, or_intror/
+  ]
+]
+qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma fpbg_fpb_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2.
+                      ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≽[h, g] ⦃G2, L2, T2⦄ →
+                      ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H2 elim (fpb_fpbu … H2) -H2
+/3 width=5 by fpbg_fleq_trans, fpbg_strap1, fpbu_fpbc/
+qed-.
+
+
+lemma fpb_fpbg_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2.
+                      ⦃G1, L1, T1⦄ ≽[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ >⋕[h, g] ⦃G2, L2, T2⦄ →
+                      ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 elim (fpb_fpbu … H1) -H1
+/3 width=5 by fleq_fpbg_trans, fpbg_strap2, fpbu_fpbc/
+qed-.
+
+lemma fpbs_fpbg_trans: ∀h,g,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ →
+                       ∀G2,L2,T2. ⦃G, L, T⦄ >⋕[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G #L1 #L #T1 #T #H @(fpbs_ind … H) -G -L -T /3 width=5 by fpb_fpbg_trans/
+qed-.
+
+(* Note: this is used in the closure proof *)
+lemma fpbg_fpbs_trans: ∀h,g,G,G2,L,L2,T,T2. ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ →
+                       ∀G1,L1,T1. ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄.
+#h #g #G #G2 #L #L2 #T #T2 #H @(fpbs_ind_dx … H) -G -L -T /3 width=5 by fpbg_fpb_trans/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbg.ma
index 2cb1f197e..9cf029f09 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbg.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbg.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/computation/fpbc_fpbs.ma".
-include "basic_2/computation/fpbg_fpns.ma".
+include "basic_2/computation/fpbg_fleq.ma".
 
 (* GENERAL "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **************)
 
@@ -22,10 +22,10 @@ include "basic_2/computation/fpbg_fpns.ma".
 lemma fpbg_inv_fpbu_sn: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄ →
                         ∃∃G,L,T. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G, L, T⦄ & ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄.
 #h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbg_ind_dx … H) -G1 -L1 -T1
-[ #G1 #L1 #T1 * /3 width=5 by fpns_fpbs, ex2_3_intro/
+[ #G1 #L1 #T1 * /3 width=5 by fleq_fpbs, ex2_3_intro/
 | #G1 #G #L1 #L #T1 #T *
   #G0 #L0 #T0 #H10 #H0 #_ *
-  /5 width=9 by fpbu_fwd_fpbs, fpbs_trans, fpns_fpbs, ex2_3_intro/
+  /5 width=9 by fpbu_fwd_fpbs, fpbs_trans, fleq_fpbs, ex2_3_intro/
 ]
 qed-.
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma
index 7ad3bb47a..361353ece 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma
@@ -16,7 +16,7 @@ include "basic_2/notation/relations/btpredstar_8.ma".
 include "basic_2/substitution/fqus.ma".
 include "basic_2/reduction/fpb.ma".
 include "basic_2/computation/cpxs.ma".
-include "basic_2/computation/lpxs.ma".
+include "basic_2/computation/llpxs.ma".
 
 (* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************)
 
@@ -72,20 +72,20 @@ lemma cpxs_fpbs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → ⦃G, L,
 /3 width=5 by fpb_cpx, fpbs_strap1/
 qed.
 
-lemma lpxs_fpbs: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → ⦃G, L1, T⦄ ≥[h, g] ⦃G, L2, T⦄.
-#h #g #G #L1 #L2 #T #H @(lpxs_ind … H) -L2
-/3 width=5 by fpb_lpx, fpbs_strap1/
+lemma llpxs_fpbs: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡*[h, g, T, 0] L2 → ⦃G, L1, T⦄ ≥[h, g] ⦃G, L2, T⦄.
+#h #g #G #L1 #L2 #T #H @(llpxs_ind … H) -L2
+/3 width=5 by fpb_llpx, fpbs_strap1/
 qed.
 
 lemma cprs_fpbs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → ⦃G, L, T1⦄ ≥[h, g] ⦃G, L, T2⦄.
 /3 width=1 by cprs_cpxs, cpxs_fpbs/ qed.
 
-lemma lprs_fpbs: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L1, T⦄ ≥[h, g] ⦃G, L2, T⦄.
-/3 width=1 by lprs_lpxs, lpxs_fpbs/ qed.
+lemma llprs_fpbs: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡*[T, 0] L2 → ⦃G, L1, T⦄ ≥[h, g] ⦃G, L2, T⦄.
+/3 width=1 by llprs_llpxs, llpxs_fpbs/ qed.
 
-lemma cpr_lpr_fpbs: ∀h,g,G,L1,L2,T1,T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ⦃G, L1⦄ ⊢ ➡ L2 →
+lemma cpr_llpr_fpbs: ∀h,g,G,L1,L2,T1,T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ⦃G, L1⦄ ⊢ ➡[T2, 0] L2 →
                     ⦃G, L1, T1⦄ ≥[h, g] ⦃G, L2, T2⦄.
-/4 width=5 by fpbs_strap1, lpr_fpb, cpr_fpb/ qed.
+/4 width=5 by fpbs_strap1, llpr_fpb, cpr_fpb/ qed.
 
 lemma fpbs_fqus_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ →
                        ⦃G, L, T⦄ ⊃* ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
@@ -103,10 +103,10 @@ lemma fpbs_cpxs_trans: ∀h,g,G1,G,L1,L,T1,T,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G
 /3 width=5 by fpbs_strap1, fpb_cpx/
 qed-.
 
-lemma fpbs_lpxs_trans: ∀h,g,G1,G,L1,L,L2,T1,T. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ →
-                       ⦃G, L⦄ ⊢ ➡*[h, g] L2 → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L2, T⦄.
-#h #g #G1 #G #L1 #L #L2 #T1 #T #H1 #H @(lpxs_ind … H) -L2
-/3 width=5 by fpbs_strap1, fpb_lpx/
+lemma fpbs_llpxs_trans: ∀h,g,G1,G,L1,L,L2,T1,T. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ →
+                       ⦃G, L⦄ ⊢ ➡*[h, g, T, 0] L2 → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L2, T⦄.
+#h #g #G1 #G #L1 #L #L2 #T1 #T #H1 #H @(llpxs_ind … H) -L2
+/3 width=5 by fpbs_strap1, fpb_llpx/
 qed-.
 
 lemma cpxs_fqus_fpbs: ∀h,g,G1,G2,L1,L2,T1,T,T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T →
@@ -117,13 +117,13 @@ lemma cpxs_fqup_fpbs: ∀h,g,G1,G2,L1,L2,T1,T,T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g]
                       ⦃G1, L1, T⦄ ⊃+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
 /3 width=5 by fpbs_fqup_trans, cpxs_fpbs/ qed-.
 
-lemma fqus_lpxs_fpbs: ∀h,g,G1,G2,L1,L,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L, T2⦄ →
-                      ⦃G2, L⦄ ⊢ ➡*[h, g] L2 → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
-/3 width=3 by fpbs_lpxs_trans, fqus_fpbs/ qed.
+lemma fqus_llpxs_fpbs: ∀h,g,G1,G2,L1,L,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L, T2⦄ →
+                      ⦃G2, L⦄ ⊢ ➡*[h, g, T2, 0] L2 → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
+/3 width=3 by fpbs_llpxs_trans, fqus_fpbs/ qed.
 
-lemma cpxs_fqus_lpxs_fpbs: ∀h,g,G1,G2,L1,L,L2,T1,T,T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T →
-                           ⦃G1, L1, T⦄ ⊃* ⦃G2, L, T2⦄ → ⦃G2, L⦄ ⊢ ➡*[h, g] L2 → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
-/3 width=5 by cpxs_fqus_fpbs, fpbs_lpxs_trans/ qed.
+lemma cpxs_fqus_llpxs_fpbs: ∀h,g,G1,G2,L1,L,L2,T1,T,T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T →
+                           ⦃G1, L1, T⦄ ⊃* ⦃G2, L, T2⦄ → ⦃G2, L⦄ ⊢ ➡*[h, g, T2, 0] L2 → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
+/3 width=5 by cpxs_fqus_fpbs, fpbs_llpxs_trans/ qed.
 
 lemma fqus_fpbs_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ →
                        ⦃G1, L1, T1⦄ ⊃* ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
@@ -137,8 +137,8 @@ lemma cpxs_fpbs_trans: ∀h,g,G1,G2,L1,L2,T1,T,T2. ⦃G1, L1, T⦄ ≥[h, g] ⦃
 /3 width=5 by fpbs_strap2, fpb_cpx/
 qed-.
 
-lemma lpxs_fpbs_trans: ∀h,g,G1,G2,L1,L,L2,T1,T2. ⦃G1, L, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ →
-                       ⦃G1, L1⦄ ⊢ ➡*[h, g] L → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
-#h #g #G1 #G2 #L1 #L #L2 #T1 #T2 #H1 #H @(lpxs_ind_dx … H) -L1
-/3 width=5 by fpbs_strap2, fpb_lpx/
+lemma llpxs_fpbs_trans: ∀h,g,G1,G2,L1,L,L2,T1,T2. ⦃G1, L, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ →
+                       ⦃G1, L1⦄ ⊢ ➡*[h, g, T1, 0] L → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G2 #L1 #L #L2 #T1 #T2 #H1 #H @(llpxs_ind_dx … H) -L1
+/3 width=5 by fpbs_strap2, fpb_llpx/
 qed-.
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 36fc55264..bf05fb03c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/notation/relations/btpredstaralt_8.ma".
-include "basic_2/computation/lpxs_cpxs.ma".
+include "basic_2/computation/llpxs_cpxs.ma".
 include "basic_2/computation/fpbs_fpbs.ma".
 
 (* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************)
@@ -23,7 +23,7 @@ definition fpbsa: ∀h. sd h → tri_relation genv lenv term ≝
                   λh,g,G1,L1,T1,G2,L2,T2.
                   ∃∃L,T. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T &
                          ⦃G1, L1, T⦄ ⊃* ⦃G2, L, T2⦄ &
-                         ⦃G2, L⦄ ⊢ ➡*[h, g] L2.
+                         ⦃G2, L⦄ ⊢ ➡*[h, g, T2, 0] L2.
 
 interpretation "'big tree' parallel computation (closure) alternative"
    'BTPRedStarAlt h g G1 L1 T1 G2 L2 T2 = (fpbsa h g G1 L1 T1 G2 L2 T2).
@@ -37,10 +37,11 @@ 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 (lpx_cpxs_trans … HT0 … HL1) -HT0
-  elim (lpx_fqus_trans … HG2 … HL1) -L
-  /3 width=7 by lpxs_strap2, cpxs_trans, ex3_2_intro/
-] 
+| lapply (cpxs_llpx_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/
+]
 qed-.
 
 (* Main properties **********************************************************)
@@ -56,5 +57,5 @@ qed.
 theorem fpbsa_inv_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2.
                         ⦃G1, L1, T1⦄ ≥≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
 #h #g #G1 #G2 #L1 #L2 #T1 #T2 *
-/4 width=5 by fpbs_trans, fqus_fpbs, cpxs_fpbs, lpxs_fpbs/
+/4 width=5 by fpbs_trans, fqus_fpbs, cpxs_fpbs, llpxs_fpbs/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_ext.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_ext.ma
index 515753860..8ae11770f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_ext.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_ext.ma
@@ -23,9 +23,9 @@ lemma fpbs_cpxs_trans_neq: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, g]
                            ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ≥[h, g] ⦃G2, L2, U2⦄.
 #h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 #HnTU2 elim (fpbs_fpbsa … H) -H
 #L0 #T0 #HT10 #H10 #HL02 elim (eq_term_dec T1 T0) [ -HT10 | -HnTU2 ]
-[ #H destruct lapply (lpxs_cpxs_trans … HTU2 … HL02) -HTU2
-  #HTU2 elim (fqus_cpxs_trans_neq … H10 … HTU2 HnTU2) -T2
-  /3 width=6 by fqus_lpxs_fpbs, ex3_intro/
-| /4 width=6 by fpbs_cpxs_trans, fqus_lpxs_fpbs, ex3_intro/
+[ #H destruct lapply (llpxs_cpxs_trans … HTU2 … HL02)
+  #H elim (fqus_cpxs_trans_neq … H10 … H HnTU2) -H10 -H -HnTU2
+  /4 width=8 by fqus_llpxs_fpbs, llpxs_cpxs_conf_dx, ex3_intro/
+| /4 width=6 by fpbs_cpxs_trans, fqus_llpxs_fpbs, ex3_intro/
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fleq.ma
new file mode 100644
index 000000000..3823dfbd0
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fleq.ma
@@ -0,0 +1,26 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/fleq.ma".
+include "basic_2/computation/llpxs_lleq.ma".
+include "basic_2/computation/fpbs.ma".
+
+(* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************)
+
+(* Properties on lazy equivalence on closures *******************************)
+
+lemma fleq_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2.
+                 ⦃G1, L1, T1⦄ ⋕[0] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 * /3 width=1 by llpxs_fpbs, llpxs_lrefl/
+qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbs.ma
index 86cbe3ee3..109dcda03 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbs.ma
@@ -23,8 +23,8 @@ theorem fpbs_trans: ∀h,g. tri_transitive … (fpbs h g).
 
 (* Advanced properties ******************************************************)
 
-lemma cpr_lpr_ssta_fpbs: ∀h,g,G,L1,L2,T1,T2,U2,l2.
-                         ⦃G, L1⦄ ⊢ T1 ➡ T2 → ⦃G, L1⦄ ⊢ ➡ L2 →
-                         ⦃G, L2⦄ ⊢ T2 ▪[h, g] l2+1 → ⦃G, L2⦄ ⊢ T2 •[h, g] U2 →
-                         ⦃G, L1, T1⦄ ≥[h, g] ⦃G, L2, U2⦄.
-/3 width=5 by fpbs_trans, cpr_lpr_fpbs, ssta_fpbs/ qed.
+lemma cpr_llpr_ssta_fpbs: ∀h,g,G,L1,L2,T1,T2,U2,l2.
+                          ⦃G, L1⦄ ⊢ T1 ➡ T2 → ⦃G, L1⦄ ⊢ ➡[T2, 0] L2 →
+                          ⦃G, L2⦄ ⊢ T2 ▪[h, g] l2+1 → ⦃G, L2⦄ ⊢ T2 •[h, g] U2 →
+                          ⦃G, L1, T1⦄ ≥[h, g] ⦃G, L2, U2⦄.
+/3 width=5 by fpbs_trans, cpr_llpr_fpbs, ssta_fpbs/ qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu.ma
index 93e837f9e..52c00a82b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu.ma
@@ -13,15 +13,15 @@
 (**************************************************************************)
 
 include "basic_2/notation/relations/btpredproper_8.ma".
-include "basic_2/relocation/lleq.ma".
+include "basic_2/substitution/lleq.ma".
 include "basic_2/computation/fpbs.ma".
 
 (* UNITARY "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **************)
 
 inductive fpbu (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝
-| fpbu_fqup: ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → fpbu h g G1 L1 T1 G2 L2 T2
-| fpbu_cpxs: ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) → fpbu h g G1 L1 T1 G1 L1 T2
-| fpbu_lpxs: ∀L2. ⦃G1, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[T1, 0] L2 → ⊥) → fpbu h g G1 L1 T1 G1 L2 T1
+| fpbu_fqup : ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → fpbu h g G1 L1 T1 G2 L2 T2
+| fpbu_cpxs : ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) → fpbu h g G1 L1 T1 G1 L1 T2
+| fpbu_llpxs: ∀L2. ⦃G1, L1⦄ ⊢ ➡*[h, g, T1, 0] L2 → (L1 ⋕[T1, 0] L2 → ⊥) → fpbu h g G1 L1 T1 G1 L2 T1
 .
 
 interpretation
@@ -34,14 +34,14 @@ lemma cprs_fpbu: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → (T1 = T2 → 
                  ⦃G, L, T1⦄ ≻[h, g] ⦃G, L, T2⦄.
 /3 width=1 by fpbu_cpxs, cprs_cpxs/ qed.
 
-lemma lprs_fpbu: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡* L2 → (L1 ⋕[T, 0] L2 → ⊥) →
-                 ⦃G, L1, T⦄ ≻[h, g] ⦃G, L2, T⦄.
-/3 width=1 by fpbu_lpxs, lprs_lpxs/ qed.
+lemma llprs_fpbu: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡*[T, 0] L2 → (L1 ⋕[T, 0] L2 → ⊥) →
+                  ⦃G, L1, T⦄ ≻[h, g] ⦃G, L2, T⦄.
+/3 width=1 by fpbu_llpxs, llprs_llpxs/ qed.
 
 (* Basic forward lemmas *****************************************************)
 
 lemma fpbu_fwd_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ →
                      ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
 #h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2
-/3 width=1 by lpxs_fpbs, cpxs_fpbs, fqup_fpbs/
+/3 width=1 by llpxs_fpbs, cpxs_fpbs, fqup_fpbs/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_fpns.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_fleq.ma
similarity index 70%
rename from matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_fpns.ma
rename to matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_fleq.ma
index 863b08196..3beb43760 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_fpns.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_fleq.ma
@@ -12,32 +12,24 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/relocation/lleq_lleq.ma".
-include "basic_2/computation/cpxs_lleq.ma".
-include "basic_2/computation/lpxs_lleq.ma".
-include "basic_2/computation/lpxs_lpxs.ma".
-include "basic_2/computation/fpns.ma".
+include "basic_2/substitution/fleq.ma".
 include "basic_2/computation/fpbs_alt.ma".
-include "basic_2/computation/fpbu.ma".
+include "basic_2/computation/fpbu_lleq.ma".
 
 (* UNITARY "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **************)
 
-(* Properties on parallel computation for "big tree" normal forms ***********)
+(* Properties on lazy equivalence for closures ******************************)
 
-lemma fpns_fpbu_trans: ∀h,g,F1,F2,K1,K2,T1,T2. ⦃F1, K1, T1⦄ ⊢ ⋕➡*[h, g] ⦃F2, K2, T2⦄ →
+lemma fleq_fpbu_trans: ∀h,g,F1,F2,K1,K2,T1,T2. ⦃F1, K1, T1⦄ ⋕[0] ⦃F2, K2, T2⦄ →
                        ∀G2,L2,U2. ⦃F2, K2, T2⦄ ≻[h, g] ⦃G2, L2, U2⦄ →
-                       ∃∃G1,L1,U1. ⦃F1, K1, T1⦄ ≻[h, g] ⦃G1, L1, U1⦄ & ⦃G1, L1, U1⦄ ⊢ ⋕➡*[h, g] ⦃G2, L2, U2⦄.
+                       ∃∃G1,L1,U1. ⦃F1, K1, T1⦄ ≻[h, g] ⦃G1, L1, U1⦄ & ⦃G1, L1, U1⦄ ⋕[0] ⦃G2, L2, U2⦄.
 #h #g #F1 #F2 #K1 #K2 #T1 #T2 * -F2 -K2 -T2
-#K2 #HK12 #HT1 #G2 #L2 #U2 * -G2 -L2 -U2
-[ #G2 #L2 #U2 #H12 elim (lpxs_lleq_fqup_trans … H12 … HK12 HT1) -K2
-  /3 width=5 by fpbu_fqup, fpns_intro, ex2_3_intro/
-| /4 width=9 by fpbu_cpxs, fpns_intro, lpxs_cpxs_trans, lleq_cpxs_conf_dx, ex2_3_intro/
-| /5 width=5 by fpbu_lpxs, lpxs_trans, lleq_canc_sn, ex2_3_intro/
-]
+#K2 #HK12 #G2 #L2 #U2 #H12 elim (lleq_fpbu_trans … HK12 … H12) -K2
+/3 width=5 by fleq_intro, ex2_3_intro/
 qed-.
 
 lemma fpb_fpbu: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ →
-                ⦃G1, L1, T1⦄ ⊢ ⋕➡*[h, g] ⦃G2, L2, T2⦄ ∨
+                ⦃G1, L1, T1⦄ ⋕[0] ⦃G2, L2, T2⦄ ∨
                 ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄.
 #h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2
 [ #G2 #L2 #T2 #H elim (fquq_inv_gen … H) -H
@@ -47,12 +39,12 @@ lemma fpb_fpbu: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2,
 | #T2 #HT12 elim (eq_term_dec T1 T2)
   #HnT12 destruct /4 width=1 by fpbu_cpxs, cpx_cpxs, or_intror, or_introl/
 | #L2 #HL12 elim (lleq_dec … T1 L1 L2 0)
-  /4 width=3 by fpbu_lpxs, fpns_intro, lpx_lpxs, or_intror, or_introl/
+  /4 width=3 by fpbu_llpxs, fleq_intro, llpx_llpxs, or_intror, or_introl/
 ]
 qed-.
 
 lemma fpbs_fpbu_sn: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ →
-                    ⦃G1, L1, T1⦄ ⊢ ⋕➡*[h, g] ⦃G2, L2, T2⦄ ∨
+                    ⦃G1, L1, T1⦄ ⋕[0] ⦃G2, L2, T2⦄ ∨
                     ∃∃G,L,T. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G, L, T⦄ & ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄.
 (* ALTERNATIVE PROOF
 #h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbs_ind_dx … H) -G1 -L1 -T1
@@ -67,8 +59,8 @@ lemma fpbs_fpbu_sn: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2,
   [ #HT2 @or_intror
     /5 width=9 by fpbsa_inv_fpbs, fpbu_fqup, ex3_2_intro, ex2_3_intro, or_intror/
   | * #HG #HL #HT destruct elim (lleq_dec T2 L L2 0) #H
-    [ /3 width=1 by fpns_intro, or_introl/
-    | /5 width=5 by fpbu_lpxs, ex2_3_intro, or_intror/
+    [ /3 width=1 by fleq_intro, or_introl/
+    | /5 width=5 by fpbu_llpxs, ex2_3_intro, or_intror/
     ]
   ]
 | elim (cpxs_neq_inv_step_sn … HT1 H) -HT1 -H
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_lleq.ma
new file mode 100644
index 000000000..a08672bc8
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_lleq.ma
@@ -0,0 +1,33 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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_fqus.ma".
+include "basic_2/substitution/lleq_lleq.ma".
+include "basic_2/computation/llpxs_lleq.ma".
+include "basic_2/computation/fpbu.ma".
+
+(* UNITARY "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **************)
+
+(* Properties on lazy equivalence for local environments ********************)
+
+lemma lleq_fpbu_trans: ∀h,g,F,K1,K2,T. K1 ⋕[T, 0] K2 →
+                       ∀G,L2,U. ⦃F, K2, T⦄ ≻[h, g] ⦃G, L2, U⦄ →
+                       ∃∃L1. ⦃F, K1, T⦄ ≻[h, g] ⦃G, L1, U⦄ & L1 ⋕[U, 0] L2.
+#h #g #F #K1 #K2 #T #HT #G #L2 #U * -G -L2 -U
+[ #G #L2 #U #H2 elim (lleq_fqup_trans … H2 … HT) -K2
+  /3 width=3 by fpbu_fqup, ex2_intro/
+| /4 width=10 by fpbu_cpxs, lleq_cpxs_conf_sn, lleq_cpxs_trans, ex2_intro/
+| /5 width=3 by fpbu_llpxs, lleq_llpxs_trans, lleq_canc_sn, ex2_intro/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpns.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpns.ma
deleted file mode 100644
index dce46b065..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpns.ma
+++ /dev/null
@@ -1,39 +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/btpredsnstar_8.ma".
-include "basic_2/relocation/lleq.ma".
-include "basic_2/computation/lpxs.ma".
-
-(* PARALLEL COMPUTATION FOR "BIG TREE" NORMAL FORMS *************************)
-
-inductive fpns (h) (g) (G) (L1) (T): relation3 genv lenv term ≝
-| fpns_intro: ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → L1 ⋕[T, 0] L2 → fpns h g G L1 T G L2 T
-.
-
-interpretation
-   "computation for 'big tree' normal forms (closure)"
-   'BTPRedSnStar h g G1 L1 T1 G2 L2 T2 = (fpns h g G1 L1 T1 G2 L2 T2).
-
-(* Basic_properties *********************************************************)
-
-lemma fpns_refl: ∀h,g. tri_reflexive … (fpns h g).
-/2 width=1 by fpns_intro/ qed.
-
-(* Basic inversion lemmas ***************************************************) 
-
-lemma fpns_inv_gen: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊢ ⋕➡*[h, g] ⦃G2, L2, T2⦄ →
-                    ∧∧ G1 = G2 & ⦃G1, L1⦄ ⊢ ➡*[h, g] L2 & L1 ⋕[T1, 0] L2 & T1 = T2.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 /2 width=1 by and4_intro/
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma
index 1616402de..6aef8f2bd 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma
@@ -43,5 +43,5 @@ qed-.
 (* Basic inversion lemmas ***************************************************)
 
 lemma fsb_inv_csx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⦥[h, g] T → ⦃G, L⦄ ⊢ ⬊*[h, g] T.
-#h #g #G #L #T #H elim H -G -L -T /5 width=1 by csx_intro_cprs, fpbu_cpxs/
+#h #g #G #L #T #H elim H -G -L -T /5 width=1 by csx_intro_cpxs, fpbu_cpxs/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma
index f983e8d06..453383dc4 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma
@@ -14,7 +14,7 @@
 
 include "basic_2/computation/fpbs_ext.ma".
 include "basic_2/computation/csx_fpbs.ma".
-include "basic_2/computation/lsx_csx.ma".
+include "basic_2/computation/llsx_csx.ma".
 include "basic_2/computation/fsb_alt.ma".
 
 (* "BIG TREE" STRONGLY NORMALIZING TERMS ************************************)
@@ -27,19 +27,19 @@ lemma csx_fsb_fpbs: ∀h,g,G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 →
 #T1 #HT1 #IHc #G2 #L2 #T2 @(fqup_wf_ind … G2 L2 T2) -G2 -L2 -T2
 #G0 #L0 #T0 #IHu #H10 lapply (csx_fpbs_conf … H10) // -HT1
 #HT0 generalize in match IHu; -IHu generalize in match H10; -H10
-@(lsx_ind … (csx_lsx … HT0 0)) -L0
+@(llsx_ind_alt … (csx_llsx … HT0 0)) -L0
 #L0 #_ #IHl #H10 #IHu @fsb_intro
 #G2 #L2 #T2 * -G2 -L2 -T2 [ -IHl -IHc | -IHu -IHl |  ]
 [ /3 width=5 by fpbs_fqup_trans/
 | #T2 #HT02 #HnT02 elim (fpbs_cpxs_trans_neq … H10 … HT02 HnT02) -T0
   /3 width=4 by/
 | #L2 #HL02 #HnL02 @(IHl … HL02 HnL02) -IHl -HnL02 [ -IHu -IHc | ]
-  [ /2 width=3 by fpbs_lpxs_trans/
-  | #G3 #L3 #T3 #H03 #_ elim (lpxs_fqup_trans … H03 … HL02) -L2
+  [ /2 width=3 by fpbs_llpxs_trans/
+  | #G3 #L3 #T3 #H03 #_ elim (llpxs_fqup_trans … H03 … HL02) -L2
     #L4 #T4 elim (eq_term_dec T0 T4) [ -IHc | -IHu ]
-    [ #H destruct /4 width=5 by fsb_fpbs_trans, lpxs_fpbs, fpbs_fqup_trans/
+    [ #H destruct /4 width=5 by fsb_fpbs_trans, llpxs_fpbs, fpbs_fqup_trans/
     | #HnT04 #HT04 #H04 elim (fpbs_cpxs_trans_neq … H10 … HT04 HnT04) -T0
-      /4 width=8 by fpbs_fqup_trans, fpbs_lpxs_trans/
+      /4 width=8 by fpbs_fqup_trans, fpbs_llpxs_trans/
     ]
   ]
 ]
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/llprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/llprs.ma
new file mode 100644
index 000000000..d3c2a6f27
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/llprs.ma
@@ -0,0 +1,61 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/lazypredsnstar_5.ma".
+include "basic_2/reduction/llpr.ma".
+
+(* LAZY SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ***********************)
+
+definition llprs: genv → relation4 ynat term lenv lenv ≝
+                  λG,d. LTC … (llpr G d).
+
+interpretation "lazy parallel computation (local environment, sn variant)"
+   'LazyPRedSnStar G L1 L2 T d = (llprs G d T L1 L2).
+
+(* Basic eliminators ********************************************************)
+
+lemma llprs_ind: ∀G,L1,T,d. ∀R:predicate lenv. R L1 →
+                 (∀L,L2. ⦃G, L1⦄ ⊢ ➡*[T, d] L → ⦃G, L⦄ ⊢ ➡[T, d] L2 → R L → R L2) →
+                 ∀L2. ⦃G, L1⦄ ⊢ ➡*[T, d] L2 → R L2.
+#G #L1 #T #d #R #HL1 #IHL1 #L2 #HL12
+@(TC_star_ind … HL1 IHL1 … HL12) //
+qed-.
+
+lemma llprs_ind_dx: ∀G,L2,T,d. ∀R:predicate lenv. R L2 →
+                    (∀L1,L. ⦃G, L1⦄ ⊢ ➡[T, d] L → ⦃G, L⦄ ⊢ ➡*[T, d] L2 → R L → R L1) →
+                    ∀L1. ⦃G, L1⦄ ⊢ ➡*[T, d] L2 → R L1.
+#G #L2 #T #d #R #HL2 #IHL2 #L1 #HL12
+@(TC_star_ind_dx … HL2 IHL2 … HL12) //
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma lpr_llprs: ∀G,L1,L2,T,d. ⦃G, L1⦄ ⊢ ➡[T, d] L2 → ⦃G, L1⦄ ⊢ ➡*[T, d] L2.
+/2 width=1 by inj/ qed.
+
+lemma llprs_refl: ∀G,L,T,d. ⦃G, L⦄ ⊢ ➡*[T, d] L.
+/2 width=1 by lpr_llprs/ qed.
+
+lemma llprs_strap1: ∀G,L1,L,L2,T,d. ⦃G, L1⦄ ⊢ ➡*[T, d] L → ⦃G, L⦄ ⊢ ➡[T, d] L2 → ⦃G, L1⦄ ⊢ ➡*[T, d] L2.
+normalize /2 width=3 by step/ qed-.
+
+lemma llprs_strap2: ∀G,L1,L,L2,T,d. ⦃G, L1⦄ ⊢ ➡[T, d] L → ⦃G, L⦄ ⊢ ➡*[T, d] L2 → ⦃G, L1⦄ ⊢ ➡*[T, d] L2.
+normalize /2 width=3 by TC_strap/ qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma llprs_fwd_length: ∀G,L1,L2,T,d. ⦃G, L1⦄ ⊢ ➡*[T, d] L2 → |L1| = |L2|.
+#G #L1 #L2 #T #d #H @(llprs_ind … H) -L2
+/3 width=6 by llpr_fwd_length, trans_eq/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/llprs_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/llprs_cprs.ma
new file mode 100644
index 000000000..910bedfe9
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/llprs_cprs.ma
@@ -0,0 +1,84 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/relocation/llpx_sn_tc.ma".
+include "basic_2/computation/cprs_cprs.ma".
+include "basic_2/computation/llprs.ma".
+
+(* LAZY SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ***********************)
+
+(* Advanced properties ******************************************************)
+
+lemma llprs_pair_dx: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡* V2 →
+                     ∀I,T. ⦃G, L.ⓑ{I}V1⦄ ⊢ ➡*[T, 0] L.ⓑ{I}V2.
+/2 width=1 by llpx_sn_TC_pair_dx/ qed.
+
+(* Properties on context-sensitive parallel computation for terms ***********)
+
+lemma llprs_cpr_trans: ∀G. s_r_transitive … (cpr G) (llprs G 0).
+/3 width=5 by cprs_llpr_trans, s_r_trans_LTC2/ qed-.
+
+(* Basic_1: was just: pr3_pr3_pr3_t *)
+lemma llprs_cprs_trans: ∀G. s_rs_transitive … (cpr G) (llprs G 0).
+#G @s_r_to_s_rs_trans @s_r_trans_LTC2
+/3 width=5 by cprs_llpr_trans, s_rs_trans_TC1/ (**) (* full auto too slow *)
+qed-.
+
+lemma cprs_bind2: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡* V2 →
+                  ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ➡* T2 →
+                  ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡* ⓑ{a,I}V2.T2.
+/4 width=3 by llprs_cprs_trans, llprs_pair_dx, cprs_bind/ qed.
+
+(* Inversion lemmas on context-sensitive parallel computation for terms *****)
+
+(* Basic_1: was: pr3_gen_abst *)
+lemma cprs_inv_abst1: ∀a,G,L,W1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{a}W1.T1 ➡* U2 →
+                      ∃∃W2,T2. ⦃G, L⦄ ⊢ W1 ➡* W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ➡* T2 &
+                               U2 = ⓛ{a}W2.T2.
+#a #G #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /2 width=5 by ex3_2_intro/
+#U0 #U2 #_ #HU02 * #V0 #T0 #HV10 #HT10 #H destruct
+elim (cpr_inv_abst1 … HU02) -HU02 #V2 #T2 #HV02 #HT02 #H destruct
+lapply (llprs_cpr_trans … HT02 (L.ⓛV1) ?)
+/3 width=5 by llprs_pair_dx, cprs_trans, cprs_strap1, ex3_2_intro/
+qed-.
+
+lemma cprs_inv_abst: ∀a,G,L,W1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓛ{a}W1.T1 ➡* ⓛ{a}W2.T2 →
+                     ⦃G, L⦄ ⊢ W1 ➡* W2 ∧ ⦃G, L.ⓛW1⦄ ⊢ T1 ➡* T2.
+#a #G #L #W1 #W2 #T1 #T2 #H
+elim (cprs_inv_abst1 … H) -H #W #T #HW1 #HT1 #H destruct /2 width=1 by conj/
+qed-.
+
+(* Basic_1: was pr3_gen_abbr *)
+lemma cprs_inv_abbr1: ∀a,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{a}V1.T1 ➡* U2 → (
+                      ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡* V2 & ⦃G, L.ⓓV1⦄ ⊢ T1 ➡* T2 &
+                               U2 = ⓓ{a}V2.T2
+                      ) ∨
+                      ∃∃T2. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡* T2 & ⇧[0, 1] U2 ≡ T2 & a = true.
+#a #G #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5 by ex3_2_intro, or_introl/
+#U0 #U2 #_ #HU02 * *
+[ #V0 #T0 #HV10 #HT10 #H destruct
+  elim (cpr_inv_abbr1 … HU02) -HU02 *
+  [ #V2 #T2 #HV02 #HT02 #H destruct
+    lapply (llprs_cpr_trans … HT02 (L.ⓓV1) ?)
+    /4 width=5 by llprs_pair_dx, cprs_trans, cprs_strap1, ex3_2_intro, or_introl/
+  | #T2 #HT02 #HUT2
+    lapply (llprs_cpr_trans … HT02 (L.ⓓV1) ?) -HT02
+    /4 width=3 by llprs_pair_dx, cprs_trans, ex3_intro, or_intror/
+  ]
+| #U1 #HTU1 #HU01
+  elim (lift_total U2 0 1) #U #HU2
+  lapply (cpr_lift … HU02 (L.ⓓV1) … HU01 … HU2) -U0
+  /4 width=3 by cprs_strap1, ldrop_drop, ex3_intro, or_intror/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/llprs_llprs.ma
similarity index 84%
rename from matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lpxs.ma
rename to matita/matita/contribs/lambdadelta/basic_2/computation/llprs_llprs.ma
index 998f89e14..4f97672f3 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lpxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/llprs_llprs.ma
@@ -12,11 +12,11 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/computation/lpxs.ma".
+include "basic_2/computation/llprs.ma".
 
-(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************)
+(* LAZY SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ***********************)
 
 (* Main properties **********************************************************)
 
-theorem lpxs_trans: ∀h,g,G. Transitive … (lpxs h g G).
-/2 width=3/ qed-.
+theorem llprs_trans: ∀G,T,d. Transitive … (llprs G d T).
+normalize /2 width=3 by trans_TC/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/llpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/llpxs.ma
new file mode 100644
index 000000000..154c24f20
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/llpxs.ma
@@ -0,0 +1,93 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/lazypredsnstar_7.ma".
+include "basic_2/reduction/llpx.ma".
+include "basic_2/computation/llprs.ma".
+
+(* LAZY SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS **************)
+
+definition llpxs: ∀h. sd h → genv → relation4 ynat term lenv lenv ≝
+                  λh,g,G,d. LTC … (llpx h g G d).
+
+interpretation "lazy extended parallel computation (local environment, sn variant)"
+   'LazyPRedSnStar G L1 L2 h g T d = (llpxs h g G d T L1 L2).
+
+(* Basic eliminators ********************************************************)
+
+lemma llpxs_ind: ∀h,g,G,L1,T,d. ∀R:predicate lenv. R L1 →
+                 (∀L,L2. ⦃G, L1⦄ ⊢ ➡*[h, g, T, d] L → ⦃G, L⦄ ⊢ ➡[h, g, T, d] L2 → R L → R L2) →
+                 ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g, T, d] L2 → R L2.
+#h #g #G #L1 #T #d #R #HL1 #IHL1 #L2 #HL12
+@(TC_star_ind … HL1 IHL1 … HL12) //
+qed-.
+
+lemma llpxs_ind_dx: ∀h,g,G,L2,T,d. ∀R:predicate lenv. R L2 →
+                    (∀L1,L. ⦃G, L1⦄ ⊢ ➡[h, g, T, d] L → ⦃G, L⦄ ⊢ ➡*[h, g, T, d] L2 → R L → R L1) →
+                    ∀L1. ⦃G, L1⦄ ⊢ ➡*[h, g, T, d] L2 → R L1.
+#h #g #G #L2 #T #d #R #HL2 #IHL2 #L1 #HL12
+@(TC_star_ind_dx … HL2 IHL2 … HL12) //
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma llprs_llpxs: ∀h,g,G,L1,L2,T,d. ⦃G, L1⦄ ⊢ ➡*[T, d] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g, T, d] L2.
+normalize /3 width=3 by llpr_llpx, monotonic_TC/ qed.
+
+lemma llpx_llpxs: ∀h,g,G,L1,L2,T,d. ⦃G, L1⦄ ⊢ ➡[h, g, T, d] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g, T, d] L2.
+normalize /2 width=1 by inj/ qed.
+
+lemma llpxs_refl: ∀h,g,G,L,T,d. ⦃G, L⦄ ⊢ ➡*[h, g, T, d] L.
+/2 width=1 by llpx_llpxs/ qed.
+
+lemma llpxs_strap1: ∀h,g,G,L1,L,L2,T,d. ⦃G, L1⦄ ⊢ ➡*[h, g, T, d] L → ⦃G, L⦄ ⊢ ➡[h, g, T, d] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g, T, d] L2.
+normalize /2 width=3 by step/ qed.
+
+lemma llpxs_strap2: ∀h,g,G,L1,L,L2,T,d. ⦃G, L1⦄ ⊢ ➡[h, g, T, d] L → ⦃G, L⦄ ⊢ ➡*[h, g, T, d] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g, T, d] L2.
+normalize /2 width=3 by TC_strap/ qed.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma llpxs_fwd_length: ∀h,g,G,L1,L2,T,d. ⦃G, L1⦄ ⊢ ➡*[h, g, T, d] L2 → |L1| = |L2|.
+#h #g #G #L1 #L2 #T #d #H @(llpxs_ind … H) -L2
+/3 width=8 by llpx_fwd_length, trans_eq/
+qed-.
+
+(* Note: this might be moved *)
+lemma llpxs_fwd_bind_sn: ∀h,g,a,I,G,L1,L2,V,T,d. ⦃G, L1⦄ ⊢ ➡*[h, g, ⓑ{a,I}V.T, d] L2 →
+                         ⦃G, L1⦄ ⊢ ➡*[h, g, V, d] L2.
+#h #g #a #I #G #L1 #L2 #V #T #d #H @(llpxs_ind … H) -L2
+/3 width=6 by llpx_fwd_bind_sn, llpxs_strap1/
+qed-.
+
+(* Note: this might be moved *)
+lemma llpxs_fwd_bind_dx: ∀h,g,a,I,G,L1,L2,V,T,d. ⦃G, L1⦄ ⊢ ➡*[h, g, ⓑ{a,I}V.T, d] L2 →
+                         ⦃G, L1.ⓑ{I}V⦄ ⊢ ➡*[h, g, T, ⫯d] L2.ⓑ{I}V.
+#h #g #a #I #G #L1 #L2 #V #T #d #H @(llpxs_ind … H) -L2
+/3 width=6 by llpx_fwd_bind_dx, llpxs_strap1/
+qed-.
+
+(* Note: this might be moved *)
+lemma llpxs_fwd_flat_sn: ∀h,g,I,G,L1,L2,V,T,d. ⦃G, L1⦄ ⊢ ➡*[h, g, ⓕ{I}V.T, d] L2 →
+                         ⦃G, L1⦄ ⊢ ➡*[h, g, V, d] L2.
+#h #g #I #G #L1 #L2 #V #T #d #H @(llpxs_ind … H) -L2
+/3 width=6 by llpx_fwd_flat_sn, llpxs_strap1/
+qed-.
+
+(* Note: this might be moved *)
+lemma llpxs_fwd_flat_dx: ∀h,g,I,G,L1,L2,V,T,d. ⦃G, L1⦄ ⊢ ➡*[h, g, ⓕ{I}V.T, d] L2 →
+                         ⦃G, L1⦄ ⊢ ➡*[h, g, T, d] L2.
+#h #g #I #G #L1 #L2 #V #T #d #H @(llpxs_ind … H) -L2
+/3 width=6 by llpx_fwd_flat_dx, llpxs_strap1/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/llpxs_aaa.ma
similarity index 69%
rename from matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_aaa.ma
rename to matita/matita/contribs/lambdadelta/basic_2/computation/llpxs_aaa.ma
index 80c43c731..f9b30323a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/llpxs_aaa.ma
@@ -12,21 +12,19 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/reduction/lpx_aaa.ma".
-include "basic_2/computation/lpxs.ma".
+include "basic_2/reduction/llpx_aaa.ma".
+include "basic_2/computation/llpxs.ma".
 
-(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************)
+(* LAZY 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.
+lemma aaa_llpxs_conf: ∀h,g,G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A →
+                      ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g, T, 0] 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/
+@(TC_Conf3 … (λL,A. ⦃G, L⦄ ⊢ T ⁝ A) … HT ? HL12) /2 width=5 by aaa_llpx_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-.
+lemma aaa_llprs_conf: ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A →
+                      ∀L2. ⦃G, L1⦄ ⊢ ➡*[T, 0] L2 → ⦃G, L2⦄ ⊢ T ⁝ A.
+/3 width=5 by aaa_llpxs_conf, llprs_llpxs/ 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
new file mode 100644
index 000000000..1ac05bce3
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/llpxs_cpxs.ma
@@ -0,0 +1,172 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/llpx_sn_tc.ma".
+include "basic_2/computation/cpxs_cpxs.ma".
+include "basic_2/computation/llpxs.ma".
+
+(* LAZY SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS **************)
+
+(* Advanced properties ******************************************************)
+
+lemma llpxs_pair_dx: ∀h,g,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 →
+                     ∀I,T. ⦃G, L.ⓑ{I}V1⦄ ⊢ ➡*[h, g, T, 0] L.ⓑ{I}V2.
+/2 width=1 by llpx_sn_TC_pair_dx/ qed.
+
+(* 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-.
+
+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 *)
+qed-.
+
+(* Note: this is an instance of a general theorem *)
+lemma llpxs_cpxs_conf_dx: ∀h,g,G2,L2,T2,U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] U2 →
+                          ∀L0. ⦃G2, L0⦄ ⊢ ➡*[h, g, T2, O] L2 → ⦃G2, L0⦄ ⊢ ➡*[h, g, U2, O] L2.
+#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/
+qed-.
+
+(* Note: this is an instance of a general theorem *)
+lemma llpxs_cpx_conf_dx: ∀h,g,G2,L2,T2,U2. ⦃G2, L2⦄ ⊢ T2 ➡[h, g] U2 →
+                         ∀L0. ⦃G2, L0⦄ ⊢ ➡*[h, g, T2, O] L2 → ⦃G2, L0⦄ ⊢ ➡*[h, g, U2, O] L2.
+#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/
+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 llpxs_cpxs_trans, llpxs_pair_dx, cpxs_bind/ qed.
+
+(* Advanced forward lemmas **************************************************)
+
+(* Note: this might be moved *)
+lemma llpxs_fwd_lref_ge_sn: ∀h,g,G,L1,L2,d,i. ⦃G, L1⦄ ⊢ ➡*[h, g, #i, d] L2 → d ≤ i →
+                            ∀I,K1,V1. ⇩[i] L1 ≡ K1.ⓑ{I}V1 →
+                            ∃∃K2,V2. ⇩[i] L2 ≡ K2.ⓑ{I}V2 &
+                                     ⦃G, K1⦄ ⊢ ➡*[h, g, V2, 0] K2 & ⦃G, K1⦄ ⊢ V1 ➡*[h, g] V2.
+#h #g #G #L1 #L2 #d #i #H #Hdi #I #K1 #V1 #HLK1 @(llpxs_ind … H) -L2 /2 width=5 by ex3_2_intro/ -HLK1
+#L #L2 #_ #HL2 * #K #V #HLK #HK1 #HV1 elim (llpx_inv_lref_ge_sn … HL2 … HLK) // -HL2 -HLK -Hdi
+#K2 #V2 #HLK2 #HK2 #HV2
+@(ex3_2_intro … HLK2) -HLK2
+[ /3 width=5 by llpxs_cpx_conf_dx, llpxs_strap1, llpx_cpx_conf/
+| /3 width=5 by llpxs_cpx_trans, cpxs_trans/
+]
+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 (llpxs_cpx_trans … HT02 (L.ⓛV1) ?)
+/3 width=5 by llpxs_pair_dx, 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 (llpxs_cpx_trans … HT02 (L.ⓓV1) ?)
+    /4 width=5 by llpxs_pair_dx, cpxs_trans, cpxs_strap1, ex3_2_intro, or_introl/
+  | #T2 #HT02 #HUT2
+    lapply (llpxs_cpx_trans … HT02 (L.ⓓV1) ?) -HT02
+    /4 width=3 by llpxs_pair_dx, 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-.
+
+(* Properties on supclosure *************************************************)
+
+lemma llpx_fqup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ →
+                       ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g, T1, 0] L1 →
+                       ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g, T2, 0] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
+[ #G2 #L2 #T2 #H12 #K1 #HKL1 elim (llpx_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 (llpx_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 llpx_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
+                       ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g, T1, 0] L1 →
+                       ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g, T2, 0] 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 (llpx_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 llpxs_fquq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
+                        ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g, T1, 0] L1 →
+                        ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g, T2, 0] L2.
+#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 (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/
+]
+qed-.
+
+lemma llpxs_fqup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ →
+                        ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g, T1, 0] L1 →
+                        ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g, T2, 0] L2.
+#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 (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/
+]
+qed-.
+
+lemma llpxs_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
+                        ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g, T1, 0] L1 →
+                        ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g, T2, 0] L2.
+#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 (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/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/llpxs_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/llpxs_lleq.ma
new file mode 100644
index 000000000..a38ba395a
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/llpxs_lleq.ma
@@ -0,0 +1,66 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/substitution/lleq_leq.ma".
+include "basic_2/reduction/llpx_lleq.ma".
+include "basic_2/computation/cpxs_lleq.ma".
+include "basic_2/computation/llpxs_cpxs.ma".
+
+(* LAZY SN EXTENDED PARALLEL COMPUTATION FOR LOCAL ENVIRONMENTS *************)
+
+(* Properties on lazy equivalence for local environments ********************)
+
+lemma llpxs_lrefl: ∀h,g,G,L1,L2,T,d. L1 ⋕[T, d] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g, T, d] L2.
+/3 width=1 by llpx_lrefl, llpx_llpxs/ qed-.
+
+lemma lleq_llpxs_trans: ∀h,g,G,L2,L,T,d. ⦃G, L2⦄ ⊢ ➡*[h, g, T, d] L →
+                        ∀L1. L1 ⋕[T, d] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g, T, d] L.
+#h #g #G #L2 #L #T #d #H @(llpxs_ind … H) -L
+/3 width=3 by llpxs_strap1, llpxs_lrefl/
+qed-.
+
+lemma lleq_llpxs_conf: ∀h,g,G,L1,L,T,d. ⦃G, L1⦄ ⊢ ➡*[h, g, T, d] L →
+                       ∀L2. L1 ⋕[T, d] L2 → ⦃G, L2⦄ ⊢ ➡*[h, g, T, d] L.
+/3 width=3 by lleq_llpxs_trans, lleq_sym/ qed-.
+(*
+foct 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-.
+
+lamma 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/fpns_fpns.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/llpxs_llpxs.ma
similarity index 74%
rename from matita/matita/contribs/lambdadelta/basic_2/computation/fpns_fpns.ma
rename to matita/matita/contribs/lambdadelta/basic_2/computation/llpxs_llpxs.ma
index deaa7a967..d316c5207 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpns_fpns.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/llpxs_llpxs.ma
@@ -12,16 +12,11 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/relocation/lleq_lleq.ma".
-include "basic_2/computation/lpxs_lpxs.ma".
-include "basic_2/computation/fpns.ma".
+include "basic_2/computation/llpxs.ma".
 
-(* PARALLEL COMPUTATION FOR "BIG TREE" NORMAL FORMS *************************)
+(* LAZY SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS **************)
 
 (* Main properties **********************************************************)
 
-theorem fpns_trans: ∀h,g. tri_transitive … (fpns h g).
-#h #g #G1 #G #L1 #L #T1 #T * -G -L -T
-#L #HL1 #HT1 #G2 #L2 #T2 * -G2 -L2 -T2
-/3 width=3 by lpxs_trans, lleq_trans, fpns_intro/
-qed-.
+theorem llpxs_trans: ∀h,g,G,T,d. Transitive … (llpxs h g G d T).
+normalize /2 width=3 by trans_TC/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/llsx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/llsx.ma
new file mode 100644
index 000000000..286d0645f
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/llsx.ma
@@ -0,0 +1,57 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/lazysn_6.ma".
+include "basic_2/substitution/lleq.ma".
+include "basic_2/reduction/llpx.ma".
+
+(* LAZY SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS *****************)
+
+definition llsx: ∀h. sd h → relation4 ynat term genv lenv ≝
+                 λh,g,d,T,G. SN … (llpx h g G d T) (lleq d T).
+
+interpretation
+   "lazy extended strong normalization (local environment)"
+   'LazySN h g d T G L = (llsx h g T d G L).
+
+(* Basic eliminators ********************************************************)
+
+lemma llsx_ind: ∀h,g,G,T,d. ∀R:predicate lenv.
+                (∀L1. G ⊢ ⋕⬊*[h, g, T, d] L1 →
+                      (∀L2. ⦃G, L1⦄ ⊢ ➡[h, g, T, d] L2 → (L1 ⋕[T, d] L2 → ⊥) → R L2) →
+                      R L1
+                ) →
+                ∀L. G ⊢ ⋕⬊*[h, g, T, d] L → R L.
+#h #g #G #T #d #R #H0 #L1 #H elim H -L1
+/5 width=1 by lleq_sym, SN_intro/
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma llsx_intro: ∀h,g,G,L1,T,d.
+                  (∀L2. ⦃G, L1⦄ ⊢ ➡[h, g, T, d] L2 → (L1 ⋕[T, d] L2 → ⊥) → G ⊢ ⋕⬊*[h, g, T, d] L2) →
+                  G ⊢ ⋕⬊*[h, g, T, d] L1.
+/5 width=1 by lleq_sym, SN_intro/ qed.
+
+lemma llsx_sort: ∀h,g,G,L,d,k. G ⊢ ⋕⬊*[h, g, ⋆k, d] L.
+#h #g #G #L1 #d #k @llsx_intro
+#L2 #HL12 #H elim H -H
+/3 width=6 by llpx_fwd_length, lleq_sort/
+qed.
+
+lemma llsx_gref: ∀h,g,G,L,d,p. G ⊢ ⋕⬊*[h, g, §p, d] L.
+#h #g #G #L1 #d #p @llsx_intro
+#L2 #HL12 #H elim H -H
+/3 width=6 by llpx_fwd_length, lleq_gref/
+qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/llsx_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/llsx_alt.ma
new file mode 100644
index 000000000..0d23439b9
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/llsx_alt.ma
@@ -0,0 +1,107 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/notation/relations/lazysnalt_6.ma".
+include "basic_2/substitution/lleq_lleq.ma".
+include "basic_2/computation/llpxs_lleq.ma".
+include "basic_2/computation/llsx.ma".
+
+(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************)
+
+(* alternative definition of llsx *)
+definition llsxa: ∀h. sd h → relation4 ynat term genv lenv ≝
+                  λh,g,d,T,G. SN … (llpxs h g G d T) (lleq d T).
+
+interpretation
+   "lazy extended strong normalization (local environment) alternative"
+   'LazySNAlt h g d T G L = (llsxa h g T d G L).
+
+(* Basic eliminators ********************************************************)
+
+lemma llsxa_ind: ∀h,g,G,T,d. ∀R:predicate lenv.
+                 (∀L1. G ⊢ ⋕⬊⬊*[h, g, T, d] L1 →
+                       (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g, T, d] L2 → (L1 ⋕[T, d] L2 → ⊥) → R L2) →
+                       R L1
+                 ) →
+                 ∀L. G ⊢ ⋕⬊⬊*[h, g, T, d] L → R L.
+#h #g #G #T #d #R #H0 #L1 #H elim H -L1
+/5 width=1 by lleq_sym, SN_intro/
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma llsxa_intro: ∀h,g,G,L1,T,d.
+                   (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g, T, d] L2 → (L1 ⋕[T, d] L2 → ⊥) → G ⊢ ⋕⬊⬊*[h, g, T, d] L2) →
+                   G ⊢ ⋕⬊⬊*[h, g, T, d] L1.
+/5 width=1 by lleq_sym, SN_intro/ qed.
+
+fact llsxa_intro_aux: ∀h,g,G,L1,T,d.
+                      (∀L,L2. ⦃G, L⦄ ⊢ ➡*[h, g, T, d] L2 → L1 ⋕[T, d] L → (L1 ⋕[T, d] L2 → ⊥) → G ⊢ ⋕⬊⬊*[h, g, T, d] L2) →
+                      G ⊢ ⋕⬊⬊*[h, g, T, d] L1.
+/4 width=3 by llsxa_intro/ qed-.
+
+lemma llsxa_llpxs_trans: ∀h,g,G,L1,T,d. G ⊢ ⋕⬊⬊*[h, g, T, d] L1 →
+                         ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g, T, d] L2 → G ⊢ ⋕⬊⬊*[h, g, T, d] L2.
+#h #g #G #L1 #T #d #H @(llsxa_ind … H) -L1 #L1 #HL1 #IHL1 #L2 #HL12 @llsxa_intro
+elim (lleq_dec T L1 L2 d) /4 width=4 by lleq_llpxs_trans, lleq_canc_sn/
+qed-.
+
+lemma llsxa_intro_llpx: ∀h,g,G,L1,T,d.
+                        (∀L2. ⦃G, L1⦄ ⊢ ➡[h, g, T, d] L2 → (L1 ⋕[T, d] L2 → ⊥) → G ⊢ ⋕⬊⬊*[h, g, T, d] L2) →
+                        G ⊢ ⋕⬊⬊*[h, g, T, d] L1.
+#h #g #G #L1 #T #d #IH @llsxa_intro_aux
+#L #L2 #H @(llpxs_ind_dx … H) -L
+[ #H destruct #H elim H //
+| #L0 #L elim (lleq_dec T L1 L d)
+  /4 width=3 by llsxa_llpxs_trans, lleq_llpx_trans/
+]
+qed.
+
+(* Main properties **********************************************************)
+
+theorem llsx_llsxa: ∀h,g,G,L,T,d. G ⊢ ⋕⬊*[h, g, T, d] L → G ⊢ ⋕⬊⬊*[h, g, T, d] L.
+#h #g #G #L #T #d #H @(llsx_ind … H) -L
+/4 width=1 by llsxa_intro_llpx/
+qed.
+
+(* Main inversion lemmas ****************************************************)
+
+theorem llsxa_inv_llsx: ∀h,g,G,L,T,d. G ⊢ ⋕⬊⬊*[h, g, T, d] L → G ⊢ ⋕⬊*[h, g, T, d] L.
+#h #g #G #L #T #d #H @(llsxa_ind … H) -L
+/4 width=1 by llsx_intro, llpx_llpxs/
+qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma llsx_intro_alt: ∀h,g,G,L1,T,d.
+                      (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g, T, d] L2 → (L1 ⋕[T, d] L2 → ⊥) → G ⊢ ⋕⬊*[h, g, T, d] L2) →
+                      G ⊢ ⋕⬊*[h, g, T, d] L1.
+/6 width=1 by llsxa_inv_llsx, llsx_llsxa, llsxa_intro/ qed.
+
+lemma llsx_llpxs_trans: ∀h,g,G,L1,T,d. G ⊢ ⋕⬊*[h, g, T, d] L1 →
+                        ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g, T, d] L2 → G ⊢ ⋕⬊*[h, g, T, d] L2.
+/4 width=3 by llsxa_inv_llsx, llsx_llsxa, llsxa_llpxs_trans/
+qed-.
+
+(* Advanced eliminators *****************************************************)
+
+lemma llsx_ind_alt: ∀h,g,G,T,d. ∀R:predicate lenv.
+                    (∀L1. G ⊢ ⋕⬊*[h, g, T, d] L1 →
+                          (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g, T, d] L2 → (L1 ⋕[T, d] L2 → ⊥) → R L2) →
+                          R L1
+                    ) →
+                    ∀L. G ⊢ ⋕⬊*[h, g, T, d] L → R L.
+#h #g #G #T #d #R #IH #L #H @(llsxa_ind h g G T d … L)
+/4 width=1 by llsxa_inv_llsx, llsx_llsxa/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/llsx_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/llsx_csx.ma
new file mode 100644
index 000000000..28a941508
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/llsx_csx.ma
@@ -0,0 +1,95 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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_llpxs.ma".
+include "basic_2/computation/llsx_ldrop.ma".
+include "basic_2/computation/llsx_llpx.ma".
+include "basic_2/computation/llsx_llpxs.ma".
+(*
+axiom cpx_llpx_trans: ∀h,g,G,L1,T1,T2. ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2 →
+                      ∀L2. ⦃G, L1⦄⊢ ➡[h, g, T2, O] L2 → 
+                      ∃∃L. ⦃G, L1⦄⊢ ➡[h, g, T1, O] L & L ⋕[T2, 0] L2.
+(*
+fact llsx_cpx_trans_aux: ∀h,g,G,L0,T1,T2. ⦃G, L0⦄ ⊢ T1 ➡[h, g] T2 →
+                         ∀L1,d. G ⊢ ⋕⬊*[h, g, T1, d] L1 → d = 0 → 
+                         L0 ⋕[T1, d] L1 → ∀L2. L1 ⋕[T2, d] L2 →
+                         G ⊢ ⋕⬊*[h, g, T2, d] L2.
+#h #g #G #L0 #T1 #T2 #HT12 #L1 #d #H @(llsx_ind … H) -L1
+#L1 #_ #IHL1 #Hd #He011 #L2 #He122 @llsx_intro
+#L3 #Hx223 #Hn223 destruct
+lapply (lleq_cpx_conf_sn … HT12 … He011) #He021
+lapply (lleq_cpx_conf … HT12 … He011) -HT12 #HT12
+lapply (lleq_llpx_trans … He122 … Hx223) -Hx223 #Hx123
+elim (cpx_llpx_trans … HT12 … Hx123) -Hx123 #L4 #Hx114 #He423
+(* lapply (lleq_cpx_conf … Hx114 … He011) #He120 *)
+@(IHL1 … Hx114) // -IHL1
+[ #HL13 @HnL2 -HnL2  
+*)
+
+fact llsx_cpx_trans_aux: ∀h,g,G,L1,T1,d. G ⊢ ⋕⬊*[h, g, T1, d] L1 → d = 0 →
+                         ∀T2. ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2 →
+                         ∀L2. L1 ⋕[T1, d] L2 → G ⊢ ⋕⬊*[h, g, T2, 0] L2.
+#h #g #G #L1 #T1 #d #H @(llsx_ind … H) -L1
+#L1 #_ #IHL1 #Hd #T2 #HT12 #L2 #He112 @llsx_intro
+#L3 #Hx223 #Hn223 destruct
+lapply (lleq_cpx_conf_sn … HT12 … He112) #He122
+lapply (lleq_cpx_conf … HT12 … He112) -HT12 #HT12
+elim (cpx_llpx_trans … HT12 … Hx223) #L4 #Hx214 #He423
+@(IHL1 … L4) //
+*)
+axiom llsx_cpx_trans_O: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 →
+                        G ⊢ ⋕⬊*[h, g, T1, 0] L → G ⊢ ⋕⬊*[h, g, T2, 0] L.
+
+(* LAZY SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS *****************)
+
+(* Advanced properties ******************************************************)
+
+lemma llsx_lref_be_lpxs: ∀h,g,I,G,K1,V,i,d. d ≤ yinj i → ⦃G, K1⦄ ⊢ ⬊*[h, g] V →
+                         ∀K2. G ⊢ ⋕⬊*[h, g, V, 0] K2 → ⦃G, K1⦄ ⊢ ➡*[h, g, V, 0] K2 →
+                         ∀L2. ⇩[i] L2 ≡ K2.ⓑ{I}V → G ⊢ ⋕⬊*[h, g, #i, d] L2.
+#h #g #I #G #K1 #V #i #d #Hdi #H @(csx_ind_alt … H) -V
+#V0 #_ #IHV0 #K2 #H @(llsx_ind … H) -K2
+#K0 #HK0 #IHK0 #HK10 #L0 #HLK0 @llsx_intro
+#L2 #HL02 #HnL02 elim (llpx_inv_lref_ge_sn … HL02 … HLK0) // -HL02
+#K2 #V2 #HLK2 #HK02 #HV02 elim (eq_term_dec V0 V2)
+#HnV02 destruct [ -IHV0 -HV02 -HK0 | -IHK0 -HnL02 -HLK0 ]
+[ /4 width=7 by llpxs_strap1, lleq_lref/
+| lapply (llpx_cpx_conf … HV02 … HK02) -HK02 #HK02
+  @(IHV0 … HnV02 … HLK2) -IHV0 -HnV02 -HLK2
+  /3 width=3 by llsx_cpx_trans_O, llpxs_cpx_conf_dx, llsx_llpx_trans, llpxs_cpx_trans, llpxs_strap1/
+]
+qed.
+
+lemma llsx_lref_be: ∀h,g,I,G,K,V,i,d. d ≤ yinj i → ⦃G, K⦄ ⊢ ⬊*[h, g] V →
+                    G ⊢ ⋕⬊*[h, g, V, 0] K →
+                    ∀L. ⇩[i] L ≡ K.ⓑ{I}V → G ⊢ ⋕⬊*[h, g, #i, d] L.
+/2 width=8 by llsx_lref_be_lpxs/ qed.
+
+(* Main properties **********************************************************)
+
+theorem csx_llsx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ∀d. G ⊢ ⋕⬊*[h, g, T, d] L.
+#h #g #G #L #T @(fqup_wf_ind_eq … G L T) -G -L -T
+#Z #Y #X #IH #G #L * * //
+[ #i #HG #HL #HT #H #d destruct
+  elim (lt_or_ge i (|L|)) /2 width=1 by llsx_lref_free/
+  elim (ylt_split i d) /2 width=1 by llsx_lref_skip/
+  #Hdi #Hi elim (ldrop_O1_lt … Hi) -Hi
+  #I #K #V #HLK lapply (csx_inv_lref_bind … HLK … H) -H
+  /4 width=6 by llsx_lref_be, fqup_lref/
+| #a #I #V #T #HG #HL #HT #H #d destruct
+  elim (csx_fwd_bind … H) -H /3 width=1 by llsx_bind/
+| #I #V #T #HG #HL #HT #H #d destruct
+  elim (csx_fwd_flat … H) -H /3 width=1 by llsx_flat/
+]
+qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/llsx_ldrop.ma
similarity index 62%
rename from matita/matita/contribs/lambdadelta/basic_2/computation/lprs_ldrop.ma
rename to matita/matita/contribs/lambdadelta/basic_2/computation/llsx_ldrop.ma
index f03d3f0e8..2d16e3240 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/llsx_ldrop.ma
@@ -12,18 +12,21 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/reduction/lpr_ldrop.ma".
-include "basic_2/computation/lprs.ma".
+include "basic_2/substitution/lleq_ldrop.ma".
+include "basic_2/computation/llsx.ma".
 
-(* SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ****************************)
+(* LAZY SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS *****************)
 
-(* Properies on local environment slicing ***********************************)
+(* Advanced properties ******************************************************)
 
-lemma lprs_ldrop_conf: ∀G. dropable_sn (lprs G).
-/3 width=3 by dropable_sn_TC, lpr_ldrop_conf/ qed-.
+lemma llsx_lref_free: ∀h,g,G,L,d,i. |L| ≤ i → G ⊢ ⋕⬊*[h, g, #i, d] L.
+#h #g #G #L1 #d #i #HL1 @llsx_intro
+#L2 #HL12 #H elim H -H
+/4 width=8 by llpx_fwd_length, lleq_free, le_repl_sn_conf_aux/
+qed.
 
-lemma ldrop_lprs_trans: ∀G. dedropable_sn (lprs G).
-/3 width=3 by dedropable_sn_TC, ldrop_lpr_trans/ qed-.
-
-lemma lprs_ldrop_trans_O1: ∀G. dropable_dx (lprs G).
-/3 width=3 by dropable_dx_TC, lpr_ldrop_trans_O1/ qed-.
+lemma llsx_lref_skip: ∀h,g,G,L,d,i. yinj i < d → G ⊢ ⋕⬊*[h, g, #i, d] L.
+#h #g #G #L1 #d #i #HL1 @llsx_intro
+#L2 #HL12 #H elim H -H
+/3 width=6 by llpx_fwd_length, lleq_skip/
+qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_lprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/llsx_llpx.ma
similarity index 67%
rename from matita/matita/contribs/lambdadelta/basic_2/computation/lprs_lprs.ma
rename to matita/matita/contribs/lambdadelta/basic_2/computation/llsx_llpx.ma
index 1da198d4e..9392afba2 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_lprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/llsx_llpx.ma
@@ -12,20 +12,16 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/reduction/lpr_lpr.ma".
-include "basic_2/computation/lprs.ma".
+include "basic_2/substitution/lleq_lleq.ma".
+include "basic_2/reduction/llpx_lleq.ma".
+include "basic_2/computation/llsx.ma".
 
-(* SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ****************************)
+(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************)
 
 (* Advanced properties ******************************************************)
 
-lemma lprs_strip: ∀G. confluent2 … (lprs G) (lpr G).
-/3 width=3 by TC_strip1, lpr_conf/ qed-.
-
-(* Main properties **********************************************************)
-
-theorem lprs_conf: ∀G. confluent2 … (lprs G) (lprs G).
-/3 width=3 by TC_confluent2, lpr_conf/ qed-.
-
-theorem lprs_trans: ∀G. Transitive … (lprs G).
-/2 width=3/ qed-.
+lemma llsx_llpx_trans: ∀h,g,G,L1,T,d. G ⊢ ⋕⬊*[h, g, T, d] L1 →
+                       ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g, T, d] L2 → G ⊢ ⋕⬊*[h, g, T, d] L2.
+#h #g #G #L1 #T #d #H @(llsx_ind … H) -L1 #L1 #HL1 #IHL1 #L2 #HL12 @llsx_intro
+elim (lleq_dec T L1 L2 d) /4 width=4 by lleq_llpx_trans, lleq_canc_sn/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/llsx_llpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/llsx_llpxs.ma
new file mode 100644
index 000000000..af37a372f
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/llsx_llpxs.ma
@@ -0,0 +1,66 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/computation/llpxs_llpxs.ma".
+include "basic_2/computation/llsx_alt.ma".
+
+(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************)
+
+(* Advanced properties ******************************************************)
+
+fact llsx_bind_llpxs_aux: ∀h,g,a,I,G,L1,V,d. G ⊢ ⋕⬊*[h, g, V, d] L1 →
+                          ∀Y,T. G ⊢ ⋕⬊*[h, g, T, ⫯d] Y →
+                          ∀L2. Y = L2.ⓑ{I}V → ⦃G, L1⦄ ⊢ ➡*[h, g, ⓑ{a,I}V.T, d] L2 →
+                          G ⊢ ⋕⬊*[h, g, ⓑ{a,I}V.T, d] L2.
+#h #g #a #I #G #L1 #V #d #H @(llsx_ind_alt … H) -L1
+#L1 #HL1 #IHL1 #Y #T #H @(llsx_ind_alt … H) -Y
+#Y #HY #IHY #L2 #H #HL12 destruct @llsx_intro_alt
+#L0 #HL20 lapply (llpxs_fwd_bind_dx … HL20)
+lapply (llpxs_trans … HL12 … HL20)
+#HL10 #HT #H elim (nlleq_inv_bind … H) -H [ -HL1 -IHY | -HY -IHL1 ]
+[ #HnV elim (lleq_dec V L1 L2 d)
+  [  -HL20 #HV @(IHL1 … L0)
+     /3 width=4 by llsx_llpxs_trans, llpxs_fwd_bind_sn, lleq_canc_sn/ (**) (* full auto too slow *)
+  | -HnV -HL10
+     /3 width=4 by llsx_llpxs_trans, llpxs_fwd_bind_sn/
+  ]
+| /3 width=4 by/
+]
+qed-.
+
+lemma llsx_bind: ∀h,g,a,I,G,L,V,d. G ⊢ ⋕⬊*[h, g, V, d] L →
+                 ∀T. G ⊢ ⋕⬊*[h, g, T, ⫯d] L.ⓑ{I}V →
+                 G ⊢ ⋕⬊*[h, g, ⓑ{a,I}V.T, d] L.
+/2 width=3 by llsx_bind_llpxs_aux/ qed.
+
+lemma llsx_flat_llpxs: ∀h,g,I,G,L1,V,d. G ⊢ ⋕⬊*[h, g, V, d] L1 →
+                       ∀L2,T. G ⊢ ⋕⬊*[h, g, T, d] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g, ⓕ{I}V.T, d] L2 →
+                       G ⊢ ⋕⬊*[h, g, ⓕ{I}V.T, d] L2.
+#h #g #I #G #L1 #V #d #H @(llsx_ind_alt … H) -L1
+#L1 #HL1 #IHL1 #L2 #T #H @(llsx_ind_alt … H) -L2
+#L2 #HL2 #IHL2 #HL12 @llsx_intro_alt
+#L0 #HL20 lapply (llpxs_fwd_flat_dx … HL20)
+lapply (llpxs_trans … HL12 … HL20)
+#HL10 #HT #H elim (nlleq_inv_flat … H) -H [ -HL1 -IHL2 | -HL2 -IHL1 ]
+[ #HnV elim (lleq_dec V L1 L2 d)
+  [ #HV @(IHL1 … L0) /3 width=3 by llsx_llpxs_trans, llpxs_fwd_flat_sn, lleq_canc_sn/ (**) (* full auto too slow: 47s *)
+  | -HnV -HL10 /3 width=4 by llsx_llpxs_trans, llpxs_fwd_flat_sn/
+  ]
+| /3 width=1 by/
+]
+qed-.
+
+lemma llsx_flat: ∀h,g,I,G,L,V,d. G ⊢ ⋕⬊*[h, g, V, d] L →
+                 ∀T. G ⊢ ⋕⬊*[h, g, T, d] L → G ⊢ ⋕⬊*[h, g, ⓕ{I}V.T, d] L.
+/2 width=3 by llsx_flat_llpxs/ qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs.ma
deleted file mode 100644
index 6e8431959..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs.ma
+++ /dev/null
@@ -1,71 +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_3.ma".
-include "basic_2/grammar/lpx_sn_tc.ma".
-include "basic_2/reduction/lpr.ma".
-
-(* SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ****************************)
-
-definition lprs: relation3 genv lenv lenv ≝
-                 λG. TC … (lpr G).
-
-interpretation "parallel computation (local environment, sn variant)"
-   'PRedSnStar G L1 L2 = (lprs G L1 L2).
-
-(* Basic eliminators ********************************************************)
-
-lemma lprs_ind: ∀G,L1. ∀R:predicate lenv. R L1 →
-                (∀L,L2. ⦃G, L1⦄ ⊢ ➡* L → ⦃G, L⦄ ⊢ ➡ L2 → R L → R L2) →
-                ∀L2. ⦃G, L1⦄ ⊢ ➡* L2 → R L2.
-#G #L1 #R #HL1 #IHL1 #L2 #HL12
-@(TC_star_ind … HL1 IHL1 … HL12) //
-qed-.
-
-lemma lprs_ind_dx: ∀G,L2. ∀R:predicate lenv. R L2 →
-                   (∀L1,L. ⦃G, L1⦄ ⊢ ➡ L → ⦃G, L⦄ ⊢ ➡* L2 → R L → R L1) →
-                   ∀L1. ⦃G, L1⦄ ⊢ ➡* L2 → R L1.
-#G #L2 #R #HL2 #IHL2 #L1 #HL12
-@(TC_star_ind_dx … HL2 IHL2 … HL12) //
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma lpr_lprs: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L1⦄ ⊢ ➡* L2.
-/2 width=1/ qed.
-
-lemma lprs_refl: ∀G,L. ⦃G, L⦄ ⊢ ➡* L.
-/2 width=1/ qed.
-
-lemma lprs_strap1: ∀G,L1,L,L2. ⦃G, L1⦄ ⊢ ➡* L → ⦃G, L⦄ ⊢ ➡ L2 → ⦃G, L1⦄ ⊢ ➡* L2.
-/2 width=3/ qed.
-
-lemma lprs_strap2: ∀G,L1,L,L2. ⦃G, L1⦄ ⊢ ➡ L → ⦃G, L⦄ ⊢ ➡* L2 → ⦃G, L1⦄ ⊢ ➡* L2.
-/2 width=3/ qed.
-
-lemma lprs_pair_refl: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → ∀I,V. ⦃G, L1.ⓑ{I}V⦄ ⊢ ➡* L2.ⓑ{I}V.
-/2 width=1 by TC_lpx_sn_pair_refl/ qed.
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma lprs_inv_atom1: ∀G,L2. ⦃G, ⋆⦄ ⊢ ➡* L2 → L2 = ⋆.
-/2 width=2 by TC_lpx_sn_inv_atom1/ qed-.
-
-lemma lprs_inv_atom2: ∀G,L1. ⦃G, L1⦄ ⊢ ➡* ⋆ → L1 = ⋆.
-/2 width=2 by TC_lpx_sn_inv_atom2/ qed-.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma lprs_fwd_length: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → |L1| = |L2|.
-/2 width=2 by TC_lpx_sn_fwd_length/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_alt.ma
deleted file mode 100644
index 315ee8f7a..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_alt.ma
+++ /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_3.ma".
-include "basic_2/computation/cprs_cprs.ma".
-include "basic_2/computation/lprs.ma".
-
-(* SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ****************************)
-
-(* alternative definition *)
-definition lprsa: relation3 genv lenv lenv ≝
-           λG. lpx_sn … (cprs G).
-
-interpretation "parallel computation (local environment, sn variant) alternative"
-   'PRedSnStarAlt G L1 L2 = (lprsa G L1 L2).
-
-(* Main properties on the alternative definition ****************************)
-
-theorem lprsa_lprs: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡➡* L2 → ⦃G, L1⦄ ⊢ ➡* L2.
-/2 width=1 by lpx_sn_LTC_TC_lpx_sn/ qed-.
-
-(* Main inversion lemmas on the alternative definition **********************)
-
-theorem lprs_inv_lprsa: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L1⦄ ⊢ ➡➡* L2.
-/3 width=3 by TC_lpx_sn_inv_lpx_sn_LTC, lpr_cprs_trans/ qed-.
-
-(* Alternative eliminators **************************************************)
-
-lemma lprs_ind_alt: ∀G. ∀R:relation lenv.
-                    R (⋆) (⋆) → (
-                       ∀I,K1,K2,V1,V2.
-                       ⦃G, K1⦄ ⊢ ➡* K2 → ⦃G, K1⦄ ⊢ V1 ➡* V2 →
-                       R K1 K2 → R (K1.ⓑ{I}V1) (K2.ⓑ{I}V2)
-                    ) →
-                    ∀L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → R L1 L2.
-/3 width=4 by TC_lpx_sn_ind, lpr_cprs_trans/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_cprs.ma
deleted file mode 100644
index 70345be5c..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_cprs.ma
+++ /dev/null
@@ -1,136 +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/cprs_cprs.ma".
-include "basic_2/computation/lprs.ma".
-
-(* SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ****************************)
-
-(* Advanced properties ******************************************************)
-
-lemma lprs_pair: ∀I,G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 →
-                 ∀V1,V2. ⦃G, L1⦄ ⊢ V1 ➡* V2 → ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡* L2.ⓑ{I}V2.
-/2 width=1 by TC_lpx_sn_pair/ qed.
-
-(* Advanced inversion lemmas ************************************************)
-
-lemma lprs_inv_pair1: ∀I,G,K1,L2,V1. ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡* L2 →
-                      ∃∃K2,V2. ⦃G, K1⦄ ⊢ ➡* K2 & ⦃G, K1⦄ ⊢ V1 ➡* V2 &
-                               L2 = K2.ⓑ{I}V2.
-/3 width=3 by TC_lpx_sn_inv_pair1, lpr_cprs_trans/ qed-.
-
-lemma lprs_inv_pair2: ∀I,G,L1,K2,V2. ⦃G, L1⦄ ⊢ ➡* K2.ⓑ{I}V2 →
-                      ∃∃K1,V1. ⦃G, K1⦄ ⊢ ➡* K2 & ⦃G, K1⦄ ⊢ V1 ➡* V2 &
-                               L1 = K1.ⓑ{I}V1.
-/3 width=3 by TC_lpx_sn_inv_pair2, lpr_cprs_trans/ qed-.
-
-(* Properties on context-sensitive parallel computation for terms ***********)
-
-lemma lprs_cpr_trans: ∀G. s_r_trans … (cpr G) (lprs G).
-/3 width=5 by s_r_trans_TC2, lpr_cprs_trans/ qed-.
-
-(* Basic_1: was just: pr3_pr3_pr3_t *)
-lemma lprs_cprs_trans: ∀G. s_rs_trans … (cpr G) (lprs G).
-/3 width=5 by s_r_trans_TC1, lprs_cpr_trans/ qed-.
-
-lemma lprs_cprs_conf_dx: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡* T1 →
-                         ∀L1. ⦃G, L0⦄ ⊢ ➡* L1 →
-                         ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡* T & ⦃G, L1⦄ ⊢ T0 ➡* T.
-#G #L0 #T0 #T1 #HT01 #L1 #H elim H -L1
-[ #L1 #HL01
-  elim (cprs_lpr_conf_dx … HT01 … HL01) -L0 /2 width=3 by ex2_intro/
-| #L #L1 #_ #HL1 * #T #HT1 #HT0 -L0
-  elim (cprs_lpr_conf_dx … HT1 … HL1) -HT1 #T2 #HT2 #HT12
-  elim (cprs_lpr_conf_dx … HT0 … HL1) -L #T3 #HT3 #HT03
-  elim (cprs_conf … HT2 … HT3) -T #T #HT2 #HT3
-  lapply (cprs_trans … HT03 … HT3) -T3
-  lapply (cprs_trans … HT12 … HT2) -T2 /2 width=3 by ex2_intro/
-]
-qed-.
-
-lemma lprs_cpr_conf_dx: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡ T1 →
-                        ∀L1. ⦃G, L0⦄ ⊢ ➡* L1 →
-                        ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡* T & ⦃G, L1⦄ ⊢ T0 ➡* T.
-/3 width=3 by lprs_cprs_conf_dx, cpr_cprs/ qed-.
-
-lemma lprs_cprs_conf_sn: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡* T1 →
-                         ∀L1. ⦃G, L0⦄ ⊢ ➡* L1 →
-                         ∃∃T. ⦃G, L0⦄ ⊢ T1 ➡* T & ⦃G, L1⦄ ⊢ T0 ➡* T.
-#G #L0 #T0 #T1 #HT01 #L1 #HL01
-elim (lprs_cprs_conf_dx … HT01 … HL01) -HT01 #T #HT1
-lapply (lprs_cprs_trans … HT1 … HL01) -HT1 /2 width=3 by ex2_intro/
-qed-.
-
-lemma lprs_cpr_conf_sn: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡ T1 →
-                        ∀L1. ⦃G, L0⦄ ⊢ ➡* L1 →
-                        ∃∃T. ⦃G, L0⦄ ⊢ T1 ➡* T & ⦃G, L1⦄ ⊢ T0 ➡* T.
-/3 width=3 by lprs_cprs_conf_sn, cpr_cprs/ qed-.
-
-lemma cprs_bind2: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡* V2 →
-                  ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ➡* T2 →
-                  ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡* ⓑ{a,I}V2.T2.
-#G #L #V1 #V2 #HV12 #I #T1 #T2 #HT12
-lapply (lprs_cprs_trans … HT12 (L.ⓑ{I}V1) ?) /2 width=1 by lprs_pair, cprs_bind/
-qed.
-
-(* Inversion lemmas on context-sensitive parallel computation for terms *****)
-
-(* Basic_1: was: pr3_gen_abst *)
-lemma cprs_inv_abst1: ∀a,G,L,W1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{a}W1.T1 ➡* U2 →
-                      ∃∃W2,T2. ⦃G, L⦄ ⊢ W1 ➡* W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ➡* T2 &
-                               U2 = ⓛ{a}W2.T2.
-#a #G #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /2 width=5 by ex3_2_intro/
-#U0 #U2 #_ #HU02 * #V0 #T0 #HV10 #HT10 #H destruct
-elim (cpr_inv_abst1 … HU02) -HU02 #V2 #T2 #HV02 #HT02 #H destruct
-lapply (lprs_cpr_trans … HT02 (L.ⓛV1) ?) /2 width=1 by lprs_pair/ -HT02 #HT02
-lapply (cprs_strap1 … HV10 … HV02) -V0
-lapply (cprs_trans … HT10 … HT02) -T0 /2 width=5 by ex3_2_intro/
-qed-.
-
-lemma cprs_inv_abst: ∀a,G,L,W1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓛ{a}W1.T1 ➡* ⓛ{a}W2.T2 →
-                     ⦃G, L⦄ ⊢ W1 ➡* W2 ∧ ⦃G, L.ⓛW1⦄ ⊢ T1 ➡* T2.
-#a #G #L #W1 #W2 #T1 #T2 #H
-elim (cprs_inv_abst1 … H) -H #W #T #HW1 #HT1 #H destruct /2 width=1 by conj/
-qed-.
-
-(* Basic_1: was pr3_gen_abbr *)
-lemma cprs_inv_abbr1: ∀a,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{a}V1.T1 ➡* U2 → (
-                      ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡* V2 & ⦃G, L.ⓓV1⦄ ⊢ T1 ➡* T2 &
-                               U2 = ⓓ{a}V2.T2
-                      ) ∨
-                      ∃∃T2. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡* T2 & ⇧[0, 1] U2 ≡ T2 & a = true.
-#a #G #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5 by ex3_2_intro, or_introl/
-#U0 #U2 #_ #HU02 * *
-[ #V0 #T0 #HV10 #HT10 #H destruct
-  elim (cpr_inv_abbr1 … HU02) -HU02 *
-  [ #V2 #T2 #HV02 #HT02 #H destruct
-    lapply (lprs_cpr_trans … HT02 (L.ⓓV1) ?) /2 width=1 by lprs_pair/ -HT02 #HT02
-    lapply (cprs_strap1 … HV10 … HV02) -V0
-    lapply (cprs_trans … HT10 … HT02) -T0 /3 width=5 by ex3_2_intro, or_introl/
-  | #T2 #HT02 #HUT2
-    lapply (lprs_cpr_trans … HT02 (L.ⓓV1) ?) -HT02 /2 width=1 by lprs_pair/ -V0 #HT02
-    lapply (cprs_trans … HT10 … HT02) -T0 /3 width=3 by ex3_intro, or_intror/
-  ]
-| #U1 #HTU1 #HU01
-  elim (lift_total U2 0 1) #U #HU2
-  lapply (cpr_lift … HU02 (L.ⓓV1) … HU01 … HU2) -U0
-  /4 width=3 by cprs_strap1, ldrop_drop, ex3_intro, or_intror/
-]
-qed-.
-
-(* More advanced properties *************************************************)
-
-lemma lprs_pair2: ∀I,G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 →
-                  ∀V1,V2. ⦃G, L2⦄ ⊢ V1 ➡* V2 → ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡* L2.ⓑ{I}V2.
-/3 width=3 by lprs_pair, lprs_cprs_trans/ qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs.ma
deleted file mode 100644
index 35a8cb482..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs.ma
+++ /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/computation/lpxs_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_alt.ma
deleted file mode 100644
index 8a6b30a57..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_alt.ma
+++ /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/computation/lpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma
deleted file mode 100644
index 2f21a8d70..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma
+++ /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/computation/lpxs_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_ldrop.ma
deleted file mode 100644
index d8c489017..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_ldrop.ma
+++ /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/computation/lpxs_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma
deleted file mode 100644
index e21c79912..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma
+++ /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/computation/fpbc_fpns.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/fpbc_fpns.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fpns.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/fpbc_fpns.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpns.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/fpbg_fpns.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpns.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/fpbg_fpns.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpns.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/fpbs_fpns.etc
similarity index 96%
rename from matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpns.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/fpbs_fpns.etc
index 2006ef222..fff178ef8 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpns.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/fpbs_fpns.etc
@@ -21,5 +21,5 @@ include "basic_2/computation/fpbs.ma".
 
 lemma fpns_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2.
                  ⦃G1, L1, T1⦄ ⊢ ⋕➡*[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 * /2 width=1 by lpxs_fpbs/
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 * /2 width=1 by llpxs_fpbs/
 qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazycosn_5.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lazycosn_5.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazycosn_5.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lazycosn_5.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lcosx.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lcosx.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/computation/lcosx.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lcosx.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lcosx_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lcosx_cpxs.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/computation/lcosx_cpxs.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lcosx_cpxs.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lsx.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lsx.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lsx_csx.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/computation/lsx_csx.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lsx_csx.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lsx_ldrop.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/computation/lsx_ldrop.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lsx_ldrop.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lsx_lpxs.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpxs.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lsx_lpxs.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazysnalt_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazysnalt_6.ma
new file mode 100644
index 000000000..0976a3136
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazysnalt_6.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 T , break term 46 d ] break term 46 L )"
+   non associative with precedence 45
+   for @{ 'LazySNAlt $h $g $T $d $G $L }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma
index b34d4e955..a6afafbdb 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma
@@ -43,6 +43,10 @@ lemma lleq_cpx_trans: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 →
 ]
 qed-.
 
+lemma lleq_cpx_conf: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 →
+                     ∀L1. L2 ⋕[T1, 0] L1 → ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2.
+/3 width=3 by lleq_cpx_trans, lleq_sym/ qed-.
+
 lemma lleq_cpx_conf_sn: ∀h,g,G. s_r_confluent1 … (cpx h g G) (lleq 0).
 /3 width=6 by llpx_sn_cpx_conf, lift_mono, ex2_intro/ qed-.
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx.ma
index ef71c6515..17bcd5a7a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx.ma
@@ -43,6 +43,21 @@ lemma llpx_fwd_pair_sn: ∀h,g,I,G,L1,L2,V,T,d. ⦃G, L1⦄ ⊢ ➡[h, g, ②{I}
                         ⦃G, L1⦄ ⊢ ➡[h, g, V, d] L2.
 /2 width=3 by llpx_sn_fwd_pair_sn/ qed-.
 
+(* Note: this might be removed *)
+lemma llpx_fwd_bind_sn: ∀h,g,a,I,G,L1,L2,V,T,d. ⦃G, L1⦄ ⊢ ➡[h, g, ⓑ{a,I}V.T, d] L2 →
+                        ⦃G, L1⦄ ⊢ ➡[h, g, V, d] L2.
+/2 width=4 by llpx_sn_fwd_bind_sn/ qed-.
+
+(* Note: this might be removed *)
+lemma llpx_fwd_bind_dx: ∀h,g,a,I,G,L1,L2,V,T,d. ⦃G, L1⦄ ⊢ ➡[h, g, ⓑ{a,I}V.T, d] L2 →
+                        ⦃G, L1.ⓑ{I}V⦄ ⊢ ➡[h, g, T, ⫯d] L2.ⓑ{I}V.
+/2 width=2 by llpx_sn_fwd_bind_dx/ qed-.
+
+(* Note: this might be removed *)
+lemma llpx_fwd_flat_sn: ∀h,g,I,G,L1,L2,V,T,d. ⦃G, L1⦄ ⊢ ➡[h, g, ⓕ{I}V.T, d] L2 →
+                        ⦃G, L1⦄ ⊢ ➡[h, g, V, d] L2.
+/2 width=3 by llpx_sn_fwd_flat_sn/ qed-.
+
 (* Basic properties *********************************************************)
 
 lemma llpx_lref: ∀h,g,I,G,L1,L2,K1,K2,V1,V2,d,i. d ≤ yinj i →
-- 
2.39.2