From 0679e5d5a305a43a8b4b01a5ac4c7caffacc73b9 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 5 May 2013 18:16:14 +0000
Subject: [PATCH] - partial commit (just the components before computation) -
 we park head normal forms for the moment - some refactoring

---
 .../cpr/ldrop_lbotr.etc}                      |   0
 .../ldrop_lpx.ma => etc/cpr/ldrop_lpx.etc}    |   0
 .../lenv_px.ma => etc/cpr/lenv_px.etc}        |   0
 .../basic_2/etc/cpr/lfprs_ltprs.etc           |  23 +++
 .../lambdadelta/basic_2/etc/cpr/lift.etc      |  25 ++++
 .../lsubr.ma => etc/cpr/lsubr.etc}            |   4 +
 .../cpr/lsubr_lbotr.etc}                      |   4 +
 .../lambdadelta/basic_2/etc/cpr/ltprs.etc     |  90 ++++++++++++
 .../lambdadelta/basic_2/etc/cpr/ltprs_alt.etc |  38 +++++
 .../basic_2/etc/cpr/ltprs_ldrop.etc           |  27 ++++
 .../basic_2/etc/cpr/ltprs_ltprs.etc           |  32 ++++
 .../lambdadelta/basic_2/etc/cpr/tprs.etc      |  94 ++++++++++++
 .../lambdadelta/basic_2/etc/cpr/tprs_lift.etc |  43 ++++++
 .../lambdadelta/basic_2/etc/cpr/tprs_tprs.etc |  43 ++++++
 .../basic_2/etc/delift/cprs_delift.etc        |  37 +++++
 .../lambdadelta/basic_2/etc/fpr/fprs.etc      |  58 ++++++++
 .../lambdadelta/basic_2/etc/fpr/fprs_aaa.etc  |  26 ++++
 .../lambdadelta/basic_2/etc/fpr/fprs_cprs.etc | 138 ++++++++++++++++++
 .../lambdadelta/basic_2/etc/fpr/fprs_fprs.etc |  34 +++++
 .../lenv_px_bi.ma => etc/fpr/lenv_px_bi.etc}  |   0
 .../basic_2/etc/fpr/lfprs_fprs.etc            |  41 ++++++
 .../{reduction/chnf.ma => etc/tshf/chnf.etc}  |   4 +
 .../cpr_tshf.ma => etc/tshf/cpr_tshf.etc}     |   0
 .../{grammar/tshf.ma => etc/tshf/tshf.etc}    |  12 ++
 .../grammar/{lenv_px_sn.ma => lpx_sn.ma}      |  31 ----
 .../basic_2/grammar/lpx_sn_lpx_sn.ma          |  48 ++++++
 .../lambdadelta/basic_2/grammar/lpx_sn_tc.ma  | 122 ++++++++++++++++
 .../contribs/lambdadelta/basic_2/notation.ma  |  54 +------
 .../lambdadelta/basic_2/reduction/cpr.ma      |   9 +-
 .../lambdadelta/basic_2/reduction/lpr.ma      |   4 +
 .../lambdadelta/basic_2/reduction/lpr_cpr.ma  |   1 +
 .../lambdadelta/basic_2/reduction/lpr_cpss.ma |   1 +
 .../lambdadelta/basic_2/relocation/ldrop.ma   |  52 +++----
 .../basic_2/relocation/ldrop_lpx_sn.ma        |   2 +-
 .../lambdadelta/basic_2/relocation/lift.ma    |  26 ----
 .../lambdadelta/basic_2/substitution/cpss.ma  |  14 +-
 .../lambdadelta/basic_2/substitution/lpss.ma  |   6 +-
 .../basic_2/substitution/lpss_cpss.ma         |   1 +
 .../lambdadelta/basic_2/substitution/lsubr.ma | 111 ++++++++++++++
 .../basic_2/substitution/lsubr_lsubr.ma       |  64 ++++++++
 .../lambdadelta/basic_2/unfold/cpqs.ma        |   9 +-
 .../lambdadelta/basic_2/unfold/lpqs.ma        |   4 +
 .../lambdadelta/basic_2/unfold/lpqs_cpqs.ma   |   1 +
 .../lambdadelta/basic_2/web/basic_2_src.tbl   |  27 ++--
 .../contribs/lambdadelta/ground_2/star.ma     |  25 +++-
 45 files changed, 1206 insertions(+), 179 deletions(-)
 rename matita/matita/contribs/lambdadelta/basic_2/{relocation/ldrop_lbotr.ma => etc/cpr/ldrop_lbotr.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{relocation/ldrop_lpx.ma => etc/cpr/ldrop_lpx.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{grammar/lenv_px.ma => etc/cpr/lenv_px.etc} (100%)
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/cpr/lfprs_ltprs.etc
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/cpr/lift.etc
 rename matita/matita/contribs/lambdadelta/basic_2/{relocation/lsubr.ma => etc/cpr/lsubr.etc} (97%)
 rename matita/matita/contribs/lambdadelta/basic_2/{relocation/lsubr_lbotr.ma => etc/cpr/lsubr_lbotr.etc} (95%)
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltprs.etc
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltprs_alt.etc
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltprs_ldrop.etc
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltprs_ltprs.etc
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tprs.etc
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tprs_lift.etc
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tprs_tprs.etc
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/delift/cprs_delift.etc
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fprs.etc
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fprs_aaa.etc
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fprs_cprs.etc
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fprs_fprs.etc
 rename matita/matita/contribs/lambdadelta/basic_2/{grammar/lenv_px_bi.ma => etc/fpr/lenv_px_bi.etc} (100%)
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/fpr/lfprs_fprs.etc
 rename matita/matita/contribs/lambdadelta/basic_2/{reduction/chnf.ma => etc/tshf/chnf.etc} (92%)
 rename matita/matita/contribs/lambdadelta/basic_2/{reduction/cpr_tshf.ma => etc/tshf/cpr_tshf.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{grammar/tshf.ma => etc/tshf/tshf.etc} (90%)
 rename matita/matita/contribs/lambdadelta/basic_2/grammar/{lenv_px_sn.ma => lpx_sn.ma} (76%)
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn_lpx_sn.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn_tc.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr_lsubr.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lbotr.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ldrop_lbotr.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lbotr.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ldrop_lbotr.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ldrop_lpx.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lpx.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ldrop_lpx.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_px.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/lenv_px.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_px.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpr/lenv_px.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/lfprs_ltprs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/lfprs_ltprs.etc
new file mode 100644
index 000000000..99ae801d7
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/lfprs_ltprs.etc
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/ltprs.ma".
+include "basic_2/computation/lfprs.ma".
+
+(* FOCALIZED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *********************)
+
+(* Properties on context-free parallel computation for local environments ***)
+
+lemma ltprs_lfprs: ∀L1,L2. L1 ➡* L2 → ⦃L1⦄ ➡* ⦃L2⦄.
+/3 width=3/ qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/lift.etc
new file mode 100644
index 000000000..f0d631ebb
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/lift.etc
@@ -0,0 +1,25 @@
+definition t_liftable: relation term → Prop ≝
+                       λR. ∀T1,T2. R T1 T2 → ∀U1,d,e. ⇧[d, e] T1 ≡ U1 →
+                       ∀U2. ⇧[d, e] T2 ≡ U2 → R U1 U2.
+
+definition t_deliftable_sn: relation term → Prop ≝
+                            λR. ∀U1,U2. R U1 U2 → ∀T1,d,e. ⇧[d, e] T1 ≡ U1 →
+                            ∃∃T2. ⇧[d, e] T2 ≡ U2 & R T1 T2.
+
+lemma t_liftable_TC: ∀R. t_liftable R → t_liftable (TC … R).
+#R #HR #T1 #T2 #H elim H -T2
+[ /3 width=7/
+| #T #T2 #_ #HT2 #IHT1 #U1 #d #e #HTU1 #U2 #HTU2
+  elim (lift_total T d e) /3 width=9/
+]
+qed.
+
+lemma t_deliftable_sn_TC: ∀R. t_deliftable_sn R → t_deliftable_sn (TC … R).
+#R #HR #U1 #U2 #H elim H -U2
+[ #U2 #HU12 #T1 #d #e #HTU1
+  elim (HR … HU12 … HTU1) -U1 /3 width=3/
+| #U #U2 #_ #HU2 #IHU1 #T1 #d #e #HTU1
+  elim (IHU1 … HTU1) -U1 #T #HTU #HT1
+  elim (HR … HU2 … HTU) -U /3 width=5/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/lsubr.etc
similarity index 97%
rename from matita/matita/contribs/lambdadelta/basic_2/relocation/lsubr.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpr/lsubr.etc
index 89359533a..8655a5e54 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lsubr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/lsubr.etc
@@ -12,6 +12,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
+notation "hvbox( L1 break ⊑ [ term 46 d , break term 46 e ] break term 46 L2 )"
+   non associative with precedence 45
+   for @{ 'SubEq $L1 $d $e $L2 }.
+
 include "basic_2/grammar/lenv_length.ma".
 
 (* LOCAL ENVIRONMENT REFINEMENT FOR SUBSTITUTION ****************************)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lsubr_lbotr.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/lsubr_lbotr.etc
similarity index 95%
rename from matita/matita/contribs/lambdadelta/basic_2/relocation/lsubr_lbotr.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpr/lsubr_lbotr.etc
index 26a9530d0..b95a19b66 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lsubr_lbotr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/lsubr_lbotr.etc
@@ -12,6 +12,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
+notation "hvbox( ⊒ [ term 46 d , break term 46 e ] break term 46 L2 )"
+   non associative with precedence 45
+   for @{ 'SubEqBottom $d $e $L2 }.
+
 include "basic_2/relocation/lsubr.ma".
 
 (* LOCAL ENVIRONMENT REFINEMENT FOR SUBSTITUTION ****************************)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltprs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltprs.etc
new file mode 100644
index 000000000..8e0c32e26
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltprs.etc
@@ -0,0 +1,90 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/reducibility/ltpr.ma".
+include "basic_2/computation/tprs.ma".
+
+(* CONTEXT-FREE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ******************)
+
+definition ltprs: relation lenv ≝ TC … ltpr.
+
+interpretation
+  "context-free parallel computation (environment)"
+  'PRedStar L1 L2 = (ltprs L1 L2).
+
+(* Basic eliminators ********************************************************)
+
+lemma ltprs_ind: ∀L1. ∀R:predicate lenv. R L1 →
+                 (∀L,L2. L1 ➡* L → L ➡ L2 → R L → R L2) →
+                 ∀L2. L1 ➡* L2 → R L2.
+#L1 #R #HL1 #IHL1 #L2 #HL12
+@(TC_star_ind … HL1 IHL1 … HL12) //
+qed-.
+
+lemma ltprs_ind_dx: ∀L2. ∀R:predicate lenv. R L2 →
+                    (∀L1,L. L1 ➡ L → L ➡* L2 → R L → R L1) →
+                    ∀L1. L1 ➡* L2 → R L1.
+#L2 #R #HL2 #IHL2 #L1 #HL12
+@(TC_star_ind_dx … HL2 IHL2 … HL12) //
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma ltprs_refl: reflexive … ltprs.
+/2 width=1/ qed.
+
+lemma ltpr_ltprs: ∀L1,L2. L1 ➡ L2 → L1 ➡* L2.
+/2 width=1/ qed.
+
+lemma ltprs_strap1: ∀L1,L,L2. L1 ➡* L → L ➡ L2 → L1 ➡* L2.
+/2 width=3/ qed.
+
+lemma ltprs_strap2: ∀L1,L,L2. L1 ➡ L → L ➡* L2 → L1 ➡* L2.
+/2 width=3/ qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma ltprs_inv_atom1: ∀L2. ⋆ ➡* L2 → L2 = ⋆.
+#L2 #H @(ltprs_ind … H) -L2 //
+#L #L2 #_ #HL2 #IHL1 destruct
+>(ltpr_inv_atom1 … HL2) -L2 //
+qed-.
+
+lemma ltprs_inv_pair1: ∀I,K1,L2,V1. K1. ⓑ{I} V1 ➡* L2 →
+                       ∃∃K2,V2. K1 ➡* K2 & V1 ➡* V2 & L2 = K2. ⓑ{I} V2.
+#I #K1 #L2 #V1 #H @(ltprs_ind … H) -L2 /2 width=5/
+#L #L2 #_ #HL2 * #K #V #HK1 #HV1 #H destruct
+elim (ltpr_inv_pair1 … HL2) -HL2 #K2 #V2 #HK2 #HV2 #H destruct /3 width=5/
+qed-.
+
+lemma ltprs_inv_atom2: ∀L1. L1 ➡* ⋆ → L1 = ⋆.
+#L1 #H @(ltprs_ind_dx … H) -L1 //
+#L1 #L #HL1 #_ #IHL2 destruct
+>(ltpr_inv_atom2 … HL1) -L1 //
+qed-.
+
+lemma ltprs_inv_pair2: ∀I,L1,K2,V2. L1 ➡* K2. ⓑ{I} V2 →
+                       ∃∃K1,V1. K1 ➡* K2 & V1 ➡* V2 & L1 = K1. ⓑ{I} V1.
+#I #L1 #K2 #V2 #H @(ltprs_ind_dx … H) -L1 /2 width=5/
+#L1 #L #HL1 #_ * #K #V #HK2 #HV2 #H destruct
+elim (ltpr_inv_pair2 … HL1) -HL1 #K1 #V1 #HK1 #HV1 #H destruct /3 width=5/
+qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma ltprs_fwd_length: ∀L1,L2. L1 ➡* L2 → |L1| = |L2|.
+#L1 #L2 #H @(ltprs_ind … H) -L2 //
+#L #L2 #_ #HL2 #IHL1
+>IHL1 -L1 >(ltpr_fwd_length … HL2) -HL2 //
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltprs_alt.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltprs_alt.etc
new file mode 100644
index 000000000..1d2db2daf
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltprs_alt.etc
@@ -0,0 +1,38 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+notation "hvbox( T1 ➡ ➡ * break term 46 T2 )"
+   non associative with precedence 45
+   for @{ 'PRedStarAlt $T1 $T2 }.
+
+include "basic_2/computation/ltprs.ma".
+
+(* CONTEXT-FREE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ******************)
+
+(* alternative definition of ltprs *)
+definition ltprsa: relation lenv ≝ lpx tprs.
+
+interpretation
+  "context-free parallel computation (environment) alternative"
+  'PRedStarAlt L1 L2 = (ltprsa L1 L2).
+
+(* Basic properties *********************************************************)
+
+lemma ltprs_ltprsa: ∀L1,L2. L1 ➡* L2 → L1 ➡➡* L2.
+/2 width=1/ qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma ltprsa_ltprs: ∀L1,L2. L1 ➡➡* L2 → L1 ➡* L2.
+/2 width=1/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltprs_ldrop.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltprs_ldrop.etc
new file mode 100644
index 000000000..a7c320089
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltprs_ldrop.etc
@@ -0,0 +1,27 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/reducibility/ltpr_ldrop.ma".
+include "basic_2/computation/ltprs.ma".
+
+(* CONTEXT-FREE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ******************)
+
+lemma ltprs_ldrop_conf: dropable_sn ltprs.
+/2 width=3/ qed.
+
+lemma ldrop_ltprs_trans: dedropable_sn ltprs.
+/2 width=3/ qed.
+
+lemma ltprs_ldrop_trans_O1: dropable_dx ltprs.
+/2 width=3/ qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltprs_ltprs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltprs_ltprs.etc
new file mode 100644
index 000000000..7ededf2af
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltprs_ltprs.etc
@@ -0,0 +1,32 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/reducibility/ltpr_ltpr.ma".
+include "basic_2/computation/ltprs.ma".
+
+(* CONTEXT-FREE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ******************)
+
+(* Advanced properties ******************************************************)
+
+lemma ltprs_strip: ∀L1. ∀L:lenv. L ➡* L1 → ∀L2. L ➡ L2 →
+                   ∃∃L0. L1 ➡ L0 & L2 ➡* L0.
+/3 width=3/ qed.
+
+(* Main properties **********************************************************)
+
+theorem ltprs_conf: confluent … ltprs.
+/3 width=3/ qed.
+
+theorem ltprs_trans: Transitive … ltprs.
+/2 width=3/ qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tprs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tprs.etc
new file mode 100644
index 000000000..492b39041
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tprs.etc
@@ -0,0 +1,94 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+notation "hvbox( T1 ➡ * break term 46 T2 )"
+   non associative with precedence 45
+   for @{ 'PRedStar $T1 $T2 }.
+
+include "basic_2/reducibility/tpr.ma".
+
+(* CONTEXT-FREE PARALLEL COMPUTATION ON TERMS *******************************)
+
+(* Basic_1: includes: pr1_pr0 *)
+definition tprs: relation term ≝ TC … tpr.
+
+interpretation "context-free parallel computation (term)"
+   'PRedStar T1 T2 = (tprs T1 T2).
+
+(* Basic eliminators ********************************************************)
+
+lemma tprs_ind: ∀T1. ∀R:predicate term. R T1 →
+                (∀T,T2. T1 ➡* T → T ➡ T2 → R T → R T2) →
+                ∀T2. T1 ➡* T2 → R T2.
+#T1 #R #HT1 #IHT1 #T2 #HT12
+@(TC_star_ind … HT1 IHT1 … HT12) //
+qed-.
+
+lemma tprs_ind_dx: ∀T2. ∀R:predicate term. R T2 →
+                   (∀T1,T. T1 ➡ T → T ➡* T2 → R T → R T1) →
+                   ∀T1. T1 ➡* T2 → R T1.
+#T2 #R #HT2 #IHT2 #T1 #HT12
+@(TC_star_ind_dx … HT2 IHT2 … HT12) //
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma tprs_refl: reflexive … tprs.
+/2 width=1/ qed.
+
+lemma tpr_tprs: ∀T1,T2. T1 ➡ T2 → T2 ➡* T2.
+/2 width=1/ qed.
+
+lemma tprs_strap1: ∀T1,T,T2. T1 ➡* T → T ➡ T2 → T1 ➡* T2.
+/2 width=3/ qed.
+
+lemma tprs_strap2: ∀T1,T,T2. T1 ➡ T → T ➡* T2 → T1 ➡* T2.
+/2 width=3/ qed.
+
+(* Basic_1: was only: pr1_head_1 *)
+lemma tprs_pair_sn: ∀I,T1,T2. T1 ➡ T2 → ∀V1,V2. V1 ➡* V2 →
+                    ②{I} V1. T1 ➡* ②{I} V2. T2.
+* [ #a ] #I #T1 #T2 #HT12 #V1 #V2 #H @(tprs_ind … H) -V2
+[1,3: /3 width=1/
+|2,4: #V #V2 #_ #HV2 #IHV1
+      @(tprs_strap1 … IHV1) -IHV1 /2 width=1/
+]
+qed.
+
+(* Basic_1: was only: pr1_head_2 *)
+lemma tprs_pair_dx: ∀I,V1,V2. V1 ➡ V2 → ∀T1,T2. T1 ➡* T2 →
+                    ②{I} V1. T1 ➡* ②{I} V2. T2.
+* [ #a ] #I #V1 #V2 #HV12 #T1 #T2 #H @(tprs_ind … H) -T2
+[1,3: /3 width=1/
+|2,4: #T #T2 #_ #HT2 #IHT1
+      @(tprs_strap1 … IHT1) -IHT1 /2 width=1/
+]
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma tprs_inv_atom1: ∀U2,k. ⋆k ➡* U2 → U2 = ⋆k.
+#U2 #k #H @(tprs_ind … H) -U2 //
+#U #U2 #_ #HU2 #IHU1 destruct
+>(tpr_inv_atom1 … HU2) -HU2 //
+qed-.
+
+lemma tprs_inv_cast1: ∀W1,T1,U2. ⓝW1.T1 ➡* U2 → T1 ➡* U2 ∨
+                      ∃∃W2,T2. W1 ➡* W2 & T1 ➡* T2 & U2 = ⓝW2.T2.
+#W1 #T1 #U2 #H @(tprs_ind … H) -U2 /3 width=5/
+#U #U2 #_ #HU2 * /3 width=3/ *
+#W #T #HW1 #HT1 #H destruct
+elim (tpr_inv_cast1 … HU2) -HU2 /3 width=3/ *
+#W2 #T2 #HW2 #HT2 #H destruct /4 width=5/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tprs_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tprs_lift.etc
new file mode 100644
index 000000000..d0d173470
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tprs_lift.etc
@@ -0,0 +1,43 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/reducibility/tpr_lift.ma".
+include "basic_2/computation/tprs.ma".
+
+(* CONTEXT-FREE PARALLEL COMPUTATION ON TERMS *******************************)
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma tprs_inv_abst1: ∀a,V1,T1,U2. ⓛ{a}V1. T1 ➡* U2 →
+                      ∃∃V2,T2. V1 ➡* V2 & T1 ➡* T2 & U2 = ⓛ{a}V2. T2.
+#a #V1 #T1 #U2 #H @(tprs_ind … H) -U2 /2 width=5/
+#U #U2 #_ #HU2 * #V #T #HV1 #HT1 #H destruct
+elim (tpr_inv_abst1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H destruct /3 width=5/
+qed-.
+
+lemma tprs_inv_abst: ∀a,V1,V2,T1,T2. ⓛ{a}V1. T1 ➡* ⓛ{a}V2. T2 →
+                     V1 ➡* V2 ∧ T1 ➡* T2.
+#a #V1 #V2 #T1 #T2 #H
+elim (tprs_inv_abst1 … H) -H #V #T #HV1 #HT1 #H destruct /2 width=1/
+qed-.
+
+(* Relocation properties ****************************************************)
+
+(* Note: this was missing in basic_1 *)
+lemma tprs_lift: t_liftable tprs.
+/3 width=7/ qed.
+
+(* Note: this was missing in basic_1 *)
+lemma tprs_inv_lift1: t_deliftable_sn tprs.
+/3 width=3 by tpr_inv_lift1, t_deliftable_sn_TC/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tprs_tprs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tprs_tprs.etc
new file mode 100644
index 000000000..87a4a71ab
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tprs_tprs.etc
@@ -0,0 +1,43 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/reducibility/tpr_tpr.ma".
+include "basic_2/computation/tprs.ma".
+
+(* CONTEXT-FREE PARALLEL COMPUTATION ON TERMS *******************************)
+
+(* Advanced properties ******************************************************)
+
+(* Basic_1: was: pr1_strip *)
+lemma tprs_strip: ∀T1,T. T ➡* T1 → ∀T2. T ➡ T2 →
+                  ∃∃T0. T1 ➡ T0 & T2 ➡* T0.
+/3 width=3 by TC_strip1, tpr_conf/ qed.
+
+(* Main propertis ***********************************************************)
+
+(* Basic_1: was: pr1_confluence *)
+theorem tprs_conf: confluent … tprs.
+/3 width=3/ qed.
+
+(* Basic_1: was: pr1_t *)
+theorem tprs_trans: Transitive … tprs.
+/2 width=3/ qed.
+
+(* Basic_1: was: pr1_comp *)
+lemma tprs_pair: ∀I,V1,V2. V1 ➡* V2 → ∀T1,T2. T1 ➡* T2 →
+                 ②{I} V1. T1 ➡* ②{I} V2. T2.
+#I #V1 #V2 #H @(tprs_ind … H) -V2 /2 width=1/
+#V #V2 #_ #HV2 #IHV1 #T1 #T2 #HT12
+@(tprs_trans … (②{I}V.T2)) /2 width=1/
+qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/delift/cprs_delift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/delift/cprs_delift.etc
new file mode 100644
index 000000000..6b7892611
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/delift/cprs_delift.etc
@@ -0,0 +1,37 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/reducibility/cpr_delift.ma".
+include "basic_2/reducibility/cpr_cpr.ma".
+include "basic_2/computation/cprs.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
+
+(* Properties on inverse basic term relocation ******************************)
+
+(* Note: this should be stated with tprs *)
+lemma cprs_zeta_delift: ∀L,V,T1,T2. L.ⓓV ⊢ ▼*[O, 1] T1 ≡ T2 → L ⊢ +ⓓV.T1 ➡* T2.
+#L #V #T1 #T2 * #T #HT1 #HT2
+@(cprs_strap2 … (+ⓓV.T)) [ /3 width=3/ | @inj /3 width=3/ ] (**) (* explicit constructor, /5 width=3/ is too slow *)
+qed.
+
+(* Basic_1: was only: pr3_gen_cabbr *)
+lemma thin_cprs_delift_conf: ∀L,U1,U2. L ⊢ U1 ➡* U2 →
+                             ∀K,d,e. ▼*[d, e] L ≡ K → ∀T1. L ⊢ ▼*[d, e] U1 ≡ T1 →
+                             ∃∃T2. K ⊢ T1 ➡* T2 & L ⊢ ▼*[d, e] U2 ≡ T2.
+#L #U1 #U2 #H @(cprs_ind … H) -U2 /2 width=3/
+#U #U2 #_ #HU2 #IHU1 #K #d #e #HLK #T1 #HTU1
+elim (IHU1 … HLK … HTU1) -U1 #T #HT1 #HUT
+elim (thin_cpr_delift_conf … HU2 … HLK … HUT) -U -HLK /3 width=3/
+qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fprs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fprs.etc
new file mode 100644
index 000000000..f42bdf7e2
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fprs.etc
@@ -0,0 +1,58 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+notation "hvbox( ⦃ term 46 L1 , term 46 T1 ⦄ ➡ * break ⦃ term 46 L2 , term 46 T2 ⦄ )"
+   non associative with precedence 45
+   for @{ 'FocalizedPRedStar $L1 $T1 $L2 $T2 }.
+
+notation "hvbox( ⦃ term 46 L1 , term 46 T1 ⦄ ➡ ➡ * break ⦃ term 46 L2 , term 46 T2 ⦄ )"
+   non associative with precedence 45
+   for @{ 'FocalizedPRedStarAlt $L1 $T1 $L2 $T2 }.
+
+include "basic_2/reducibility/fpr.ma".
+
+(* CONTEXT-FREE PARALLEL COMPUTATION ON CLOSURES ****************************)
+
+definition fprs: bi_relation lenv term ≝ bi_TC … fpr.
+
+interpretation "context-free parallel computation (closure)"
+   'FocalizedPRedStar L1 T1 L2 T2 = (fprs L1 T1 L2 T2).
+
+(* Basic eliminators ********************************************************)
+
+lemma fprs_ind: ∀L1,T1. ∀R:relation2 lenv term. R L1 T1 →
+                (∀L,L2,T,T2. ⦃L1, T1⦄ ➡* ⦃L, T⦄ → ⦃L, T⦄ ➡ ⦃L2, T2⦄ → R L T → R L2 T2) →
+                ∀L2,T2. ⦃L1, T1⦄ ➡* ⦃L2, T2⦄ → R L2 T2.
+/3 width=7 by bi_TC_star_ind/ qed-.
+
+lemma fprs_ind_dx: ∀L2,T2. ∀R:relation2 lenv term. R L2 T2 →
+                   (∀L1,L,T1,T. ⦃L1, T1⦄ ➡ ⦃L, T⦄ → ⦃L, T⦄ ➡* ⦃L2, T2⦄ → R L T → R L1 T1) →
+                   ∀L1,T1. ⦃L1, T1⦄ ➡* ⦃L2, T2⦄ → R L1 T1.
+/3 width=7 by bi_TC_star_ind_dx/ qed-.
+
+(* Basic properties *********************************************************)
+
+lemma fpr_fprs: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡ ⦃L2, T2⦄ → ⦃L1, T1⦄ ➡* ⦃L2, T2⦄.
+/2 width=1/ qed.
+
+lemma fprs_refl: bi_reflexive … fprs.
+/2 width=1/ qed.
+
+lemma fprs_strap1: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ➡* ⦃L, T⦄ → ⦃L, T⦄ ➡ ⦃L2, T2⦄ →
+                   ⦃L1, T1⦄ ➡* ⦃L2, T2⦄.
+/2 width=4/ qed.
+
+lemma fprs_strap2: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ➡ ⦃L, T⦄ → ⦃L, T⦄ ➡* ⦃L2, T2⦄ →
+                   ⦃L1, T1⦄ ➡* ⦃L2, T2⦄.
+/2 width=4/ qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fprs_aaa.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fprs_aaa.etc
new file mode 100644
index 000000000..b76637ff7
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fprs_aaa.etc
@@ -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/reducibility/cfpr_aaa.ma".
+include "basic_2/computation/fprs.ma".
+
+(* CONTEXT-FREE PARALLEL COMPUTATION ON CLOSURES ****************************)
+
+(* Properties about atomic arity assignment on terms ************************)
+
+lemma aaa_fprs_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A →
+                     ∀L2,T2. ⦃L1, T1⦄ ➡* ⦃L2, T2⦄ → L2 ⊢ T2 ⁝ A.
+#L1 #T1 #A #HT1 #L2 #T2 #HLT12
+@(bi_TC_Conf3 … HT1 ?? HLT12) /2 width=4/
+qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fprs_cprs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fprs_cprs.etc
new file mode 100644
index 000000000..9d4d954b8
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fprs_cprs.etc
@@ -0,0 +1,138 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/reducibility/fpr_cpr.ma".
+include "basic_2/computation/cprs_lfprs.ma".
+include "basic_2/computation/lfprs_ltprs.ma".
+include "basic_2/computation/lfprs_fprs.ma".
+
+(* CONTEXT-FREE PARALLEL COMPUTATION ON CLOSURES ****************************)
+
+(* Advanced properties ******************************************************)
+
+lemma fprs_flat_dx_tpr: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡* ⦃L2, T2⦄ → ∀V1,V2. V1 ➡ V2 →
+                        ∀I. ⦃L1, ⓕ{I}V1.T1⦄ ➡* ⦃L2, ⓕ{I}V2.T2⦄.
+#L1 #L2 #T1 #T2 #HT12 @(fprs_ind … HT12) -L2 -T2 /3 width=1/
+#L #L2 #T #T2 #_ #HT2 #IHT2 #V1 #V2 #HV12 #I
+lapply (IHT2 … HV12 I) -IHT2 -HV12 /3 width=6/
+qed.
+
+lemma fprs_bind2_minus: ∀I,L1,L2,V1,T1,U2. ⦃L1, -ⓑ{I}V1.T1⦄ ➡* ⦃L2, U2⦄ →
+                        ∃∃V2,T2. ⦃L1.ⓑ{I}V1, T1⦄ ➡* ⦃L2.ⓑ{I}V2, T2⦄ &
+                                 U2 = -ⓑ{I}V2.T2.
+#I #L1 #L2 #V1 #T1 #U2 #H @(fprs_ind … H) -L2 -U2 /2 width=4/
+#L #L2 #U #U2 #_ #HU2 * #V #T #HT1 #H destruct
+elim (fpr_bind2_minus … HU2) -HU2 /3 width=4/
+qed-.
+
+lemma fprs_lift: ∀K1,K2,T1,T2. ⦃K1, T1⦄ ➡* ⦃K2, T2⦄ →
+                 ∀d,e,L1. ⇩[d, e] L1 ≡ K1 →
+                 ∀U1,U2. ⇧[d, e] T1 ≡ U1 → ⇧[d, e] T2 ≡ U2 →
+                 ∃∃L2. ⦃L1, U1⦄ ➡* ⦃L2, U2⦄ & ⇩[d, e] L2 ≡ K2.
+#K1 #K2 #T1 #T2 #HT12 @(fprs_ind … HT12) -K2 -T2
+[ #d #e #L1 #HLK1 #U1 #U2 #HTU1 #HTU2
+  >(lift_mono … HTU2 … HTU1) -U2 /2 width=3/
+| #K #K2 #T #T2 #_ #HT2 #IHT1 #d #e #L1 #HLK1 #U1 #U2 #HTU1 #HTU2
+  elim (lift_total T d e) #U #HTU
+  elim (IHT1 … HLK1 … HTU1 HTU) -K1 -T1 #L #HU1 #HKL
+  elim (fpr_lift … HT2 … HKL … HTU HTU2) -K -T -T2 /3 width=4/
+]
+qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma fprs_inv_pair1: ∀I,K1,L2,V1,T1,T2. ⦃K1.ⓑ{I}V1, T1⦄ ➡* ⦃L2, T2⦄ →
+                      ∃∃K2,V2. ⦃K1, V1⦄  ➡* ⦃K2, V2⦄ &
+                               ⦃K1, -ⓑ{I}V1.T1⦄ ➡* ⦃K2, -ⓑ{I}V2.T2⦄  &
+                               L2 = K2.ⓑ{I}V2.
+#I #K1 #L2 #V1 #T1 #T2 #H @(fprs_ind … H) -L2 -T2 /2 width=5/
+#L #L2 #T #T2 #_ #HT2 * #K #V #HV1 #HT1 #H destruct
+elim (fpr_inv_pair1 … HT2) -HT2 #K2 #V2 #HV2 #HT2 #H destruct /3 width=5/
+qed-.
+
+lemma fprs_inv_pair3: ∀I,L1,K2,V2,T1,T2. ⦃L1, T1⦄ ➡* ⦃K2.ⓑ{I}V2, T2⦄ →
+                      ∃∃K1,V1. ⦃K1, V1⦄  ➡* ⦃K2, V2⦄ &
+                               ⦃K1, -ⓑ{I}V1.T1⦄ ➡* ⦃K2, -ⓑ{I}V2.T2⦄  &
+                               L1 = K1.ⓑ{I}V1.
+#I2 #L1 #K2 #V2 #T1 #T2 #H @(fprs_ind_dx … H) -L1 -T1 /2 width=5/
+#L1 #L #T1 #T #HT1 #_ * #K #V #HV2 #HT2 #H destruct
+elim (fpr_inv_pair3 … HT1) -HT1 #K1 #V1 #HV1 #HT1 #H destruct /3 width=5/
+qed-.
+
+(* Advanced forward lemmas **************************************************)
+
+lemma fprs_fwd_bind2_minus: ∀I,L1,L,V1,T1,T. ⦃L1, -ⓑ{I}V1.T1⦄ ➡* ⦃L, T⦄ → ∀b.
+                            ∃∃V2,T2. ⦃L1, ⓑ{b,I}V1.T1⦄ ➡* ⦃L, ⓑ{b,I}V2.T2⦄ &
+                                     T = -ⓑ{I}V2.T2.
+#I #L1 #L #V1 #T1 #T #H1 #b @(fprs_ind … H1) -L -T /2 width=4/
+#L0 #L #T0 #T #_ #H0 * #W1 #U1 #HTU1 #H destruct
+elim (fpr_fwd_bind2_minus … H0 b) -H0 /3 width=4/
+qed-.
+
+lemma fprs_fwd_pair1_full: ∀I,K1,L2,V1,T1,T2. ⦃K1.ⓑ{I}V1, T1⦄ ➡* ⦃L2, T2⦄ →
+                           ∀b. ∃∃K2,V2. ⦃K1, V1⦄  ➡* ⦃K2, V2⦄ &
+                                        ⦃K1, ⓑ{b,I}V1.T1⦄ ➡* ⦃K2, ⓑ{b,I}V2.T2⦄ &
+                                        L2 = K2.ⓑ{I}V2.
+#I #K1 #L2 #V1 #T1 #T2 #H #b
+elim (fprs_inv_pair1 … H) -H #K2 #V2 #HV12 #HT12 #H destruct
+elim (fprs_fwd_bind2_minus … HT12 b) -HT12 #W1 #U1 #HTU1 #H destruct /2 width=5/
+qed-.
+
+lemma fprs_fwd_abst2: ∀a,L1,L2,V1,T1,U2. ⦃L1, ⓛ{a}V1.T1⦄ ➡* ⦃L2, U2⦄ → ∀b,I,W.
+                      ∃∃V2,T2. ⦃L1, ⓑ{b,I}W.T1⦄ ➡* ⦃L2, ⓑ{b,I}W.T2⦄ &
+                               U2 = ⓛ{a}V2.T2.
+#a #L1 #L2 #V1 #T1 #U2 #H #b #I #W @(fprs_ind … H) -L2 -U2 /2 width=4/
+#L #L2 #U #U2 #_ #H2 * #V #T #HT1 #H destruct
+elim (fpr_fwd_abst2 … H2 b I W) -H2 /3 width=4/
+qed-.
+
+(* Properties on context-sensitive parallel computation for terms ***********)
+
+lemma cprs_fprs: ∀L,T1,T2. L ⊢ T1 ➡* T2 → ⦃L, T1⦄ ➡* ⦃L, T2⦄.
+#L #T1 #T2 #H @(cprs_ind … H) -T2 // /3 width=4/
+qed.
+
+(* Forward lemmas on context-sensitive parallel computation for terms *******)
+
+lemma fprs_fwd_cprs: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡* ⦃L2, T2⦄ → L1 ⊢ T1 ➡* T2.
+#L1 #L2 #T1 #T2 #H @(fprs_ind … H) -L2 -T2 //
+#L #L2 #T #T2 #H1 #H2 #IH1
+elim (fpr_inv_all … H2) -H2 #L0 #HL0 #HT2 #_ -L2
+lapply (lfprs_cpr_trans L1 … HT2) -HT2 /3 width=3/
+qed-.
+(*
+(* Advanced properties ******************************************************)
+
+lamma fpr_bind_sn: ∀L1,L2,V1,V2. ⦃L1, V1⦄ ➡ ⦃L2, V2⦄ → ∀T1,T2. T1 ➡ T2 →
+                   ∀a,I. ⦃L1, ⓑ{a,I}V1.T1⦄ ➡ ⦃L2, ⓑ{a,I}V2.T2⦄.
+#L1 #L2 #V1 #V2 #H #T1 #T2 #HT12 #a #I
+elim (fpr_inv_all … H) /3 width=4/
+qed.
+
+(* Advanced forward lemmas **************************************************)
+
+lamma fpr_fwd_shift_bind_minus: ∀I1,I2,L1,L2,V1,V2,T1,T2.
+                                ⦃L1, -ⓑ{I1}V1.T1⦄ ➡ ⦃L2, -ⓑ{I2}V2.T2⦄ →
+                                ⦃L1, V1⦄ ➡ ⦃L2, V2⦄ ∧ I1 = I2.
+* #I2 #L1 #L2 #V1 #V2 #T1 #T2 #H
+elim (fpr_inv_all … H) -H #L #HL1 #H #HL2
+[ elim (cpr_inv_abbr1 … H) -H *
+  [ #V #V0 #T #HV1 #HV0 #_ #H destruct /4 width=4/
+  | #T #_ #_ #H destruct
+  ]
+| elim (cpr_inv_abst1 … H Abst V2) -H
+  #V #T #HV1 #_ #H destruct /3 width=4/
+]
+qed-.
+*)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fprs_fprs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fprs_fprs.etc
new file mode 100644
index 000000000..e0c1b3058
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fprs_fprs.etc
@@ -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/reducibility/fpr_fpr.ma".
+include "basic_2/computation/fprs.ma".
+
+(* CONTEXT-FREE PARALLEL COMPUTATION ON CLOSURES ****************************)
+
+(* Advanced properties ******************************************************)
+
+lemma fprs_strip: ∀L0,L1,T0,T1. ⦃L0, T0⦄ ➡ ⦃L1, T1⦄ →
+                  ∀L2,T2. ⦃L0, T0⦄ ➡* ⦃L2, T2⦄ →
+                  ∃∃L,T. ⦃L1, T1⦄ ➡* ⦃L, T⦄ & ⦃L2, T2⦄ ➡ ⦃L, T⦄.
+#H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8
+/2 width=4/ qed.
+
+(* Main propertis ***********************************************************)
+
+theorem fprs_conf: bi_confluent … fprs.
+/2 width=4/ qed.
+
+theorem fprs_trans: bi_transitive … fprs.
+/2 width=4/ qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_px_bi.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/lenv_px_bi.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_px_bi.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/fpr/lenv_px_bi.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/lfprs_fprs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/lfprs_fprs.etc
new file mode 100644
index 000000000..a5c42ba65
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/lfprs_fprs.etc
@@ -0,0 +1,41 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/reducibility/lfpr_fpr.ma".
+include "basic_2/computation/fprs_fprs.ma".
+include "basic_2/computation/lfprs.ma".
+
+(* FOCALIZED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *********************)
+
+(* Inversion lemmas on context-free parallel reduction for closures *********)
+
+lemma lfprs_inv_fprs: ∀L1,L2. ⦃L1⦄ ➡* ⦃L2⦄ → ∀T. ⦃L1, T⦄ ➡* ⦃L2, T⦄.
+#L1 #L2 #H @(lfprs_ind … H) -L2 //
+#L #L2 #_ #HL2 #IHL1 #T
+lapply (lfpr_inv_fpr … HL2 T) -HL2 /3 width=4/
+qed-.
+
+(* Properties on context-free parallel computation for closures *************)
+
+lemma fprs_lfprs: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡* ⦃L2, T2⦄ → ⦃L1⦄ ➡* ⦃L2⦄.
+#L1 #L2 #T1 #T2 #H @(fprs_ind … H) -L2 -T2 // /3 width=5/
+qed.
+
+lemma lfprs_fprs_trans: ∀L1,L,L2,T1,T2. ⦃L1⦄ ➡* ⦃L⦄ → ⦃L, T1⦄ ➡* ⦃L2, T2⦄ → ⦃L1, T1⦄ ➡* ⦃L2, T2⦄.
+#L1 #L #L2 #T1 #T2 #HL1 #HL2
+lapply (lfprs_inv_fprs … HL1 T1) -HL1 /2 width=4/
+qed.
+(*
+lamma lfprs_cprs_conf: ∀L1,L,L2,T1,T2. ⦃L1⦄ ➡* ⦃L2⦄ → L1 ⊢ T1 ➡* T2 → ⦃L1, T1⦄ ➡* ⦃L2, T2⦄.
+*)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/chnf.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/tshf/chnf.etc
similarity index 92%
rename from matita/matita/contribs/lambdadelta/basic_2/reduction/chnf.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/tshf/chnf.etc
index 839450da3..f6106d38d 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/chnf.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/tshf/chnf.etc
@@ -12,6 +12,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
+notation "hvbox( L ⊢ break 𝐇𝐍 ⦃ term 46 T ⦄ )"
+   non associative with precedence 45
+   for @{ 'HdNormal $L $T }.
+
 include "basic_2/reduction/cpr_tshf.ma".
 
 (* CONTEXT-SENSITIVE WEAK HEAD NORMAL TERMS *********************************)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_tshf.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/tshf/cpr_tshf.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_tshf.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/tshf/cpr_tshf.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/tshf.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/tshf/tshf.etc
similarity index 90%
rename from matita/matita/contribs/lambdadelta/basic_2/grammar/tshf.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/tshf/tshf.etc
index a8873c18b..583c3f46f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/tshf.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/tshf/tshf.etc
@@ -12,6 +12,18 @@
 (*                                                                        *)
 (**************************************************************************)
 
+notation "hvbox( L ⊢ break term 46 T1 ≈ break term 46 T2 )"
+   non associative with precedence 45
+   for @{ 'Hom $L $T1 $T2 }.
+
+notation "hvbox( L ⊢ break 𝐇𝐑 ⦃ term 46 T ⦄ )"
+   non associative with precedence 45
+   for @{ 'HdReducible $L $T }.
+
+notation "hvbox( L ⊢ break 𝐇𝐈 ⦃ term 46 T ⦄ )"
+   non associative with precedence 45
+   for @{ 'NotHdReducible $L $T }.
+
 include "basic_2/grammar/term_simple.ma".
 
 (* SAME HEAD TERM FORMS *****************************************************)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_px_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn.ma
similarity index 76%
rename from matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_px_sn.ma
rename to matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn.ma
index d7cdcf595..b229526dd 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_px_sn.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn.ma
@@ -23,15 +23,6 @@ inductive lpx_sn (R:lenv→relation term): relation lenv ≝
                lpx_sn R (K1. ⓑ{I} V1) (K2. ⓑ{I} V2)
 .
 
-definition lpx_sn_confluent: relation (lenv→relation term) ≝ λR1,R2.
-                             ∀L0,T0,T1. R1 L0 T0 T1 → ∀T2. R2 L0 T0 T2 →
-                             ∀L1. lpx_sn R1 L0 L1 → ∀L2. lpx_sn R2 L0 L2 →
-                             ∃∃T. R2 L1 T1 T & R1 L2 T2 T.
-
-definition lpx_sn_transitive: relation (lenv→relation term) ≝ λR1,R2.
-                              ∀L1,T1,T. R1 L1 T1 T → ∀L2. lpx_sn R1 L1 L2 →
-                              ∀T2. R2 L2 T T2 → R1 L1 T1 T2.
-
 (* Basic inversion lemmas ***************************************************)
 
 fact lpx_sn_inv_atom1_aux: ∀R,L1,L2. lpx_sn R L1 L2 → L1 = ⋆ → L2 = ⋆.
@@ -121,25 +112,3 @@ lemma lpx_sn_append: ∀R. l_appendable_sn R →
                      lpx_sn R (L1 @@ K1) (L2 @@ K2).
 #R #HR #K1 #K2 #H elim H -K1 -K2 // /3 width=1/
 qed-.
-
-(* Advanced properties ******************************************************)
-
-lemma lpx_sn_trans: ∀R. lpx_sn_transitive R R → Transitive … (lpx_sn R).
-#R #HR #L1 #L #H elim H -L1 -L //
-#I #L1 #L #V1 #V #HL1 #HV1 #IHL1 #X #H
-elim (lpx_sn_inv_pair1 … H) -H #L2 #V2 #HL2 #HV2 #H destruct /3 width=5/
-qed-.
-
-lemma lpx_sn_conf: ∀R1,R2. lpx_sn_confluent R1 R2 →
-                   confluent2 … (lpx_sn R1) (lpx_sn R2).
-#R1 #R2 #HR12 #L0 @(f_ind … length … L0) -L0 #n #IH *
-[ #_ #X1 #H1 #X2 #H2 -n
-  >(lpx_sn_inv_atom1 … H1) -X1
-  >(lpx_sn_inv_atom1 … H2) -X2 /2 width=3/
-| #L0 #I #V0 #Hn #X1 #H1 #X2 #H2 destruct
-  elim (lpx_sn_inv_pair1 … H1) -H1 #L1 #V1 #HL01 #HV01 #H destruct
-  elim (lpx_sn_inv_pair1 … H2) -H2 #L2 #V2 #HL02 #HV02 #H destruct
-  elim (IH … HL01 … HL02) -IH normalize // #L #HL1 #HL2
-  elim (HR12 … HV01 … HV02 … HL01 … HL02) -L0 -V0 /3 width=5/
-]
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn_lpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn_lpx_sn.ma
new file mode 100644
index 000000000..69c010a19
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn_lpx_sn.ma
@@ -0,0 +1,48 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/grammar/lpx_sn.ma".
+
+(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********)
+
+definition lpx_sn_confluent: relation (lenv→relation term) ≝ λR1,R2.
+                             ∀L0,T0,T1. R1 L0 T0 T1 → ∀T2. R2 L0 T0 T2 →
+                             ∀L1. lpx_sn R1 L0 L1 → ∀L2. lpx_sn R2 L0 L2 →
+                             ∃∃T. R2 L1 T1 T & R1 L2 T2 T.
+
+definition lpx_sn_transitive: relation (lenv→relation term) ≝ λR1,R2.
+                              ∀L1,T1,T. R1 L1 T1 T → ∀L2. lpx_sn R1 L1 L2 →
+                              ∀T2. R2 L2 T T2 → R1 L1 T1 T2.
+
+(* Main properties **********************************************************)
+
+theorem lpx_sn_trans: ∀R. lpx_sn_transitive R R → Transitive … (lpx_sn R).
+#R #HR #L1 #L #H elim H -L1 -L //
+#I #L1 #L #V1 #V #HL1 #HV1 #IHL1 #X #H
+elim (lpx_sn_inv_pair1 … H) -H #L2 #V2 #HL2 #HV2 #H destruct /3 width=5/
+qed-.
+
+theorem lpx_sn_conf: ∀R1,R2. lpx_sn_confluent R1 R2 →
+                     confluent2 … (lpx_sn R1) (lpx_sn R2).
+#R1 #R2 #HR12 #L0 @(f_ind … length … L0) -L0 #n #IH *
+[ #_ #X1 #H1 #X2 #H2 -n
+  >(lpx_sn_inv_atom1 … H1) -X1
+  >(lpx_sn_inv_atom1 … H2) -X2 /2 width=3/
+| #L0 #I #V0 #Hn #X1 #H1 #X2 #H2 destruct
+  elim (lpx_sn_inv_pair1 … H1) -H1 #L1 #V1 #HL01 #HV01 #H destruct
+  elim (lpx_sn_inv_pair1 … H2) -H2 #L2 #V2 #HL02 #HV02 #H destruct
+  elim (IH … HL01 … HL02) -IH normalize // #L #HL1 #HL2
+  elim (HR12 … HV01 … HV02 … HL01 … HL02) -L0 -V0 /3 width=5/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn_tc.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn_tc.ma
new file mode 100644
index 000000000..fa1234d1a
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn_tc.ma
@@ -0,0 +1,122 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/grammar/lpx_sn.ma".
+
+(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********)
+
+(* Properties on transitive_closure *****************************************)
+
+lemma TC_lpx_sn_pair_refl: ∀R. (∀L. reflexive … (R L)) →
+                           ∀L1,L2. TC … (lpx_sn R) L1 L2 →
+                           ∀I,V. TC … (lpx_sn R) (L1. ⓑ{I} V) (L2. ⓑ{I} V).
+#R #HR #L1 #L2 #H @(TC_star_ind … L2 H) -L2
+[ /2 width=1 by lpx_sn_refl/
+| /3 width=1 by TC_reflexive, lpx_sn_refl/
+| /3 width=5/
+]
+qed-.
+
+lemma TC_lpx_sn_pair: ∀R. (∀L. reflexive … (R L)) →
+                      ∀I,L1,L2. TC … (lpx_sn R) L1 L2 →
+                      ∀V1,V2. LTC … R L1 V1 V2 →
+                      TC … (lpx_sn R) (L1. ⓑ{I} V1) (L2. ⓑ{I} V2).
+#R #HR #I #L1 #L2 #HL12 #V1 #V2 #H @(TC_star_ind_dx … V1 H) -V1 //
+[ /2 width=1 by TC_lpx_sn_pair_refl/
+| /4 width=3 by TC_strap, lpx_sn_pair, lpx_sn_refl/
+]
+qed-.
+
+lemma lpx_sn_LTC_TC_lpx_sn: ∀R. (∀L. reflexive … (R L)) →
+                            ∀L1,L2. lpx_sn (LTC … R) L1 L2 →
+                            TC … (lpx_sn R) L1 L2.
+#R #HR #L1 #L2 #H elim H -L1 -L2 /2 width=1/
+/2 width=1 by TC_lpx_sn_pair/
+qed-.
+
+(* Inversion lemmas on transitive closure ***********************************)
+
+lemma TC_lpx_sn_inv_atom2: ∀R,L1. TC … (lpx_sn R) L1 (⋆) → L1 = ⋆.
+#R #L1 #H @(TC_ind_dx … L1 H) -L1
+[ #L1 #H lapply (lpx_sn_inv_atom2 … H) -H //
+| #L1 #L #HL1 #_ #IHL2 destruct
+  lapply (lpx_sn_inv_atom2 … HL1) -HL1 //
+]
+qed-.
+
+lemma TC_lpx_sn_inv_pair2: ∀R. s_rs_trans … R (lpx_sn R) →
+                           ∀I,L1,K2,V2. TC  … (lpx_sn R) L1 (K2.ⓑ{I}V2) →
+                           ∃∃K1,V1. TC … (lpx_sn R) K1 K2 & LTC … R K1 V1 V2 & L1 = K1. ⓑ{I} V1.
+#R #HR #I #L1 #K2 #V2 #H @(TC_ind_dx … L1 H) -L1
+[ #L1 #H elim (lpx_sn_inv_pair2 … H) -H /3 width=5/
+| #L1 #L #HL1 #_ * #K #V #HK2 #HV2 #H destruct
+  elim (lpx_sn_inv_pair2 … HL1) -HL1 #K1 #V1 #HK1 #HV1 #H destruct
+  lapply (HR … HV2 … HK1) -HR -HV2 #HV2 /3 width=5/
+]
+qed-.
+
+lemma TC_lpx_sn_ind: ∀R. s_rs_trans … R (lpx_sn R) →
+                     ∀S:relation lenv.
+                     S (⋆) (⋆) → (
+                        ∀I,K1,K2,V1,V2.
+                        TC … (lpx_sn R) K1 K2 → LTC … R K1 V1 V2 →
+                        S K1 K2 → S (K1.ⓑ{I}V1) (K2.ⓑ{I}V2)
+                     ) →
+                     ∀L2,L1. TC … (lpx_sn R) L1 L2 → S L1 L2.
+#R #HR #S #IH1 #IH2 #L2 elim L2 -L2
+[ #X #H >(TC_lpx_sn_inv_atom2 … H) -X //
+| #L2 #I #V2 #IHL2 #X #H
+  elim (TC_lpx_sn_inv_pair2 … H) // -H -HR
+  #L1 #V1 #HL12 #HV12 #H destruct /3 width=1/
+]
+qed-.
+
+lemma TC_lpx_sn_inv_atom1: ∀R,L2. TC … (lpx_sn R) (⋆) L2 → L2 = ⋆.
+#R #L2 #H elim H -L2
+[ #L2 #H lapply (lpx_sn_inv_atom1 … H) -H //
+| #L #L2 #_ #HL2 #IHL1 destruct
+  lapply (lpx_sn_inv_atom1 … HL2) -HL2 //
+]
+qed-.
+
+fact TC_lpx_sn_inv_pair1_aux: ∀R. s_rs_trans … R (lpx_sn R) →
+                              ∀L1,L2. TC … (lpx_sn R) L1 L2 →
+                              ∀I,K1,V1. L1 = K1.ⓑ{I}V1 →
+                              ∃∃K2,V2. TC … (lpx_sn R) K1 K2 & LTC … R K1 V1 V2 & L2 = K2. ⓑ{I} V2.
+#R #HR #L1 #L2 #H @(TC_lpx_sn_ind … H) // -HR -L1 -L2
+[ #J #K #W #H destruct
+| #I #L1 #L2 #V1 #V2 #HL12 #HV12 #_ #J #K #W #H destruct /2 width=5/
+]
+qed-.
+
+lemma TC_lpx_sn_inv_pair1: ∀R. s_rs_trans … R (lpx_sn R) →
+                           ∀I,K1,L2,V1. TC … (lpx_sn R) (K1.ⓑ{I}V1) L2 →
+                           ∃∃K2,V2. TC … (lpx_sn R) K1 K2 & LTC … R K1 V1 V2 & L2 = K2. ⓑ{I} V2.
+/2 width=3 by TC_lpx_sn_inv_pair1_aux/ qed-.
+
+lemma TC_lpx_sn_inv_lpx_sn_LTC: ∀R. s_rs_trans … R (lpx_sn R) →
+                                ∀L1,L2. TC … (lpx_sn R) L1 L2 →
+                                lpx_sn (LTC … R) L1 L2.
+#R #HR #L1 #L2 #H @(TC_lpx_sn_ind … H) // -HR -L1 -L2 /2 width=1/
+qed-.
+
+(* Forward lemmas on transitive closure *************************************)
+
+lemma TC_lpx_sn_fwd_length: ∀R,L1,L2. TC … (lpx_sn R) L1 L2 → |L1| = |L2|.
+#R #L1 #L2 #H elim H -L2
+[ #L2 #HL12 >(lpx_sn_fwd_length … HL12) -HL12 //
+| #L #L2 #_ #HL2 #IHL1
+  >IHL1 -L1 >(lpx_sn_fwd_length … HL2) -HL2 //
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation.ma b/matita/matita/contribs/lambdadelta/basic_2/notation.ma
index 6a5b14e62..d53b103c8 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation.ma
@@ -116,10 +116,6 @@ notation "hvbox( T1 . break ⓛ T2 )"
  left associative with precedence 49
  for @{ 'DxAbst $T1 $T2 }.
 
-notation "hvbox( T . break ④ { term 46 I } break { term 46 T1 , break term 46 T2 , break term 46 T3 } )"
- non associative with precedence 50
- for @{ 'DxItem4 $T $I $T1 $T2 $T3 }.
-
 notation "hvbox( ♯ { term 46 x } )"
  non associative with precedence 90
  for @{ 'Weight $x }.
@@ -132,10 +128,6 @@ notation "hvbox( 𝐒 ⦃ term 46 T ⦄ )"
    non associative with precedence 45
    for @{ 'Simple $T }.
 
-notation "hvbox( L ⊢ break term 46 T1 ≈ break term 46 T2 )"
-   non associative with precedence 45
-   for @{ 'Hom $L $T1 $T2 }.
-
 notation "hvbox( T1 ≃ break term 46 T2 )"
    non associative with precedence 45
    for @{ 'Iso $T1 $T2 }.
@@ -146,14 +138,6 @@ notation "hvbox( ⇧ [ term 46 d , break term 46 e ] break term 46 T1 ≡ break
    non associative with precedence 45
    for @{ 'RLift $d $e $T1 $T2 }.
 
-notation "hvbox( L1 break ⊑ [ term 46 d , break term 46 e ] break term 46 L2 )"
-   non associative with precedence 45
-   for @{ 'SubEq $L1 $d $e $L2 }.
-
-notation "hvbox( ⊒ [ term 46 d , break term 46 e ] break term 46 L2 )"
-   non associative with precedence 45
-   for @{ 'SubEqBottom $d $e $L2 }.
-
 notation "hvbox( ⇩ [ term 46 e ] break term 46 L1 ≡ break term 46 L2 )"
    non associative with precedence 45
    for @{ 'RDrop $e $L1 $L2 }.
@@ -196,6 +180,10 @@ notation "hvbox( ⦃ term 46 L1, break term 46 T1 ⦄ ⊃ * break ⦃ term 46 L2
    non associative with precedence 45
    for @{ 'SupTermStar $L1 $T1 $L2 $T2 }.
 
+notation "hvbox( L1 ⊑ break term 46 L2 )"
+   non associative with precedence 45
+   for @{ 'SubEq $L1 $L2 }.
+
 notation "hvbox( L ⊢ break term 46 T1 ▶* break term 46 T2 )"
    non associative with precedence 45
    for @{ 'PSubstStar $L $T1 $T2 }.
@@ -258,36 +246,6 @@ notation "hvbox( L ⊢ break 𝐍 ⦃ term 46 T ⦄ )"
    non associative with precedence 45
    for @{ 'Normal $L $T }.
 
-(* this might be removed *)
-notation "hvbox( 𝐇𝐑 ⦃ term 46 T ⦄ )"
-   non associative with precedence 45
-   for @{ 'HdReducible $T }.
-
-(* this might be removed *)
-notation "hvbox( L ⊢ break 𝐇𝐑 ⦃ term 46 T ⦄ )"
-   non associative with precedence 45
-   for @{ 'HdReducible $L $T }.
-
-(* this might be removed *)
-notation "hvbox( 𝐇𝐈 ⦃ term 46 T ⦄ )"
-   non associative with precedence 45
-   for @{ 'NotHdReducible $T }.
-
-(* this might be removed *)
-notation "hvbox( L ⊢ break 𝐇𝐈 ⦃ term 46 T ⦄ )"
-   non associative with precedence 45
-   for @{ 'NotHdReducible $L $T }.
-
-(* this might be removed *)
-notation "hvbox( 𝐇𝐍 ⦃ term 46 T ⦄ )"
-   non associative with precedence 45
-   for @{ 'HdNormal $T }.
-
-(* this might be removed *)
-notation "hvbox( L ⊢ break 𝐇𝐍 ⦃ term 46 T ⦄ )"
-   non associative with precedence 45
-   for @{ 'HdNormal $L $T }.
-
 notation "hvbox( L ⊢ break term 46 T1 ➡ break term 46 T2 )"
    non associative with precedence 45
    for @{ 'PRed $L $T1 $T2 }.
@@ -306,6 +264,10 @@ notation "hvbox( L1 ⊢ ➡* break term 46 L2 )"
    non associative with precedence 45
    for @{ 'PRedSnStar $L1 $L2 }.
 
+notation "hvbox( L1 ⊢ ➡➡* break term 46 L2 )"
+   non associative with precedence 45
+   for @{ 'PRedSnStarAlt $L1 $L2 }.
+
 notation "hvbox( L ⊢ break term 46 T1 ➡ * break 𝐍 ⦃ term 46 T2 ⦄ )"
    non associative with precedence 45
    for @{ 'PEval $L $T1 $T2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma
index e6ad7b2ba..421cc97de 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma
@@ -45,16 +45,11 @@ interpretation "context-sensitive parallel reduction (term)"
 
 (* Basic properties *********************************************************)
 
-(* Note: it does not hold replacing |L1| with |L2| *)
-lemma cpr_lsubr_trans: ∀L1,T1,T2. L1 ⊢ T1 ➡ T2 →
-                       ∀L2. L2 ⊑ [0, |L1|] L1 → L2 ⊢ T1 ➡ T2.
+lemma cpr_lsubr_trans: lsubr_trans … cpr.
 #L1 #T1 #T2 #H elim H -L1 -T1 -T2
 [ //
 | #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
-  lapply (ldrop_fwd_ldrop2_length … HLK1) #Hi
-  lapply (ldrop_fwd_O1_length … HLK1) #H2i
-  elim (ldrop_lsubr_ldrop2_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // -Hi
-  <H2i -H2i <minus_plus_m_m /3 width=6/
+  elim (lsubr_fwd_ldrop2_abbr … HL12 … HLK1) -HL12 -HLK1 /3 width=6/
 |3,7: /4 width=1/
 |4,6: /3 width=1/
 |5,8: /4 width=3/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr.ma
index 1b3100ffb..04d5d1a29 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr.ma
@@ -46,6 +46,10 @@ lemma lpr_inv_pair2: ∀I,L1,K2,V2. L1 ⊢ ➡ K2. ⓑ{I} V2 →
 lemma lpr_refl: ∀L. L ⊢ ➡ L.
 /2 width=1 by lpx_sn_refl/ qed.
 
+lemma lpr_pair: ∀I,K1,K2,V1,V2. K1 ⊢ ➡ K2 → K1 ⊢ V1 ➡ V2 →
+                K1.ⓑ{I}V1 ⊢ ➡ K2.ⓑ{I}V2.
+/2 width=1/ qed.
+
 lemma lpr_append: ∀K1,K2. K1 ⊢ ➡ K2 → ∀L1,L2. L1 ⊢ ➡ L2 →
                   L1 @@ K1 ⊢ ➡ L2 @@ K2.
 /3 width=1 by lpx_sn_append, cpr_append/ qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_cpr.ma
index 1d83a1314..c0f33584c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_cpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_cpr.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basic_2/grammar/lpx_sn_lpx_sn.ma".
 include "basic_2/relocation/fsup.ma".
 include "basic_2/reduction/lpr_ldrop.ma".
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_cpss.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_cpss.ma
index c5cb57721..955108572 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_cpss.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_cpss.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basic_2/grammar/lpx_sn_lpx_sn.ma".
 include "basic_2/substitution/lpss_ldrop.ma".
 include "basic_2/reduction/lpr_ldrop.ma".
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma
index 6d91d0aa0..85d36c39f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma
@@ -14,7 +14,6 @@
 
 include "basic_2/grammar/cl_weight.ma".
 include "basic_2/relocation/lift.ma".
-include "basic_2/relocation/lsubr.ma".
 
 (* LOCAL ENVIRONMENT SLICING ************************************************)
 
@@ -30,24 +29,24 @@ inductive ldrop: nat → nat → relation lenv ≝
 
 interpretation "local slicing" 'RDrop d e L1 L2 = (ldrop d e L1 L2).
 
-definition l_liftable: (lenv → relation term) → Prop ≝
+definition l_liftable: predicate (lenv → relation term) ≝
                        λR. ∀K,T1,T2. R K T1 T2 → ∀L,d,e. ⇩[d, e] L ≡ K →
                        ∀U1. ⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d, e] T2 ≡ U2 → R L U1 U2.
 
-definition l_deliftable_sn: (lenv → relation term) → Prop ≝
+definition l_deliftable_sn: predicate (lenv → relation term) ≝
                             λR. ∀L,U1,U2. R L U1 U2 → ∀K,d,e. ⇩[d, e] L ≡ K →
                             ∀T1. ⇧[d, e] T1 ≡ U1 →
                             ∃∃T2. ⇧[d, e] T2 ≡ U2 & R K T1 T2.
 
-definition dropable_sn: relation lenv → Prop ≝
+definition dropable_sn: predicate (relation lenv) ≝
                         λR. ∀L1,K1,d,e. ⇩[d, e] L1 ≡ K1 → ∀L2. R L1 L2 →
                         ∃∃K2. R K1 K2 & ⇩[d, e] L2 ≡ K2.
 
-definition dedropable_sn: relation lenv → Prop ≝
+definition dedropable_sn: predicate (relation lenv) ≝
                           λR. ∀L1,K1,d,e. ⇩[d, e] L1 ≡ K1 → ∀K2. R K1 K2 →
                           ∃∃L2. R L1 L2 & ⇩[d, e] L2 ≡ K2.
 
-definition dropable_dx: relation lenv → Prop ≝
+definition dropable_dx: predicate (relation lenv) ≝
                         λR. ∀L1,L2. R L1 L2 → ∀K2,e. ⇩[0, e] L2 ≡ K2 →
                         ∃∃K1. ⇩[0, e] L1 ≡ K1 & R K1 K2.
 
@@ -199,32 +198,21 @@ lemma ldrop_O1_lt: ∀L,i. i < |L| → ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V.
 ]
 qed.
 
-lemma ldrop_lsubr_ldrop2_abbr: ∀L1,L2,d,e. L1 ⊑ [d, e] L2 →
-                               ∀K2,V,i. ⇩[0, i] L2 ≡ K2. ⓓV →
-                               d ≤ i → i < d + e →
-                               ∃∃K1. K1 ⊑ [0, d + e - i - 1] K2 &
-                                     ⇩[0, i] L1 ≡ K1. ⓓV.
-#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
-[ #d #e #K1 #V #i #H
-  lapply (ldrop_inv_atom1 … H) -H #H destruct
-| #L1 #L2 #K1 #V #i #_ #_ #H
-  elim (lt_zero_false … H)
-| #L1 #L2 #V #e #HL12 #IHL12 #K1 #W #i #H #_ #Hie
-  elim (ldrop_inv_O1 … H) -H * #Hi #HLK1
-  [ -IHL12 -Hie destruct
-    <minus_n_O <minus_plus_m_m // /2 width=3/
-  | -HL12
-    elim (IHL12 … HLK1 ? ?) -IHL12 -HLK1 // /2 width=1/ -Hie >minus_minus_comm >arith_b1 // /4 width=3/
-  ]
-| #L1 #L2 #I #V1 #V2 #e #_ #IHL12 #K1 #W #i #H #_ #Hie
-  elim (ldrop_inv_O1 … H) -H * #Hi #HLK1
-  [ -IHL12 -Hie -Hi destruct
-  | elim (IHL12 … HLK1 ? ?) -IHL12 -HLK1 // /2 width=1/ -Hie >minus_minus_comm >arith_b1 // /3 width=3/
-  ]
-| #L1 #L2 #I1 #I2 #V1 #V2 #d #e #_ #IHL12 #K1 #V #i #H #Hdi >plus_plus_comm_23 #Hide
-  elim (le_inv_plus_l … Hdi) #Hdim #Hi
-  lapply (ldrop_inv_ldrop1 … H ?) -H // #HLK1
-  elim (IHL12 … HLK1 ? ?) -IHL12 -HLK1 // /2 width=1/ -Hdi -Hide >minus_minus_comm >arith_b1 // /3 width=3/
+lemma l_liftable_LTC: ∀R. l_liftable R → l_liftable (LTC … R).
+#R #HR #K #T1 #T2 #H elim H -T2
+[ /3 width=9/
+| #T #T2 #_ #HT2 #IHT1 #L #d #e #HLK #U1 #HTU1 #U2 #HTU2
+  elim (lift_total T d e) /4 width=11 by step/ (**) (* auto too slow without trace *)
+]
+qed.
+
+lemma l_deliftable_sn_LTC: ∀R. l_deliftable_sn R → l_deliftable_sn (LTC … R).
+#R #HR #L #U1 #U2 #H elim H -U2
+[ #U2 #HU12 #K #d #e #HLK #T1 #HTU1
+  elim (HR … HU12 … HLK … HTU1) -HR -L -U1 /3 width=3/
+| #U #U2 #_ #HU2 #IHU1 #K #d #e #HLK #T1 #HTU1
+  elim (IHU1 … HLK … HTU1) -IHU1 -U1 #T #HTU #HT1
+  elim (HR … HU2 … HLK … HTU) -HR -L -U /3 width=5/
 ]
 qed.
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lpx_sn.ma
index 98a7c7157..41490973f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lpx_sn.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lpx_sn.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/grammar/lenv_px_sn.ma".
+include "basic_2/grammar/lpx_sn.ma".
 include "basic_2/relocation/ldrop.ma".
 
 (* DROPPING *****************************************************************)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lift.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lift.ma
index 7e7961eab..909b02125 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lift.ma
@@ -35,14 +35,6 @@ inductive lift: nat → nat → relation term ≝
 
 interpretation "relocation" 'RLift d e T1 T2 = (lift d e T1 T2).
 
-definition t_liftable: relation term → Prop ≝
-                       λR. ∀T1,T2. R T1 T2 → ∀U1,d,e. ⇧[d, e] T1 ≡ U1 →
-                       ∀U2. ⇧[d, e] T2 ≡ U2 → R U1 U2.
-
-definition t_deliftable_sn: relation term → Prop ≝
-                            λR. ∀U1,U2. R U1 U2 → ∀T1,d,e. ⇧[d, e] T1 ≡ U1 →
-                            ∃∃T2. ⇧[d, e] T2 ≡ U2 & R T1 T2.
-
 (* Basic inversion lemmas ***************************************************)
 
 fact lift_inv_refl_O2_aux: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → e = 0 → T1 = T2.
@@ -378,24 +370,6 @@ lemma is_lift_dec: ∀T2,d,e. Decidable (∃T1. ⇧[d,e] T1 ≡ T2).
 ]
 qed.
 
-lemma t_liftable_TC: ∀R. t_liftable R → t_liftable (TC … R).
-#R #HR #T1 #T2 #H elim H -T2
-[ /3 width=7/
-| #T #T2 #_ #HT2 #IHT1 #U1 #d #e #HTU1 #U2 #HTU2
-  elim (lift_total T d e) /3 width=9/
-]
-qed.
-
-lemma t_deliftable_sn_TC: ∀R. t_deliftable_sn R → t_deliftable_sn (TC … R).
-#R #HR #U1 #U2 #H elim H -U2
-[ #U2 #HU12 #T1 #d #e #HTU1
-  elim (HR … HU12 … HTU1) -U1 /3 width=3/
-| #U #U2 #_ #HU2 #IHU1 #T1 #d #e #HTU1
-  elim (IHU1 … HTU1) -U1 #T #HTU #HT1
-  elim (HR … HU2 … HTU) -U /3 width=5/
-]
-qed-.
-
 (* Basic_1: removed theorems 7:
             lift_head lift_gen_head
             lift_weight_map lift_weight lift_weight_add lift_weight_add_O
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpss.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpss.ma
index 993669ad4..f6bae4fa2 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpss.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpss.ma
@@ -13,6 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/relocation/ldrop_append.ma".
+include "basic_2/substitution/lsubr.ma".
 
 (* CONTEXT-SENSITIVE PARALLEL SUBSTITUTION FOR TERMS ************************)
 
@@ -34,16 +35,11 @@ interpretation "context-sensitive parallel substitution (term)"
 
 (* Basic properties *********************************************************)
 
-(* Note: it does not hold replacing |L1| with |L2| *)
-lemma cpss_lsubr_trans: ∀L1,T1,T2. L1 ⊢ T1 ▶* T2 →
-                        ∀L2. L2 ⊑ [0, |L1|] L1 → L2 ⊢ T1 ▶* T2.
+lemma cpss_lsubr_trans: lsubr_trans … cpss.
 #L1 #T1 #T2 #H elim H -L1 -T1 -T2
 [ //
 | #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
-  lapply (ldrop_fwd_ldrop2_length … HLK1) #Hi
-  lapply (ldrop_fwd_O1_length … HLK1) #H2i
-  elim (ldrop_lsubr_ldrop2_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // -Hi
-  <H2i -H2i <minus_plus_m_m /3 width=6/
+  elim (lsubr_fwd_ldrop2_abbr … HL12 … HLK1) -HL12 -HLK1 /3 width=6/
 | /4 width=1/
 | /3 width=1/
 ]
@@ -63,10 +59,10 @@ lemma cpss_delift: ∀K,V,T1,L,d. ⇩[0, d] L ≡ (K. ⓓV) →
   elim (lt_or_eq_or_gt i d) #Hid /3 width=4/
   destruct
   elim (lift_total V 0 (i+1)) #W #HVW
-  elim (lift_split … HVW i i ? ? ?) // /3 width=6/
+  elim (lift_split … HVW i i) // /3 width=6/
 | * [ #a ] #I #W1 #U1 #IHW1 #IHU1 #L #d #HLK
   elim (IHW1 … HLK) -IHW1 #W2 #W #HW12 #HW2
-  [ elim (IHU1 (L. ⓑ{I} W1) (d+1) ?) -IHU1 /2 width=1/ -HLK /3 width=9/
+  [ elim (IHU1 (L. ⓑ{I} W1) (d+1)) -IHU1 /2 width=1/ -HLK /3 width=9/
   | elim (IHU1 … HLK) -IHU1 -HLK /3 width=8/
   ]
 ]
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lpss.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lpss.ma
index d440960f1..0c806c49f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lpss.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lpss.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/grammar/lenv_px_sn.ma".
+include "basic_2/grammar/lpx_sn.ma".
 include "basic_2/substitution/cpss.ma".
 
 (* SN PARALLEL SUBSTITUTION FOR LOCAL ENVIRONMENTS **************************)
@@ -45,6 +45,10 @@ lemma lpss_inv_pair2: ∀I,L1,K2,V2. L1 ⊢ ▶* K2. ⓑ{I} V2 →
 lemma lpss_refl: ∀L. L ⊢ ▶* L.
 /2 width=1 by lpx_sn_refl/ qed.
 
+lemma lpss_pair: ∀I,K1,K2,V1,V2. K1 ⊢ ▶* K2 → K1 ⊢ V1 ▶* V2 →
+                 K1.ⓑ{I}V1 ⊢ ▶* K2.ⓑ{I}V2.
+/2 width=1/ qed.
+
 lemma lpss_append: ∀K1,K2. K1 ⊢ ▶* K2 → ∀L1,L2. L1 ⊢ ▶* L2 →
                     L1 @@ K1 ⊢ ▶* L2 @@ K2.
 /3 width=1 by lpx_sn_append, cpss_append/ qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lpss_cpss.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lpss_cpss.ma
index a67eaeb05..2a418d759 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lpss_cpss.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lpss_cpss.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basic_2/grammar/lpx_sn_lpx_sn.ma".
 include "basic_2/relocation/fsup.ma".
 include "basic_2/substitution/lpss_ldrop.ma".
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr.ma
new file mode 100644
index 000000000..e3afc573d
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr.ma
@@ -0,0 +1,111 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/relocation/ldrop.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR SUBSTITUTION ****************************)
+
+inductive lsubr: relation lenv ≝
+| lsubr_sort: ∀L. lsubr L (⋆)
+| lsubr_abbr: ∀L1,L2,V. lsubr L1 L2 → lsubr (L1. ⓓV) (L2.ⓓV)
+| lsubr_abst: ∀I,L1,L2,V1,V2. lsubr L1 L2 → lsubr (L1. ⓑ{I}V1) (L2. ⓛV2)
+.
+
+interpretation
+  "local environment refinement (substitution)"
+  'SubEq L1 L2 = (lsubr L1 L2).
+
+definition lsubr_trans: ∀S. predicate (lenv → relation S) ≝ λS,R.
+                        ∀L2,s1,s2. R L2 s1 s2 → ∀L1. L1 ⊑ L2 → R L1 s1 s2.
+
+(* Basic properties *********************************************************)
+
+lemma lsubr_bind: ∀I,L1,L2,V. L1 ⊑ L2 → L1. ⓑ{I} V ⊑ L2.ⓑ{I} V.
+* /2 width=1/ qed.
+
+lemma lsubr_abbr: ∀I,L1,L2,V. L1 ⊑ L2 → L1. ⓓV ⊑ L2. ⓑ{I}V.
+* /2 width=1/ qed.
+
+lemma lsubr_refl: ∀L. L ⊑ L.
+#L elim L -L // /2 width=1/
+qed.
+
+lemma TC_lsubr_trans: ∀S,R. lsubr_trans S R → lsubr_trans S (LTC … R).
+#S #R #HR #L1 #s1 #s2 #H elim H -s2
+[ /3 width=3/
+| #s #s2 #_ #Hs2 #IHs1 #L2 #HL12
+  lapply (HR … Hs2 … HL12) -HR -Hs2 /3 width=3/
+]
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact lsubr_inv_atom1_aux: ∀L1,L2. L1 ⊑ L2 → L1 = ⋆ → L2 = ⋆.
+#L1 #L2 * -L1 -L2 //
+[ #L1 #L2 #V #_ #H destruct
+| #I #L1 #L2 #V1 #V2 #_ #H destruct
+]
+qed-.
+
+lemma lsubr_inv_atom1: ∀L2. ⋆ ⊑ L2 → L2 = ⋆.
+/2 width=3 by lsubr_inv_atom1_aux/ qed-.
+
+fact lsubr_inv_abbr2_aux: ∀L1,L2. L1 ⊑ L2 → ∀K2,W. L2 = K2.ⓓW →
+                          ∃∃K1. K1 ⊑ K2 & L1 = K1.ⓓW.
+#L1 #L2 * -L1 -L2
+[ #L #K2 #W #H destruct
+| #L1 #L2 #V #HL12 #K2 #W #H destruct /2 width=3/
+| #I #L1 #L2 #V1 #V2 #_ #K2 #W #H destruct
+]
+qed-.
+
+lemma lsubr_inv_abbr2: ∀L1,K2,W. L1 ⊑ K2.ⓓW →
+                       ∃∃K1. K1 ⊑ K2 & L1 = K1.ⓓW.
+/2 width=3 by lsubr_inv_abbr2_aux/ qed-.
+
+fact lsubr_inv_abst2_aux: ∀L1,L2. L1 ⊑ L2 → ∀K2,W2. L2 = K2.ⓛW2 →
+                          ∃∃I,K1,W1. K1 ⊑ K2 & L1 = K1.ⓑ{I}W1.
+#L1 #L2 * -L1 -L2
+[ #L #K2 #W2 #H destruct
+| #L1 #L2 #V #_ #K2 #W2 #H destruct
+| #I #L1 #L2 #V1 #V2 #HL12 #K2 #W2 #H destruct /2 width=5/
+]
+qed-.
+
+lemma lsubr_inv_abst2: ∀L1,K2,W2. L1 ⊑ K2.ⓛW2 →
+                       ∃∃I,K1,W1. K1 ⊑ K2 & L1 = K1.ⓑ{I}W1.
+/2 width=4 by lsubr_inv_abst2_aux/ qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lsubr_fwd_length: ∀L1,L2. L1 ⊑ L2 → |L2| ≤ |L1|.
+#L1 #L2 #H elim H -L1 -L2 // /2 width=1/
+qed-.
+
+lemma lsubr_fwd_ldrop2_abbr: ∀L1,L2. L1 ⊑ L2 →
+                             ∀K2,W,i. ⇩[0, i] L2 ≡ K2. ⓓW →
+                             ∃∃K1. K1 ⊑ K2 & ⇩[0, i] L1 ≡ K1. ⓓW.
+#L1 #L2 #H elim H -L1 -L2
+[ #L #K2 #W #i #H
+  lapply (ldrop_inv_atom1 … H) -H #H destruct
+| #L1 #L2 #V #HL12 #IHL12 #K2 #W #i #H
+  elim (ldrop_inv_O1 … H) -H * #Hi #HLK2 destruct [ -IHL12 | -HL12 ]
+  [ /2 width=3/
+  | elim (IHL12 … HLK2) -IHL12 -HLK2 /3 width=3/
+  ]
+| #I #L1 #L2 #V1 #V2 #_ #IHL12 #K2 #W #i #H
+  elim (ldrop_inv_O1 … H) -H * #Hi #HLK2 destruct
+  elim (IHL12 … HLK2) -IHL12 -HLK2 /3 width=3/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr_lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr_lsubr.ma
new file mode 100644
index 000000000..426166ab6
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr_lsubr.ma
@@ -0,0 +1,64 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/lsubr.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR SUBSTITUTION ****************************)
+
+fact lsubr_inv_abbr1_aux: ∀L1,L2. L1 ⊑ L2 → ∀K1,W. L1 = K1.ⓓW →
+                          ∨∨ L2 = ⋆
+                           | ∃∃K2. K1 ⊑ K2 & L2 = K2.ⓓW
+                           | ∃∃K2,W2. K1 ⊑ K2 & L2 = K2.ⓛW2.
+#L1 #L2 * -L1 -L2
+[ #L #K1 #W #H destruct /2 width=1/
+| #L1 #L2 #V #HL12 #K1 #W #H destruct /3 width=3/
+| #I #L1 #L2 #V1 #V2 #HL12 #K1 #W #H destruct /3 width=4/
+]
+qed-.
+
+lemma lsubr_inv_abbr1: ∀K1,L2,W. K1.ⓓW ⊑ L2 →
+                       ∨∨ L2 = ⋆
+                        | ∃∃K2. K1 ⊑ K2 & L2 = K2.ⓓW
+                        | ∃∃K2,W2. K1 ⊑ K2 & L2 = K2.ⓛW2.
+/2 width=3 by lsubr_inv_abbr1_aux/ qed-.
+
+fact lsubr_inv_abst1_aux: ∀L1,L2. L1 ⊑ L2 → ∀K1,W1. L1 = K1.ⓛW1 →
+                          L2 = ⋆ ∨
+                          ∃∃K2,W2. K1 ⊑ K2 & L2 = K2.ⓛW2.
+#L1 #L2 * -L1 -L2
+[ #L #K1 #W1 #H destruct /2 width=1/
+| #L1 #L2 #V #_ #K1 #W1 #H destruct
+| #I #L1 #L2 #V1 #V2 #HL12 #K1 #W1 #H destruct /3 width=4/
+]
+qed-.
+
+lemma lsubr_inv_abst1: ∀K1,L2,W1. K1.ⓛW1 ⊑ L2 →
+                       L2 = ⋆ ∨
+                       ∃∃K2,W2. K1 ⊑ K2 & L2 = K2.ⓛW2.
+/2 width=4 by lsubr_inv_abst1_aux/ qed-.
+
+(* Main properties **********************************************************)
+
+theorem lsubr_trans: Transitive … lsubr.
+#L1 #L #H elim H -L1 -L
+[ #L1 #X #H
+  lapply (lsubr_inv_atom1 … H) -H //
+| #L1 #L #V #_ #IHL1 #X #H
+  elim (lsubr_inv_abbr1 … H) -H // *
+  #L2 [2: #V2 ] #HL2 #H destruct /3 width=1/
+| #I #L1 #L #V1 #V #_ #IHL1 #X #H
+  elim (lsubr_inv_abst1 … H) -H // *
+  #L2 #V2 #HL2 #H destruct /3 width=1/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/cpqs.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/cpqs.ma
index dbe7beff1..cddb52b6e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/cpqs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/cpqs.ma
@@ -37,16 +37,11 @@ interpretation "context-sensitive restricted parallel computation (term)"
 
 (* Basic properties *********************************************************)
 
-(* Note: it does not hold replacing |L1| with |L2| *)
-lemma cpqs_lsubr_trans: ∀L1,T1,T2. L1 ⊢ T1 ➤* T2 →
-                        ∀L2. L2 ⊑ [0, |L1|] L1 → L2 ⊢ T1 ➤* T2.
+lemma cpqs_lsubr_trans: lsubr_trans … cpqs.
 #L1 #T1 #T2 #H elim H -L1 -T1 -T2
 [ //
 | #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
-  lapply (ldrop_fwd_ldrop2_length … HLK1) #Hi
-  lapply (ldrop_fwd_O1_length … HLK1) #H2i
-  elim (ldrop_lsubr_ldrop2_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // -Hi
-  <H2i -H2i <minus_plus_m_m /3 width=6/
+  elim (lsubr_fwd_ldrop2_abbr … HL12 … HLK1) -HL12 -HLK1 /3 width=6/
 | /4 width=1/
 |4,6: /3 width=1/
 | /4 width=3/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lpqs.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lpqs.ma
index b3f6ee4d0..29e577c16 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/lpqs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/lpqs.ma
@@ -43,6 +43,10 @@ lemma lpqs_inv_pair2: ∀I,L1,K2,V2. L1 ⊢ ➤* K2. ⓑ{I} V2 →
 lemma lpqs_refl: ∀L. L ⊢ ➤* L.
 /2 width=1 by lpx_sn_refl/ qed.
 
+lemma lpqs_pair: ∀I,K1,K2,V1,V2. K1 ⊢ ➤* K2 → K1 ⊢ V1 ➤* V2 →
+                 K1.ⓑ{I}V1 ⊢ ➤* K2.ⓑ{I}V2.
+/2 width=1/ qed.
+
 lemma lpqs_append: ∀K1,K2. K1 ⊢ ➤* K2 → ∀L1,L2. L1 ⊢ ➤* L2 →
                    L1 @@ K1 ⊢ ➤* L2 @@ K2.
 /3 width=1 by lpx_sn_append, cpqs_append/ qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lpqs_cpqs.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lpqs_cpqs.ma
index 47d3b7cdf..d546005bb 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/lpqs_cpqs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/lpqs_cpqs.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basic_2/grammar/lpx_sn_lpx_sn.ma".
 include "basic_2/relocation/fsup.ma".
 include "basic_2/unfold/lpqs_ldrop.ma".
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
index 5fa65b5dd..a2d504130 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
@@ -100,12 +100,8 @@ table {
           }
         ]
         [ { "context-sensitive computation" * } {
-             [ "cprs (? ⊢ ? ➡* ?)" "cprs_lift" + "cprs_tpss" + "cprs_ltpss_dx" + "cprs_ltpss_sn" + "cprs_delift" + "cprs_aaa" + "cprs_ltpr" + "cprs_lfpr" + "cprs_cprs" + "cprs_lfprs" + "cprs_tstc" + "cprs_tstc_vector" * ]
-          }
-        ]
-        [ { "context-free computation" * } {
-             [ "ltprs ( ? ➡* ? )" "ltprs_alt ( ? ➡➡* ? )" "ltprs_ldrop" + "ltprs_ltprs" * ]
-             [ "tprs ( ? ➡* ?)" "tprs_lift" + "tprs_tprs" * ]
+             [ "lprs ( ? ⊢ ➡* ? )" "lprs_alt ( ? ⊢ ➡➡* ? )" "lprs_ldrop" + "lprs_aaa" + "lprs_cprs" + "lprs_lprs" * ]
+             [ "cprs ( ? ⊢ ? ➡* ?)" "cprs_lift" + "cprs_tpss" + "cprs_ltpss_dx" + "cprs_ltpss_sn" + "cprs_aaa" + "cprs_lpr" + "cprs_cprs" + "cprs_tstc" + "cprs_tstc_vector" * ]
           }
         ]
         [ { "local env. ref. for abstract candidates of reducibility" * } {
@@ -122,12 +118,11 @@ table {
    [ { "reduction" * } {
         [ { "context-sensitive normal forms" * } {
              [ "cnf ( ? ⊢ 𝐍⦃?⦄ )" "cnf_liftt" + "cnf_crf" + "cnf_cif" * ]
-             [ "chnf ( ? ⊢ 𝐇𝐍⦃?⦄ )" * ]
           }
         ]
         [ { "context-sensitive reduction" * } {
              [ "lpr ( ? ⊢ ➡ ? )" "lpr_ldrop" + "lpr_cpss" + "lpr_lpss" + "lpr_aaa" + "lpr_cpr" + "lpr_lpr" * ]
-             [ "cpr ( ? ⊢ ? ➡ ? )" "lpr_tshf" + "cpr_lift" + "cpr_cif" * ]
+             [ "cpr ( ? ⊢ ? ➡ ? )" "cpr_lift" + "cpr_cif" * ]
           }
         ]
         [ { "context-sensitive reducible forms" * } {
@@ -180,6 +175,10 @@ table {
              [ "cpss ( ? ⊢ ? ▶* ? )" "cpss_lift" * ]
           }
         ]        
+        [ { "local env. ref. for substitution" * } {
+             [ "lsubr ( ? ⊑ ? )" "lsubr_lsubr" * ]
+          }
+        ]
         [ { "iterated structural successor for closures" * } {
              [ "fsups ( ⦃?,?⦄ ⊃* ⦃?,?⦄ )" "fsups_fsups" * ]
              [ "fsupp ( ⦃?,?⦄ ⊃+ ⦃?,?⦄ )" "fsupp_fsupp" * ]
@@ -211,11 +210,7 @@ table {
           }
         ]
         [ { "basic local env. slicing" * } {
-             [ "ldrop ( ⇩[?,?] ? ≡ ? )" "ldrop_append" + "ldrop_lpx" + "ldrop_lpx_sn" + "ldrop_lbotr" + "ldrop_ldrop" * ]
-          }
-        ]
-        [ { "local env. ref. for substitution" * } {
-             [ "lsubr ( ? ⊑[?,?] ? )" "(lsubr_lsubr)" "lsubr_lbotr ( ⊒[?,?] ? )" * ]
+             [ "ldrop ( ⇩[?,?] ? ≡ ? )" "ldrop_append" + "ldrop_lpx_sn" + "ldrop_ldrop" * ]
           }
         ]
         [ { "basic term relocation" * } {
@@ -227,8 +222,8 @@ table {
    ]
    class "red"
    [ { "grammar" * } {
-        [ { "same head term form" * } {
-             [ "tshf ( ? ≈ ? )" "(tshf_tshf)" * ]
+	[ { "pointwise extension of a relation" * } {
+             [ "lpx_sn" "lpx_sn_tc" + "lpx_sn_lpx_sn" * ]
           }
         ]
         [ { "same top term constructor" * } {
@@ -241,7 +236,7 @@ table {
         ]
         [ { "internal syntax" * } {
              [ "genv" * ]
-             [ "lenv" "lenv_weight ( ♯{?} )" "lenv_length ( |?| )" "lenv_append ( ? @@ ? )" "lenv_px" + "lenv_px_sn" + "lenv_px_bi" * ]
+             [ "lenv" "lenv_weight ( ♯{?} )" "lenv_length ( |?| )" "lenv_append ( ? @@ ? )" * ]
              [ "term" "term_weight ( ♯{?} )" "term_simple ( 𝐒⦃?⦄ )" "term_vector" * ]
              [ "item" * ]
           }
diff --git a/matita/matita/contribs/lambdadelta/ground_2/star.ma b/matita/matita/contribs/lambdadelta/ground_2/star.ma
index 431ef80a8..1358f8da2 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/star.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/star.ma
@@ -35,6 +35,15 @@ definition bi_confluent:  ∀A,B. ∀R: bi_relation A B. Prop ≝ λA,B,R.
                           ∀a0,a1,b0,b1. R a0 b0 a1 b1 → ∀a2,b2. R a0 b0 a2 b2 →
                           ∃∃a,b. R a1 b1 a b & R a2 b2 a b.
 
+definition LTC: ∀A:Type[0]. ∀B. (A→relation B) → (A→relation B) ≝
+                λA,B,R,a. TC … (R a).
+
+definition s_r_trans: ∀A,B. relation2 (A→relation B) (relation A) ≝ λA,B,R1,R2.
+                      ∀L2,T1,T2. R1 L2 T1 T2 → ∀L1. R2 L1 L2 → LTC … R1 L1 T1 T2.
+
+definition s_rs_trans: ∀A,B. relation2 (A→relation B) (relation A) ≝ λA,B,R1,R2.
+                       ∀L2,T1,T2. LTC … R1 L2 T1 T2 → ∀L1. R2 L1 L2 → LTC … R1 L1 T1 T2.
+
 lemma TC_strip1: ∀A,R1,R2. confluent2 A R1 R2 →
                  ∀a0,a1. TC … R1 a0 a1 → ∀a2. R2 a0 a2 →
                  ∃∃a. R2 a1 a & TC … R1 a2 a.
@@ -115,7 +124,7 @@ inductive SN (A) (R,S:relation A): predicate A ≝
 lemma NF_to_SN: ∀A,R,S,a. NF A R S a → SN A R S a.
 #A #R #S #a1 #Ha1
 @SN_intro #a2 #HRa12 #HSa12
-elim (HSa12 ?) -HSa12 /2 width=1/
+elim HSa12 -HSa12 /2 width=1/
 qed.
 
 definition NF_sn: ∀A. relation A → relation A → predicate A ≝
@@ -128,7 +137,7 @@ inductive SN_sn (A) (R,S:relation A): predicate A ≝
 lemma NF_to_SN_sn: ∀A,R,S,a. NF_sn A R S a → SN_sn A R S a.
 #A #R #S #a2 #Ha2
 @SN_sn_intro #a1 #HRa12 #HSa12
-elim (HSa12 ?) -HSa12 /2 width=1/
+elim HSa12 -HSa12 /2 width=1/
 qed.
 
 lemma bi_TC_strip: ∀A,B,R. bi_confluent A B R →
@@ -164,8 +173,18 @@ lemma bi_TC_decomp_l: ∀A,B. ∀R:bi_relation A B.
                       ∀a1,a2,b1,b2. bi_TC … R a1 b1 a2 b2 →
                       R a1 b1 a2 b2 ∨
                       ∃∃a,b. R a1 b1 a b & bi_TC … R a b a2 b2.
-#A #B #R #a1 #a2 #b1 #b2 #H @(bi_TC_ind_dx ?????????? H) -a1 -b1
+#A #B #R #a1 #a2 #b1 #b2 #H @(bi_TC_ind_dx … a1 b1 H) -a1 -b1
 [ /2 width=1/
 | #a1 #a #b1 #b #Hab1 #Hab2 #_ /3 width=4/
 ]
 qed-.
+
+lemma s_r_trans_TC1: ∀A,B,R,S. s_r_trans A B R S → s_rs_trans A B R S.
+#A #B #R #S #HRS #L2 #T1 #T2 #H elim H -T2 [ /3 width=3/ ]
+#T #T2 #_ #HT2 #IHT1 #L1 #HL12
+lapply (HRS … HT2 … HL12) -HRS -HT2 /3 width=3/
+qed-.
+
+lemma s_r_trans_TC2: ∀A,B,R,S. s_rs_trans A B R S → s_r_trans A B R (TC … S).
+#A #B #R #S #HRS #L2 #T1 #T2 #HT12 #L1 #H @(TC_ind_dx … L1 H) -L1 /2 width=3/ /3 width=3/
+qed-.
-- 
2.39.2