From: Ferruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
Date: Fri, 25 May 2018 14:39:04 +0000 (+0200)
Subject: partial update update in basic_2
X-Git-Tag: make_still_working~316
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6b35f96790b871aa06b22045b4e8e8dd7bba6590;p=helm.git

partial update update in basic_2

+ lpxs reconstructed
---

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpxs/cpxs_fqus.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpxs/cpxs_fqus.etc
new file mode 100644
index 000000000..2509cf852
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpxs/cpxs_fqus.etc
@@ -0,0 +1,24 @@
+(* Properties on supclosure *************************************************)
+
+lemma lpx_fqup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ →
+                      ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 →
+                      ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊐+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
+[ #G2 #L2 #T2 #H12 #K1 #HKL1 elim (lpx_fqu_trans … H12 … HKL1) -L1
+  /3 width=5 by cpx_cpxs, fqu_fqup, ex3_2_intro/
+| #G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1
+  #L0 #T0 #HT10 #HT0 #HL0 elim (lpx_fqu_trans … H2 … HL0) -L
+  #L #T3 #HT3 #HT32 #HL2 elim (fqup_cpx_trans … HT0 … HT3) -T
+  /3 width=7 by cpxs_strap1, fqup_strap1, ex3_2_intro/
+]
+qed-.
+
+lemma lpx_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ →
+                      ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 →
+                      ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊐* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -G2 -L2 -T2 [ /2 width=5 by ex3_2_intro/ ]
+#G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1
+#L0 #T0 #HT10 #HT0 #HL0 elim (lpx_fquq_trans … H2 … HL0) -L
+#L #T3 #HT3 #HT32 #HL2 elim (fqus_cpx_trans … HT0 … HT3) -T
+/3 width=7 by cpxs_strap1, fqus_strap1, ex3_2_intro/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lfpxs/lfpxs_cpxs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lfpxs/lfpxs_cpxs.etc
deleted file mode 100644
index a6eb3b6ac..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/lfpxs/lfpxs_cpxs.etc
+++ /dev/null
@@ -1,27 +0,0 @@
-(* Advanced inversion lemmas ************************************************)
-
-lemma lpxs_inv_pair1: ∀h,o,I,G,K1,L2,V1. ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡*[h, o] L2 →
-                      ∃∃K2,V2. ⦃G, K1⦄ ⊢ ➡*[h, o] K2 & ⦃G, K1⦄ ⊢ V1 ➡*[h, o] V2 & L2 = K2.ⓑ{I}V2.
-/3 width=3 by TC_lpx_sn_inv_pair1, lpx_cpxs_trans/ qed-.
-
-lemma lpxs_inv_pair2: ∀h,o,I,G,L1,K2,V2. ⦃G, L1⦄ ⊢ ➡*[h, o] K2.ⓑ{I}V2 →
-                      ∃∃K1,V1. ⦃G, K1⦄ ⊢ ➡*[h, o] K2 & ⦃G, K1⦄ ⊢ V1 ➡*[h, o] V2 & L1 = K1.ⓑ{I}V1.
-/3 width=3 by TC_lpx_sn_inv_pair2, lpx_cpxs_trans/ qed-.
-
-(* Advanced eliminators *****************************************************)
-
-lemma lpxs_ind_alt: ∀h,o,G. ∀R:relation lenv.
-                    R (⋆) (⋆) → (
-                       ∀I,K1,K2,V1,V2.
-                       ⦃G, K1⦄ ⊢ ➡*[h, o] K2 → ⦃G, K1⦄ ⊢ V1 ➡*[h, o] V2 →
-                       R K1 K2 → R (K1.ⓑ{I}V1) (K2.ⓑ{I}V2)
-                    ) →
-                    ∀L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, o] L2 → R L1 L2.
-/3 width=4 by TC_lpx_sn_ind, lpx_cpxs_trans/ qed-.
-
-
-(* More advanced properties *************************************************)
-
-lemma lpxs_pair2: ∀h,o,I,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, o] L2 →
-                  ∀V1,V2. ⦃G, L2⦄ ⊢ V1 ➡*[h, o] V2 → ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡*[h, o] L2.ⓑ{I}V2.
-/3 width=3 by lpxs_pair, lpxs_cpxs_trans/ qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lfpxs/lfpxs_lreq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lfpxs/lfpxs_lreq.etc
deleted file mode 100644
index fc77921e7..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/lfpxs/lfpxs_lreq.etc
+++ /dev/null
@@ -1,29 +0,0 @@
-fact lreq_lpxs_trans_lleq_aux: ∀h,o,G,L1,L0,l,k. L1 ⩬[l, k] L0 → k = ∞ →
-                               ∀L2. ⦃G, L0⦄ ⊢ ➡*[h, o] L2 →
-                               ∃∃L. L ⩬[l, k] L2 & ⦃G, L1⦄ ⊢ ➡*[h, o] L &
-                                    (∀T. L0 ≡[T, l] L2 ↔ L1 ≡[T, l] L).
-#h #o #G #L1 #L0 #l #k #H elim H -L1 -L0 -l -k
-[ #l #k #_ #L2 #H >(lpxs_inv_atom1 … H) -H
-  /3 width=5 by ex3_intro, conj/
-| #I1 #I0 #L1 #L0 #V1 #V0 #_ #_ #Hm destruct
-| #I #L1 #L0 #V1 #k #HL10 #IHL10 #Hm #Y #H
-  elim (lpxs_inv_pair1 … H) -H #L2 #V2 #HL02 #HV02 #H destruct
-  lapply (ysucc_inv_Y_dx … Hm) -Hm #Hm
-  elim (IHL10 … HL02) // -IHL10 -HL02 #L #HL2 #HL1 #IH
-  @(ex3_intro … (L.ⓑ{I}V2)) /3 width=3 by lpxs_pair, lreq_cpxs_trans, lreq_pair/
-  #T elim (IH T) #HL0dx #HL0sn
-  @conj #H @(lleq_lreq_repl … H) -H /3 width=1 by lreq_sym, lreq_pair_O_Y/
-| #I1 #I0 #L1 #L0 #V1 #V0 #l #k #HL10 #IHL10 #Hm #Y #H
-  elim (lpxs_inv_pair1 … H) -H #L2 #V2 #HL02 #HV02 #H destruct
-  elim (IHL10 … HL02) // -IHL10 -HL02 #L #HL2 #HL1 #IH
-  @(ex3_intro … (L.ⓑ{I1}V1)) /3 width=1 by lpxs_pair, lreq_succ/
-  #T elim (IH T) #HL0dx #HL0sn
-  @conj #H @(lleq_lreq_repl … H) -H /3 width=1 by lreq_sym, lreq_succ/
-]
-qed-.
-
-lemma lreq_lpxs_trans_lleq: ∀h,o,G,L1,L0,l. L1 ⩬[l, ∞] L0 →
-                            ∀L2. ⦃G, L0⦄ ⊢ ➡*[h, o] L2 →
-                            ∃∃L. L ⩬[l, ∞] L2 & ⦃G, L1⦄ ⊢ ➡*[h, o] L &
-                                 (∀T. L0 ≡[T, l] L2 ↔ L1 ≡[T, l] L).
-/2 width=1 by lreq_lpxs_trans_lleq_aux/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn_tc.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn_tc.etc
new file mode 100644
index 000000000..51b09380f
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn_tc.etc
@@ -0,0 +1,91 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/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 by lpx_sn_pair, step/
+]
+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-.
+
+(* 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
+[ /2 width=2 by lpx_sn_inv_atom2/
+| #L1 #L #HL1 #_ #IHL2 destruct /2 width=2 by lpx_sn_inv_atom2/
+]
+qed-.
+
+lemma TC_lpx_sn_inv_pair2: ∀R. s_rs_transitive … 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 by inj, ex3_2_intro/
+| #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 /3 width=5 by TC_strap, ex3_2_intro/
+]
+qed-.
+
+lemma TC_lpx_sn_inv_atom1: ∀R,L2. TC … (lpx_sn R) (⋆) L2 → L2 = ⋆.
+#R #L2 #H elim H -L2
+[ /2 width=2 by lpx_sn_inv_atom1/
+| #L #L2 #_ #HL2 #IHL1 destruct /2 width=2 by lpx_sn_inv_atom1/
+]
+qed-.
+
+fact TC_lpx_sn_inv_pair1_aux: ∀R. s_rs_transitive … 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 by ex3_2_intro/
+]
+qed-.
+
+lemma TC_lpx_sn_inv_pair1: ∀R. s_rs_transitive … 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-.
+
+(* 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/etc/lpxs/lpxs_lreq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpxs/lpxs_lreq.etc
new file mode 100644
index 000000000..fc77921e7
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpxs/lpxs_lreq.etc
@@ -0,0 +1,29 @@
+fact lreq_lpxs_trans_lleq_aux: ∀h,o,G,L1,L0,l,k. L1 ⩬[l, k] L0 → k = ∞ →
+                               ∀L2. ⦃G, L0⦄ ⊢ ➡*[h, o] L2 →
+                               ∃∃L. L ⩬[l, k] L2 & ⦃G, L1⦄ ⊢ ➡*[h, o] L &
+                                    (∀T. L0 ≡[T, l] L2 ↔ L1 ≡[T, l] L).
+#h #o #G #L1 #L0 #l #k #H elim H -L1 -L0 -l -k
+[ #l #k #_ #L2 #H >(lpxs_inv_atom1 … H) -H
+  /3 width=5 by ex3_intro, conj/
+| #I1 #I0 #L1 #L0 #V1 #V0 #_ #_ #Hm destruct
+| #I #L1 #L0 #V1 #k #HL10 #IHL10 #Hm #Y #H
+  elim (lpxs_inv_pair1 … H) -H #L2 #V2 #HL02 #HV02 #H destruct
+  lapply (ysucc_inv_Y_dx … Hm) -Hm #Hm
+  elim (IHL10 … HL02) // -IHL10 -HL02 #L #HL2 #HL1 #IH
+  @(ex3_intro … (L.ⓑ{I}V2)) /3 width=3 by lpxs_pair, lreq_cpxs_trans, lreq_pair/
+  #T elim (IH T) #HL0dx #HL0sn
+  @conj #H @(lleq_lreq_repl … H) -H /3 width=1 by lreq_sym, lreq_pair_O_Y/
+| #I1 #I0 #L1 #L0 #V1 #V0 #l #k #HL10 #IHL10 #Hm #Y #H
+  elim (lpxs_inv_pair1 … H) -H #L2 #V2 #HL02 #HV02 #H destruct
+  elim (IHL10 … HL02) // -IHL10 -HL02 #L #HL2 #HL1 #IH
+  @(ex3_intro … (L.ⓑ{I1}V1)) /3 width=1 by lpxs_pair, lreq_succ/
+  #T elim (IH T) #HL0dx #HL0sn
+  @conj #H @(lleq_lreq_repl … H) -H /3 width=1 by lreq_sym, lreq_succ/
+]
+qed-.
+
+lemma lreq_lpxs_trans_lleq: ∀h,o,G,L1,L0,l. L1 ⩬[l, ∞] L0 →
+                            ∀L2. ⦃G, L0⦄ ⊢ ➡*[h, o] L2 →
+                            ∃∃L. L ⩬[l, ∞] L2 & ⦃G, L1⦄ ⊢ ➡*[h, o] L &
+                                 (∀T. L0 ≡[T, l] L2 ↔ L1 ≡[T, l] L).
+/2 width=1 by lreq_lpxs_trans_lleq_aux/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs.etc
new file mode 100644
index 000000000..0e1bee1d1
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs.etc
@@ -0,0 +1,56 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/notation/relations/predtysnstar_5.ma".
+include "basic_2/i_static/tc_lfxs.ma".
+include "basic_2/rt_transition/lfpx.ma".
+
+(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******)
+
+definition lfpxs: ∀h. relation4 genv term lenv lenv ≝
+                  λh,G. tc_lfxs (cpx h G).
+
+interpretation
+   "unbound parallel rt-computation on referred entries (local environment)"
+   'PRedTySnStar h T G L1 L2 = (lfpxs h G T L1 L2).
+
+(* Basic properties *********************************************************)
+
+(* Basic_2A1: was just: lpx_lpxs *)
+lemma lfpx_lfpxs: ∀h,G,T,L1,L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2.
+/2 width=1 by inj/ qed.
+
+lemma lfpxs_step_dx: ∀h,G,T,L1,L,L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L → ⦃G, L⦄ ⊢ ⬈[h, T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2.
+/2 width=3 by tc_lfxs_step_dx/ qed.
+
+lemma lfpxs_step_sn: ∀h,G,T,L1,L,L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L → ⦃G, L⦄ ⊢ ⬈*[h, T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2.
+/2 width=3 by tc_lfxs_step_sn/ qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+(* Basic_2A1: uses: lpxs_inv_atom1 *)
+lemma lfpxs_inv_atom1: ∀h,I,G,L2. ⦃G, ⋆⦄ ⊢ ⬈*[h, ⓪{I}] L2 → L2 = ⋆.
+/2 width=3 by tc_lfxs_inv_atom_sn/ qed-.
+
+(* Basic_2A1: uses: lpxs_inv_atom2 *)
+lemma lfpxs_inv_atom2: ∀h,I,G,L1. ⦃G, L1⦄ ⊢ ⬈*[h, ⓪{I}] ⋆ → L1 = ⋆.
+/2 width=3 by tc_lfxs_inv_atom_dx/ qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lfpxs_fwd_pair_sn: ∀h,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ⬈*[h, ②{I}V.T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, V] L2.
+/2 width=3 by tc_lfxs_fwd_pair_sn/ qed-.
+
+lemma lfpxs_fwd_flat_dx: ∀h,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ⬈*[h, ⓕ{I}V.T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2.
+/2 width=3 by tc_lfxs_fwd_flat_dx/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_aaa.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_aaa.etc
new file mode 100644
index 000000000..43febff41
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_aaa.etc
@@ -0,0 +1,25 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/rt_transition/lfpx_aaa.ma".
+include "basic_2/rt_computation/lfpxs.ma".
+
+(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******)
+
+(* Properties with atomic arity assignment on terms *************************)
+
+(* Basic_2A1: uses: lpxs_aaa_conf *) 
+lemma lfpxs_aaa_conf: ∀h,G,T. Conf3 … (λL. aaa G L T) (lfpxs h G T).
+#h #G #T @TC_Conf3 @lfpx_aaa_conf (**) (* auto fails *)
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_cpxs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_cpxs.etc
new file mode 100644
index 000000000..a5288e11a
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_cpxs.etc
@@ -0,0 +1,76 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/rt_computation/cpxs_lfpx.ma".
+include "basic_2/rt_computation/lfpxs_fqup.ma".
+
+(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******)
+
+(* Properties with unbound context-sensitive rt-computation for terms *******)
+
+(* Basic_2A1: uses: lpxs_pair lpxs_pair_refl *)
+lemma lfpxs_pair_refl: ∀h,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈*[h] V2 →
+                       ∀I,T. ⦃G, L.ⓑ{I}V1⦄ ⊢ ⬈*[h, T] L.ⓑ{I}V2.
+/2 width=1 by tc_lfxs_pair_refl/ qed.
+
+lemma lfpxs_cpx_trans: ∀h,G. s_r_transitive … (cpx h G) (lfpxs h G).
+#h #G @s_r_trans_CTC2 @lfpx_cpxs_trans (**) (* auto fails *)
+qed-.
+
+(* Note: lfpxs_cpx_conf does not hold, thus we cannot invoke s_r_trans_CTC1 *)
+lemma lfpxs_cpxs_trans: ∀h,G. s_rs_transitive … (cpx h G) (lfpxs h G).
+#h #G @s_r_to_s_rs_trans @s_r_trans_CTC2
+@s_rs_trans_TC1 /2 width=3 by lfpx_cpxs_trans/ (**) (* full auto too slow *)
+qed-.
+
+(* Advanced properties on unbound rt-computation for terms ******************)
+
+lemma cpxs_bind2: ∀h,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈*[h] V2 →
+                  ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ⬈*[h] T2 →
+                  ∀p. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈*[h] ⓑ{p,I}V2.T2.
+/4 width=3 by lfpxs_cpxs_trans, lfpxs_pair_refl, cpxs_bind/ qed.
+
+(* Advanced inversion lemmas on unbound rt-computation for terms ************)
+
+lemma cpxs_inv_abst1: ∀h,p,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{p}V1.T1 ⬈*[h] U2 →
+                      ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ⬈*[h] V2 & ⦃G, L.ⓛV1⦄ ⊢ T1 ⬈*[h] T2 &
+                               U2 = ⓛ{p}V2.T2.
+#h #p #G #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 /2 width=5 by ex3_2_intro/
+#U0 #U2 #_ #HU02 * #V0 #T0 #HV10 #HT10 #H destruct
+elim (cpx_inv_abst1 … HU02) -HU02 #V2 #T2 #HV02 #HT02 #H destruct
+lapply (lfpxs_cpx_trans … HT02 (L.ⓛV1) ?)
+/3 width=5 by lfpxs_pair_refl, cpxs_trans, cpxs_strap1, ex3_2_intro/
+qed-.
+
+lemma cpxs_inv_abbr1: ∀h,p,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{p}V1.T1 ⬈*[h] U2 → (
+                      ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ⬈*[h] V2 & ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈*[h] T2 &
+                               U2 = ⓓ{p}V2.T2
+                      ) ∨
+                      ∃∃T2. ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈*[h] T2 & ⬆*[1] U2 ≘ T2 & p = true.
+#h #p #G #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 /3 width=5 by ex3_2_intro, or_introl/
+#U0 #U2 #_ #HU02 * *
+[ #V0 #T0 #HV10 #HT10 #H destruct
+  elim (cpx_inv_abbr1 … HU02) -HU02 *
+  [ #V2 #T2 #HV02 #HT02 #H destruct
+    lapply (lfpxs_cpx_trans … HT02 (L.ⓓV1) ?)
+    /4 width=5 by lfpxs_pair_refl, cpxs_trans, cpxs_strap1, ex3_2_intro, or_introl/
+  | #T2 #HT02 #HUT2
+    lapply (lfpxs_cpx_trans … HT02 (L.ⓓV1) ?) -HT02
+    /4 width=3 by lfpxs_pair_refl, cpxs_trans, ex3_intro, or_intror/
+  ]
+| #U1 #HTU1 #HU01
+  elim (cpx_lifts_sn … HU02 (Ⓣ) … (L.ⓓV1) … HU01)
+  /4 width=3 by cpxs_strap1, drops_refl, drops_drop, ex3_intro, or_intror/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_drops.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_drops.etc
new file mode 100644
index 000000000..caeb2bf77
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_drops.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/i_static/tc_lfxs_drops.ma".
+include "basic_2/rt_transition/lfpx_drops.ma".
+
+(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******)
+
+(* Properties with generic slicing for local environments *******************)
+
+(* Basic_2A1: uses: drop_lpxs_trans *)
+lemma drops_lfpxs_trans: ∀h,G. tc_dedropable_sn (cpx h G).
+/3 width=5 by drops_lfpx_trans, dedropable_sn_CTC/ qed-.
+
+(* Inversion lemmas with generic slicing for local environments *************)
+
+(* Basic_2A1: uses: lpxs_drop_conf *)
+lemma lfpxs_drops_conf: ∀h,G. tc_dropable_sn (cpx h G).
+/3 width=5 by lfpx_drops_conf, dropable_sn_CTC/ qed-.
+
+(* Basic_2A1: uses: lpxs_drop_trans_O1 *)
+lemma lfpxs_drops_trans: ∀h,G. tc_dropable_dx (cpx h G).
+/3 width=5 by lfpx_drops_trans, dropable_dx_CTC/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_ffdeq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_ffdeq.etc
new file mode 100644
index 000000000..35ed9931b
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_ffdeq.etc
@@ -0,0 +1,30 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/static/ffdeq.ma".
+include "basic_2/rt_computation/lfpxs_lfdeq.ma".
+
+(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******)
+
+(* Properties with degree-based equivalence on closures *********************)
+
+lemma ffdeq_lfpxs_trans: ∀h,o,G1,G2,L1,L0,T1,T2. ⦃G1, L1, T1⦄ ≛[h, o] ⦃G2, L0, T2⦄ →
+                         ∀L2. ⦃G2, L0⦄ ⊢⬈*[h, T2] L2 →
+                         ∃∃L. ⦃G1, L1⦄ ⊢⬈*[h, T1] L & ⦃G1, L, T1⦄ ≛[h, o] ⦃G2, L2, T2⦄.
+#h #o #G1 #G2 #L1 #L0 #T1 #T2 #H1 #L2 #HL02
+elim (ffdeq_inv_gen_dx … H1) -H1 #HG #HL10 #HT12 destruct
+elim (lfdeq_lfpxs_trans … HL02 … HL10) -L0 #L0 #HL10 #HL02
+lapply (tdeq_lfpxs_trans … HT12 … HL10) -HL10 #HL10
+/3 width=3 by ffdeq_intro_dx, ex2_intro/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_fqup.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_fqup.etc
new file mode 100644
index 000000000..1ca306ddb
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_fqup.etc
@@ -0,0 +1,49 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/i_static/tc_lfxs_fqup.ma".
+include "basic_2/rt_computation/lfpxs.ma".
+
+(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******)
+
+(* Advanced properties ******************************************************)
+
+lemma lfpxs_refl: ∀h,G,T. reflexive … (lfpxs h G T).
+/2 width=1 by tc_lfxs_refl/ qed.
+
+(* Advanced forward lemmas **************************************************)
+
+lemma lfpxs_fwd_bind_dx: ∀h,p,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ⬈*[h, ⓑ{p,I}V.T] L2 →
+                         ⦃G, L1.ⓑ{I}V⦄ ⊢ ⬈*[h, T] L2.ⓑ{I}V.
+/2 width=2 by tc_lfxs_fwd_bind_dx/ qed-.
+
+lemma lfpxs_fwd_bind_dx_void: ∀h,p,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ⬈*[h, ⓑ{p,I}V.T] L2 →
+                              ⦃G, L1.ⓧ⦄ ⊢ ⬈*[h, T] L2.ⓧ.
+/2 width=4 by tc_lfxs_fwd_bind_dx_void/ qed-.
+
+(* Advanced eliminators *****************************************************)
+
+(* Basic_2A1: uses: lpxs_ind *)
+lemma lfpxs_ind_sn: ∀h,G,L1,T. ∀R:predicate lenv. R L1 →
+                    (∀L,L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L → ⦃G, L⦄ ⊢ ⬈[h, T] L2 → R L → R L2) →
+                    ∀L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → R L2.
+#h #G @tc_lfxs_ind_sn // (**) (* auto fails *)
+qed-. 
+
+(* Basic_2A1: uses: lpxs_ind_dx *)
+lemma lfpxs_ind_dx: ∀h,G,L2,T. ∀R:predicate lenv. R L2 →
+                    (∀L1,L. ⦃G, L1⦄ ⊢ ⬈[h, T] L → ⦃G, L⦄ ⊢ ⬈*[h, T] L2 → R L → R L1) →
+                    ∀L1. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → R L1.
+#h #G @tc_lfxs_ind_dx // (**) (* auto fails *)
+qed-. 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_length.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_length.etc
new file mode 100644
index 000000000..27bf18d49
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_length.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/i_static/tc_lfxs_length.ma".
+include "basic_2/rt_computation/lfpxs.ma".
+
+(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******)
+
+(* Forward lemmas with length for local environments ************************)
+
+lemma lfpxs_fwd_length: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → |L1| = |L2|.
+/2 width=3 by tc_lfxs_fwd_length/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_lfdeq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_lfdeq.etc
new file mode 100644
index 000000000..2d6871c34
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_lfdeq.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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/rt_transition/lfpx_lfdeq.ma".
+include "basic_2/rt_computation/lfpxs_fqup.ma".
+
+(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******)
+
+(* Properties with degree-based equivalence on terms ************************)
+
+lemma lfpxs_tdeq_trans: ∀h,o,G. s_r_confluent1 … (cdeq h o) (lfpxs h G).
+#h #o #G #L1 #T1 #T2 #HT12 #L2 #H @(lfpxs_ind_sn … H) -L2
+/3 width=6 by lfpxs_step_dx, lfpx_tdeq_conf/
+qed-.
+
+lemma tdeq_lfpxs_trans: ∀h,o,T1,T2. T1 ≛[h, o] T2 →
+                        ∀G,L1,L2. ⦃G, L1⦄ ⊢⬈*[h, T2] L2 → ⦃G, L1⦄ ⊢⬈*[h, T1] L2.
+/3 width=4 by lfpxs_tdeq_trans, tdeq_sym/ qed-.
+
+(* Properties with degree-based equivalence on referred entries *************)
+
+(* Basic_2A1: was: lleq_lpxs_trans *)
+lemma lfdeq_lfpxs_trans: ∀h,o,G,L2,K2,T. ⦃G, L2⦄ ⊢ ⬈*[h, T] K2 →
+                         ∀L1. L1 ≛[h, o, T] L2 →
+                         ∃∃K1. ⦃G, L1⦄ ⊢ ⬈*[h, T] K1 & K1 ≛[h, o, T] K2.
+#h #o #G #L2 #K2 #T #H @(lfpxs_ind_sn … H) -K2 /2 width=3 by ex2_intro/
+#K #K2 #_ #HK2 #IH #L1 #HT elim (IH … HT) -L2
+#L #HL1 #HT elim (lfdeq_lfpx_trans … HK2 … HT) -K
+/3 width=3 by lfpxs_step_dx, ex2_intro/
+qed-.
+
+(* Basic_2A1: was: lpxs_nlleq_inv_step_sn *)
+lemma lfpxs_lfdneq_inv_step_sn: ∀h,o,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → (L1 ≛[h, o, T] L2 → ⊥) →
+                                ∃∃L,L0. ⦃G, L1⦄ ⊢ ⬈[h, T] L & L1 ≛[h, o, T] L → ⊥ & ⦃G, L⦄ ⊢ ⬈*[h, T] L0 & L0 ≛[h, o, T] L2.
+#h #o #G #L1 #L2 #T #H @(lfpxs_ind_dx … H) -L1
+[ #H elim H -H //
+| #L1 #L #H1 #H2 #IH2 #H12 elim (lfdeq_dec h o L1 L T) #H
+  [ -H1 -H2 elim IH2 -IH2 /3 width=3 by lfdeq_trans/ -H12
+    #L0 #L3 #H1 #H2 #H3 #H4 lapply (lfdeq_lfdneq_trans … H … H2) -H2
+    #H2 elim (lfdeq_lfpx_trans … H1 … H) -L
+    #L #H1 #H lapply (lfdneq_lfdeq_div … H … H2) -H2
+    #H2 elim (lfdeq_lfpxs_trans … H3 … H) -L0
+    /3 width=8 by lfdeq_trans, ex4_2_intro/
+  | -H12 -IH2 /3 width=6 by ex4_2_intro/
+  ]
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_lfpxs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_lfpxs.etc
new file mode 100644
index 000000000..9f2b0b6e1
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_lfpxs.etc
@@ -0,0 +1,24 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/i_static/tc_lfxs_tc_lfxs.ma".
+include "basic_2/rt_computation/lfpxs.ma".
+
+(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******)
+
+(* Main properties **********************************************************)
+
+(* Basic_2A1: uses: lpxs_trans *)
+theorem lfpxs_trans: ∀h,G,T. Transitive … (lfpxs h G T).
+/2 width=3 by tc_lfxs_trans/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_lpxs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_lpxs.etc
new file mode 100644
index 000000000..aa13ac53a
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_lpxs.etc
@@ -0,0 +1,36 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/i_static/tc_lfxs_lex.ma".
+include "basic_2/rt_transition/cpx_lfeq.ma".
+include "basic_2/rt_computation/cpxs_lpx.ma".
+include "basic_2/rt_computation/lpxs.ma".
+include "basic_2/rt_computation/lfpxs.ma".
+
+(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******)
+
+(* Properties with unbound parallel rt-computation for local environments ***)
+
+lemma lfpxs_lpxs: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2.
+/2 width=1 by tc_lfxs_lex/ qed.
+
+lemma lfpxs_lpxs_lfeq: ∀h,G,L1,L. ⦃G, L1⦄ ⊢ ⬈*[h] L →
+                       ∀L2,T. L ≡[T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2.
+/2 width=3 by tc_lfxs_lex_lfeq/ qed.
+
+(* Inversion lemmas with unbound parallel rt-computation for local envs *****)
+
+lemma lfpxs_inv_lpxs_lfeq: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 →
+                           ∃∃L. ⦃G, L1⦄ ⊢ ⬈*[h] L & L ≡[T] L2.
+/3 width=5 by lfpx_fsge_comp, lpx_cpxs_trans, lfeq_cpx_trans, tc_lfxs_inv_lex_lfeq/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/referred/predtysnstar_5.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/predtysnstar_5.etc
new file mode 100644
index 000000000..5bb15a4f0
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/predtysnstar_5.etc
@@ -0,0 +1,19 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ⬈ * [ break term 46 h, break term 46 T ] break term 46 L2 )"
+   non associative with precedence 45
+   for @{ 'PRedTySnStar $h $T $G $L1 $L2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_4.ma
new file mode 100644
index 000000000..a12748a9b
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_4.ma
@@ -0,0 +1,19 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡*[ break term 46 h ] break term 46 L2 )"
+   non associative with precedence 45
+   for @{ 'PRedSnStar $h $G $L1 $L2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_5.ma
deleted file mode 100644
index 095cc3e31..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_5.ma
+++ /dev/null
@@ -1,19 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡ * [ break term 46 h, break term 46 o ] break term 46 L2 )"
-   non associative with precedence 45
-   for @{ 'PRedSnStar $h $o $G $L1 $L2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysnstar_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysnstar_5.ma
deleted file mode 100644
index 5bb15a4f0..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysnstar_5.ma
+++ /dev/null
@@ -1,19 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ⬈ * [ break term 46 h, break term 46 T ] break term 46 L2 )"
-   non associative with precedence 45
-   for @{ 'PRedTySnStar $h $T $G $L1 $L2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lex_tc.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lex_tc.ma
index 9e48f4d36..a9ed87b92 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lex_tc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lex_tc.ma
@@ -23,14 +23,14 @@ alias symbol "subseteq" = "relation inclusion".
 (* Inversion lemmas with transitive closure *********************************)
 
 (* Basic_2A1: was: lpx_sn_LTC_TC_lpx_sn *)
-lemma lex_inv_CTC: ∀R. c_reflexive … R →
-                   lex (CTC … R) ⊆ TC … (lex R).
+lemma lex_inv_CTC (R): c_reflexive … R →
+                       lex (CTC … R) ⊆ TC … (lex R).
 #R #HR #L1 #L2 *
 /5 width=11 by lexs_inv_tc_dx, lexs_co, ext2_inv_tc, ext2_refl, monotonic_TC, ex2_intro/
 qed-.
 
-lemma s_rs_transitive_lex_inv_isid: ∀R. s_rs_transitive … R (λ_.lex R) →
-                                    s_rs_transitive_isid cfull (cext2 R).
+lemma s_rs_transitive_lex_inv_isid (R): s_rs_transitive … R (λ_.lex R) →
+                                        s_rs_transitive_isid cfull (cext2 R).
 #R #HR #f #Hf #L2 #T1 #T2 #H #L1 #HL12
 elim (ext2_tc … H) -H
 [ /3 width=1 by ext2_inv_tc, ext2_unit/
@@ -43,8 +43,8 @@ qed-.
 (* Properties with transitive closure ***************************************)
 
 (* Basic_2A1: was: TC_lpx_sn_inv_lpx_sn_LTC *)
-lemma lex_CTC: ∀R. s_rs_transitive … R (λ_. lex R) →
-               TC … (lex R) ⊆ lex (CTC … R).
+lemma lex_CTC (R): s_rs_transitive … R (λ_. lex R) →
+                   TC … (lex R) ⊆ lex (CTC … R).
 #R #HR #L1 #L2 #HL12
 lapply (monotonic_TC … (lexs cfull (cext2 R) 𝐈𝐝) … HL12) -HL12
 [ #L1 #L2 * /3 width=3 by lexs_eq_repl_fwd, eq_id_inv_isid/
@@ -52,12 +52,38 @@ lapply (monotonic_TC … (lexs cfull (cext2 R) 𝐈𝐝) … HL12) -HL12
 ]
 qed-.
 
-lemma lex_CTC_step_dx: ∀R. c_reflexive … R → s_rs_transitive … R (λ_. lex R) →
-                       ∀L1,L. lex (CTC … R) L1 L →
-                       ∀L2. lex R L L2 → lex (CTC … R) L1 L2.
+lemma lex_CTC_inj (R): s_rs_transitive … R (λ_. lex R) →
+                       (lex R) ⊆ lex (CTC … R).
+/3 width=1 by lex_CTC, inj/ qed-.
+
+lemma lex_CTC_step_dx (R): c_reflexive … R → s_rs_transitive … R (λ_. lex R) →
+                           ∀L1,L. lex (CTC … R) L1 L →
+                           ∀L2. lex R L L2 → lex (CTC … R) L1 L2.
 /4 width=3 by lex_CTC, lex_inv_CTC, step/ qed-.
 
-lemma lex_CTC_step_sn: ∀R. c_reflexive … R → s_rs_transitive … R (λ_. lex R) →
-                       ∀L1,L. lex R L1 L →
-                       ∀L2. lex (CTC … R) L L2 → lex (CTC … R) L1 L2.
+lemma lex_CTC_step_sn (R): c_reflexive … R → s_rs_transitive … R (λ_. lex R) →
+                           ∀L1,L. lex R L1 L →
+                           ∀L2. lex (CTC … R) L L2 → lex (CTC … R) L1 L2.
 /4 width=3 by lex_CTC, lex_inv_CTC, TC_strap/ qed-.
+
+(* Eliminators with transitive closure **************************************)
+
+lemma lex_CTC_ind_sn (R) (L2): c_reflexive … R → s_rs_transitive … R (λ_. lex R) →
+                               ∀Q:predicate lenv. Q L2 →
+                               (∀L1,L. L1 ⪤[R] L → L ⪤[CTC … R] L2 → Q L → Q L1) →
+                               ∀L1. L1 ⪤[CTC … R] L2 → Q L1.
+#R #L2 #H1R #H2R #Q #IH1 #IH2 #L1 #H
+lapply (lex_inv_CTC … H1R … H) -H #H
+@(TC_star_ind_dx ???????? H) -H
+/3 width=4 by lex_CTC, lex_refl/
+qed-.
+
+lemma lex_CTC_ind_dx (R) (L1): c_reflexive … R → s_rs_transitive … R (λ_. lex R) →
+                               ∀Q:predicate lenv. Q L1 →
+                               (∀L,L2. L1 ⪤[CTC … R] L → L ⪤[R] L2 → Q L → Q L2) →
+                               ∀L2. L1 ⪤[CTC … R] L2 → Q L2.
+#R #L1 #H1R #H2R #Q #IH1 #IH2 #L2 #H
+lapply (lex_inv_CTC … H1R … H) -H #H
+@(TC_star_ind ???????? H) -H
+/3 width=4 by lex_CTC, lex_refl/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs.ma
deleted file mode 100644
index 0e1bee1d1..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs.ma
+++ /dev/null
@@ -1,56 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/notation/relations/predtysnstar_5.ma".
-include "basic_2/i_static/tc_lfxs.ma".
-include "basic_2/rt_transition/lfpx.ma".
-
-(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******)
-
-definition lfpxs: ∀h. relation4 genv term lenv lenv ≝
-                  λh,G. tc_lfxs (cpx h G).
-
-interpretation
-   "unbound parallel rt-computation on referred entries (local environment)"
-   'PRedTySnStar h T G L1 L2 = (lfpxs h G T L1 L2).
-
-(* Basic properties *********************************************************)
-
-(* Basic_2A1: was just: lpx_lpxs *)
-lemma lfpx_lfpxs: ∀h,G,T,L1,L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2.
-/2 width=1 by inj/ qed.
-
-lemma lfpxs_step_dx: ∀h,G,T,L1,L,L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L → ⦃G, L⦄ ⊢ ⬈[h, T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2.
-/2 width=3 by tc_lfxs_step_dx/ qed.
-
-lemma lfpxs_step_sn: ∀h,G,T,L1,L,L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L → ⦃G, L⦄ ⊢ ⬈*[h, T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2.
-/2 width=3 by tc_lfxs_step_sn/ qed.
-
-(* Basic inversion lemmas ***************************************************)
-
-(* Basic_2A1: uses: lpxs_inv_atom1 *)
-lemma lfpxs_inv_atom1: ∀h,I,G,L2. ⦃G, ⋆⦄ ⊢ ⬈*[h, ⓪{I}] L2 → L2 = ⋆.
-/2 width=3 by tc_lfxs_inv_atom_sn/ qed-.
-
-(* Basic_2A1: uses: lpxs_inv_atom2 *)
-lemma lfpxs_inv_atom2: ∀h,I,G,L1. ⦃G, L1⦄ ⊢ ⬈*[h, ⓪{I}] ⋆ → L1 = ⋆.
-/2 width=3 by tc_lfxs_inv_atom_dx/ qed-.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma lfpxs_fwd_pair_sn: ∀h,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ⬈*[h, ②{I}V.T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, V] L2.
-/2 width=3 by tc_lfxs_fwd_pair_sn/ qed-.
-
-lemma lfpxs_fwd_flat_dx: ∀h,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ⬈*[h, ⓕ{I}V.T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2.
-/2 width=3 by tc_lfxs_fwd_flat_dx/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_aaa.ma
deleted file mode 100644
index 43febff41..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_aaa.ma
+++ /dev/null
@@ -1,25 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/rt_transition/lfpx_aaa.ma".
-include "basic_2/rt_computation/lfpxs.ma".
-
-(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******)
-
-(* Properties with atomic arity assignment on terms *************************)
-
-(* Basic_2A1: uses: lpxs_aaa_conf *) 
-lemma lfpxs_aaa_conf: ∀h,G,T. Conf3 … (λL. aaa G L T) (lfpxs h G T).
-#h #G #T @TC_Conf3 @lfpx_aaa_conf (**) (* auto fails *)
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_cpxs.ma
deleted file mode 100644
index a5288e11a..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_cpxs.ma
+++ /dev/null
@@ -1,76 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/rt_computation/cpxs_lfpx.ma".
-include "basic_2/rt_computation/lfpxs_fqup.ma".
-
-(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******)
-
-(* Properties with unbound context-sensitive rt-computation for terms *******)
-
-(* Basic_2A1: uses: lpxs_pair lpxs_pair_refl *)
-lemma lfpxs_pair_refl: ∀h,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈*[h] V2 →
-                       ∀I,T. ⦃G, L.ⓑ{I}V1⦄ ⊢ ⬈*[h, T] L.ⓑ{I}V2.
-/2 width=1 by tc_lfxs_pair_refl/ qed.
-
-lemma lfpxs_cpx_trans: ∀h,G. s_r_transitive … (cpx h G) (lfpxs h G).
-#h #G @s_r_trans_CTC2 @lfpx_cpxs_trans (**) (* auto fails *)
-qed-.
-
-(* Note: lfpxs_cpx_conf does not hold, thus we cannot invoke s_r_trans_CTC1 *)
-lemma lfpxs_cpxs_trans: ∀h,G. s_rs_transitive … (cpx h G) (lfpxs h G).
-#h #G @s_r_to_s_rs_trans @s_r_trans_CTC2
-@s_rs_trans_TC1 /2 width=3 by lfpx_cpxs_trans/ (**) (* full auto too slow *)
-qed-.
-
-(* Advanced properties on unbound rt-computation for terms ******************)
-
-lemma cpxs_bind2: ∀h,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈*[h] V2 →
-                  ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ⬈*[h] T2 →
-                  ∀p. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈*[h] ⓑ{p,I}V2.T2.
-/4 width=3 by lfpxs_cpxs_trans, lfpxs_pair_refl, cpxs_bind/ qed.
-
-(* Advanced inversion lemmas on unbound rt-computation for terms ************)
-
-lemma cpxs_inv_abst1: ∀h,p,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{p}V1.T1 ⬈*[h] U2 →
-                      ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ⬈*[h] V2 & ⦃G, L.ⓛV1⦄ ⊢ T1 ⬈*[h] T2 &
-                               U2 = ⓛ{p}V2.T2.
-#h #p #G #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 /2 width=5 by ex3_2_intro/
-#U0 #U2 #_ #HU02 * #V0 #T0 #HV10 #HT10 #H destruct
-elim (cpx_inv_abst1 … HU02) -HU02 #V2 #T2 #HV02 #HT02 #H destruct
-lapply (lfpxs_cpx_trans … HT02 (L.ⓛV1) ?)
-/3 width=5 by lfpxs_pair_refl, cpxs_trans, cpxs_strap1, ex3_2_intro/
-qed-.
-
-lemma cpxs_inv_abbr1: ∀h,p,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{p}V1.T1 ⬈*[h] U2 → (
-                      ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ⬈*[h] V2 & ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈*[h] T2 &
-                               U2 = ⓓ{p}V2.T2
-                      ) ∨
-                      ∃∃T2. ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈*[h] T2 & ⬆*[1] U2 ≘ T2 & p = true.
-#h #p #G #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 /3 width=5 by ex3_2_intro, or_introl/
-#U0 #U2 #_ #HU02 * *
-[ #V0 #T0 #HV10 #HT10 #H destruct
-  elim (cpx_inv_abbr1 … HU02) -HU02 *
-  [ #V2 #T2 #HV02 #HT02 #H destruct
-    lapply (lfpxs_cpx_trans … HT02 (L.ⓓV1) ?)
-    /4 width=5 by lfpxs_pair_refl, cpxs_trans, cpxs_strap1, ex3_2_intro, or_introl/
-  | #T2 #HT02 #HUT2
-    lapply (lfpxs_cpx_trans … HT02 (L.ⓓV1) ?) -HT02
-    /4 width=3 by lfpxs_pair_refl, cpxs_trans, ex3_intro, or_intror/
-  ]
-| #U1 #HTU1 #HU01
-  elim (cpx_lifts_sn … HU02 (Ⓣ) … (L.ⓓV1) … HU01)
-  /4 width=3 by cpxs_strap1, drops_refl, drops_drop, ex3_intro, or_intror/
-]
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_drops.ma
deleted file mode 100644
index caeb2bf77..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_drops.ma
+++ /dev/null
@@ -1,34 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/i_static/tc_lfxs_drops.ma".
-include "basic_2/rt_transition/lfpx_drops.ma".
-
-(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******)
-
-(* Properties with generic slicing for local environments *******************)
-
-(* Basic_2A1: uses: drop_lpxs_trans *)
-lemma drops_lfpxs_trans: ∀h,G. tc_dedropable_sn (cpx h G).
-/3 width=5 by drops_lfpx_trans, dedropable_sn_CTC/ qed-.
-
-(* Inversion lemmas with generic slicing for local environments *************)
-
-(* Basic_2A1: uses: lpxs_drop_conf *)
-lemma lfpxs_drops_conf: ∀h,G. tc_dropable_sn (cpx h G).
-/3 width=5 by lfpx_drops_conf, dropable_sn_CTC/ qed-.
-
-(* Basic_2A1: uses: lpxs_drop_trans_O1 *)
-lemma lfpxs_drops_trans: ∀h,G. tc_dropable_dx (cpx h G).
-/3 width=5 by lfpx_drops_trans, dropable_dx_CTC/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_ffdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_ffdeq.ma
deleted file mode 100644
index 35ed9931b..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_ffdeq.ma
+++ /dev/null
@@ -1,30 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/static/ffdeq.ma".
-include "basic_2/rt_computation/lfpxs_lfdeq.ma".
-
-(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******)
-
-(* Properties with degree-based equivalence on closures *********************)
-
-lemma ffdeq_lfpxs_trans: ∀h,o,G1,G2,L1,L0,T1,T2. ⦃G1, L1, T1⦄ ≛[h, o] ⦃G2, L0, T2⦄ →
-                         ∀L2. ⦃G2, L0⦄ ⊢⬈*[h, T2] L2 →
-                         ∃∃L. ⦃G1, L1⦄ ⊢⬈*[h, T1] L & ⦃G1, L, T1⦄ ≛[h, o] ⦃G2, L2, T2⦄.
-#h #o #G1 #G2 #L1 #L0 #T1 #T2 #H1 #L2 #HL02
-elim (ffdeq_inv_gen_dx … H1) -H1 #HG #HL10 #HT12 destruct
-elim (lfdeq_lfpxs_trans … HL02 … HL10) -L0 #L0 #HL10 #HL02
-lapply (tdeq_lfpxs_trans … HT12 … HL10) -HL10 #HL10
-/3 width=3 by ffdeq_intro_dx, ex2_intro/
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_fqup.ma
deleted file mode 100644
index 1ca306ddb..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_fqup.ma
+++ /dev/null
@@ -1,49 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/i_static/tc_lfxs_fqup.ma".
-include "basic_2/rt_computation/lfpxs.ma".
-
-(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******)
-
-(* Advanced properties ******************************************************)
-
-lemma lfpxs_refl: ∀h,G,T. reflexive … (lfpxs h G T).
-/2 width=1 by tc_lfxs_refl/ qed.
-
-(* Advanced forward lemmas **************************************************)
-
-lemma lfpxs_fwd_bind_dx: ∀h,p,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ⬈*[h, ⓑ{p,I}V.T] L2 →
-                         ⦃G, L1.ⓑ{I}V⦄ ⊢ ⬈*[h, T] L2.ⓑ{I}V.
-/2 width=2 by tc_lfxs_fwd_bind_dx/ qed-.
-
-lemma lfpxs_fwd_bind_dx_void: ∀h,p,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ⬈*[h, ⓑ{p,I}V.T] L2 →
-                              ⦃G, L1.ⓧ⦄ ⊢ ⬈*[h, T] L2.ⓧ.
-/2 width=4 by tc_lfxs_fwd_bind_dx_void/ qed-.
-
-(* Advanced eliminators *****************************************************)
-
-(* Basic_2A1: uses: lpxs_ind *)
-lemma lfpxs_ind_sn: ∀h,G,L1,T. ∀R:predicate lenv. R L1 →
-                    (∀L,L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L → ⦃G, L⦄ ⊢ ⬈[h, T] L2 → R L → R L2) →
-                    ∀L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → R L2.
-#h #G @tc_lfxs_ind_sn // (**) (* auto fails *)
-qed-. 
-
-(* Basic_2A1: uses: lpxs_ind_dx *)
-lemma lfpxs_ind_dx: ∀h,G,L2,T. ∀R:predicate lenv. R L2 →
-                    (∀L1,L. ⦃G, L1⦄ ⊢ ⬈[h, T] L → ⦃G, L⦄ ⊢ ⬈*[h, T] L2 → R L → R L1) →
-                    ∀L1. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → R L1.
-#h #G @tc_lfxs_ind_dx // (**) (* auto fails *)
-qed-. 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_length.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_length.ma
deleted file mode 100644
index 27bf18d49..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_length.ma
+++ /dev/null
@@ -1,23 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/i_static/tc_lfxs_length.ma".
-include "basic_2/rt_computation/lfpxs.ma".
-
-(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******)
-
-(* Forward lemmas with length for local environments ************************)
-
-lemma lfpxs_fwd_length: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → |L1| = |L2|.
-/2 width=3 by tc_lfxs_fwd_length/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfdeq.ma
deleted file mode 100644
index 2d6871c34..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfdeq.ma
+++ /dev/null
@@ -1,58 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/rt_transition/lfpx_lfdeq.ma".
-include "basic_2/rt_computation/lfpxs_fqup.ma".
-
-(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******)
-
-(* Properties with degree-based equivalence on terms ************************)
-
-lemma lfpxs_tdeq_trans: ∀h,o,G. s_r_confluent1 … (cdeq h o) (lfpxs h G).
-#h #o #G #L1 #T1 #T2 #HT12 #L2 #H @(lfpxs_ind_sn … H) -L2
-/3 width=6 by lfpxs_step_dx, lfpx_tdeq_conf/
-qed-.
-
-lemma tdeq_lfpxs_trans: ∀h,o,T1,T2. T1 ≛[h, o] T2 →
-                        ∀G,L1,L2. ⦃G, L1⦄ ⊢⬈*[h, T2] L2 → ⦃G, L1⦄ ⊢⬈*[h, T1] L2.
-/3 width=4 by lfpxs_tdeq_trans, tdeq_sym/ qed-.
-
-(* Properties with degree-based equivalence on referred entries *************)
-
-(* Basic_2A1: was: lleq_lpxs_trans *)
-lemma lfdeq_lfpxs_trans: ∀h,o,G,L2,K2,T. ⦃G, L2⦄ ⊢ ⬈*[h, T] K2 →
-                         ∀L1. L1 ≛[h, o, T] L2 →
-                         ∃∃K1. ⦃G, L1⦄ ⊢ ⬈*[h, T] K1 & K1 ≛[h, o, T] K2.
-#h #o #G #L2 #K2 #T #H @(lfpxs_ind_sn … H) -K2 /2 width=3 by ex2_intro/
-#K #K2 #_ #HK2 #IH #L1 #HT elim (IH … HT) -L2
-#L #HL1 #HT elim (lfdeq_lfpx_trans … HK2 … HT) -K
-/3 width=3 by lfpxs_step_dx, ex2_intro/
-qed-.
-
-(* Basic_2A1: was: lpxs_nlleq_inv_step_sn *)
-lemma lfpxs_lfdneq_inv_step_sn: ∀h,o,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → (L1 ≛[h, o, T] L2 → ⊥) →
-                                ∃∃L,L0. ⦃G, L1⦄ ⊢ ⬈[h, T] L & L1 ≛[h, o, T] L → ⊥ & ⦃G, L⦄ ⊢ ⬈*[h, T] L0 & L0 ≛[h, o, T] L2.
-#h #o #G #L1 #L2 #T #H @(lfpxs_ind_dx … H) -L1
-[ #H elim H -H //
-| #L1 #L #H1 #H2 #IH2 #H12 elim (lfdeq_dec h o L1 L T) #H
-  [ -H1 -H2 elim IH2 -IH2 /3 width=3 by lfdeq_trans/ -H12
-    #L0 #L3 #H1 #H2 #H3 #H4 lapply (lfdeq_lfdneq_trans … H … H2) -H2
-    #H2 elim (lfdeq_lfpx_trans … H1 … H) -L
-    #L #H1 #H lapply (lfdneq_lfdeq_div … H … H2) -H2
-    #H2 elim (lfdeq_lfpxs_trans … H3 … H) -L0
-    /3 width=8 by lfdeq_trans, ex4_2_intro/
-  | -H12 -IH2 /3 width=6 by ex4_2_intro/
-  ]
-]
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfpxs.ma
deleted file mode 100644
index 9f2b0b6e1..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfpxs.ma
+++ /dev/null
@@ -1,24 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/i_static/tc_lfxs_tc_lfxs.ma".
-include "basic_2/rt_computation/lfpxs.ma".
-
-(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******)
-
-(* Main properties **********************************************************)
-
-(* Basic_2A1: uses: lpxs_trans *)
-theorem lfpxs_trans: ∀h,G,T. Transitive … (lfpxs h G T).
-/2 width=3 by tc_lfxs_trans/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lpxs.ma
deleted file mode 100644
index aa13ac53a..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lpxs.ma
+++ /dev/null
@@ -1,36 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/i_static/tc_lfxs_lex.ma".
-include "basic_2/rt_transition/cpx_lfeq.ma".
-include "basic_2/rt_computation/cpxs_lpx.ma".
-include "basic_2/rt_computation/lpxs.ma".
-include "basic_2/rt_computation/lfpxs.ma".
-
-(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******)
-
-(* Properties with unbound parallel rt-computation for local environments ***)
-
-lemma lfpxs_lpxs: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2.
-/2 width=1 by tc_lfxs_lex/ qed.
-
-lemma lfpxs_lpxs_lfeq: ∀h,G,L1,L. ⦃G, L1⦄ ⊢ ⬈*[h] L →
-                       ∀L2,T. L ≡[T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2.
-/2 width=3 by tc_lfxs_lex_lfeq/ qed.
-
-(* Inversion lemmas with unbound parallel rt-computation for local envs *****)
-
-lemma lfpxs_inv_lpxs_lfeq: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 →
-                           ∃∃L. ⦃G, L1⦄ ⊢ ⬈*[h] L & L ≡[T] L2.
-/3 width=5 by lfpx_fsge_comp, lpx_cpxs_trans, lfeq_cpx_trans, tc_lfxs_inv_lex_lfeq/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma
index 4969c4c73..d6538eb9f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma
@@ -16,30 +16,66 @@ include "basic_2/notation/relations/predtysnstar_4.ma".
 include "basic_2/relocation/lex.ma".
 include "basic_2/rt_computation/cpxs_ext.ma".
 
-(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENVIRONMENTS *******************)
+(* UNBOUND PARALLEL RT-COMPUTATION FOR FULL LOCAL ENVIRONMENTS **************)
 
-definition lpxs: ∀h. relation3 genv lenv lenv ≝
-                 λh,G. lex (cpxs h G).
+definition lpxs (h) (G): relation lenv ≝
+                         lex (cpxs h G).
 
 interpretation
-   "unbound parallel rt-computation (local environment)"
+   "unbound parallel rt-computation on all entries (local environment)"
    'PRedTySnStar h G L1 L2 = (lpxs h G L1 L2).
 
 (* Basic properties *********************************************************)
 
-lemma lpxs_refl: ∀h,G. reflexive … (lpxs h G).
+(* Basic_2A1: uses: lpxs_pair_refl *)
+lemma lpxs_bind_refl_dx (h) (G): ∀L1,L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 →
+                                 ∀I. ⦃G, L1.ⓘ{I}⦄ ⊢ ⬈*[h] L2.ⓘ{I}.
+/2 width=1 by lex_bind_refl_dx/ qed.
+
+lemma lpxs_pair (h) (G): ∀L1,L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 →
+                         ∀V1,V2. ⦃G, L1⦄ ⊢ V1 ⬈*[h] V2 →
+                         ∀I. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ⬈*[h] L2.ⓑ{I}V2.
+/2 width=1 by lex_pair/ qed.
+
+lemma lpxs_refl (h) (G): reflexive … (lpxs h G).
 /2 width=1 by lex_refl/ qed.
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma lpxs_inv_bind_sn: ∀h,G,I1,L2,K1. ⦃G, K1.ⓘ{I1}⦄ ⊢⬈*[h] L2 →
-                        ∃∃I2,K2. ⦃G, K1⦄ ⊢⬈*[h] K2 & ⦃G, K1⦄ ⊢ I1 ⬈*[h] I2 & L2 = K2.ⓘ{I2}.
+(* Basic_2A1: was: lpxs_inv_atom1 *)
+lemma lpxs_inv_atom_sn (h) (G): ∀L2. ⦃G, ⋆⦄ ⊢ ⬈*[h] L2 → L2 = ⋆.
+/2 width=2 by lex_inv_atom_sn/ qed-.
+
+lemma lpxs_inv_bind_sn (h) (G): ∀I1,L2,K1. ⦃G, K1.ⓘ{I1}⦄ ⊢⬈*[h] L2 →
+                                ∃∃I2,K2. ⦃G, K1⦄ ⊢⬈*[h] K2 & ⦃G, K1⦄ ⊢ I1 ⬈*[h] I2 & L2 = K2.ⓘ{I2}.
 /2 width=1 by lex_inv_bind_sn/ qed-.
 
-lemma lpxs_inv_pair_sn: ∀h,G,I,L2,K1,V1. ⦃G, K1.ⓑ{I}V1⦄ ⊢⬈*[h] L2 →
-                        ∃∃K2,V2. ⦃G, K1⦄ ⊢⬈*[h] K2 & ⦃G, K1⦄ ⊢ V1 ⬈*[h] V2 & L2 = K2.ⓑ{I}V2.
-#h #G #I #L2 #K1 #V1 #H
-elim (lpxs_inv_bind_sn … H) -H #Y #K2 #HK12 #H0 #H destruct
-elim (ext2_inv_pair_sn … H0) -H0 #V2 #HV12 #H destruct
-/2 width=5 by ex3_2_intro/
-qed-.
+(* Basic_2A1: was: lpxs_inv_pair1 *)
+lemma lpxs_inv_pair_sn (h) (G): ∀I,L2,K1,V1. ⦃G, K1.ⓑ{I}V1⦄ ⊢⬈*[h] L2 →
+                                ∃∃K2,V2. ⦃G, K1⦄ ⊢⬈*[h] K2 & ⦃G, K1⦄ ⊢ V1 ⬈*[h] V2 & L2 = K2.ⓑ{I}V2.
+/2 width=1 by lex_inv_pair_sn/ qed-.
+
+(* Basic_2A1: was: lpxs_inv_atom2 *)
+lemma lpxs_inv_atom_dx (h) (G): ∀L1. ⦃G, L1⦄ ⊢ ⬈*[h] ⋆ → L1 = ⋆.
+/2 width=2 by lex_inv_atom_dx/ qed-.
+
+(* Basic_2A1: was: lpxs_inv_pair2 *)
+lemma lpxs_inv_pair_dx (h) (G): ∀I,L1,K2,V2. ⦃G, L1⦄ ⊢ ⬈*[h] K2.ⓑ{I}V2 →
+                                ∃∃K1,V1. ⦃G, K1⦄ ⊢ ⬈*[h] K2 & ⦃G, K1⦄ ⊢ V1 ⬈*[h] V2 & L1 = K1.ⓑ{I}V1.
+/2 width=1 by lex_inv_pair_dx/ qed-.
+
+(* Basic eliminators ********************************************************)
+
+(* Basic_2A1: was: lpxs_ind_alt *)
+lemma lpxs_ind (h) (G): ∀R:relation lenv.
+                        R (⋆) (⋆) → (
+                          ∀I,K1,K2.
+                          ⦃G, K1⦄ ⊢ ⬈*[h] K2 →
+                          R K1 K2 → R (K1.ⓘ{I}) (K2.ⓘ{I})
+                        ) → (
+                          ∀I,K1,K2,V1,V2.
+                          ⦃G, K1⦄ ⊢ ⬈*[h] K2 → ⦃G, K1⦄ ⊢ V1 ⬈*[h] V2 →
+                          R K1 K2 → R (K1.ⓑ{I}V1) (K2.ⓑ{I}V2)
+                        ) →
+                        ∀L1,L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → R L1 L2.
+/3 width=4 by lex_ind/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_aaa.ma
new file mode 100644
index 000000000..3ec241468
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_aaa.ma
@@ -0,0 +1,26 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/rt_transition/lpx_aaa.ma".
+include "basic_2/rt_computation/lpxs_lpx.ma".
+
+(* UNBOUND PARALLEL RT-COMPUTATION FOR FULL LOCAL ENVIRONMENTS **************)
+
+(* Properties with atomic arity assignment for terms ************************)
+
+lemma lpxs_aaa_conf (h) (G) (T): Conf3 … (λL. aaa G L T) (lpxs h G).
+#h #G #T #A #L1 #HT #L2 #H
+lapply (lex_inv_CTC … H) -H //
+@TC_Conf3 [4: // |*: /2 width=4 by lpx_aaa_conf/ ]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_cpxs.ma
index 19cc746fc..10831ed73 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_cpxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_cpxs.ma
@@ -12,15 +12,47 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/rt_computation/lfpxs_cpxs.ma".
-include "basic_2/rt_computation/lfpxs_lpxs.ma".
+include "basic_2/rt_computation/lpxs_lpx.ma".
 
-(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENVIRONMENTS *******************)
+(* UNBOUND PARALLEL RT-COMPUTATION FOR FULL LOCAL ENVIRONMENTS **************)
 
-(* Properties with unbound context-sensitive rt-computation for terms *******)
+(* Properties with context-sensitive extended rt-computation for terms ******)
 
-lemma lpxs_cpx_trans: ∀h,G. s_r_transitive … (cpx h G) (λ_.lpxs h G).
-/3 width=3 by lfpxs_cpx_trans, lfpxs_lpxs/ qed-.
+(* Basic_2A1: was: cpxs_bind2 *)
+lemma cpxs_bind_dx (h) (G): ∀L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈*[h] V2 →
+                            ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ⬈*[h] T2 →
+                            ∀p. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈*[h] ⓑ{p,I}V2.T2.
+/4 width=5 by lpxs_cpxs_trans, lpxs_pair, cpxs_bind/ qed.
 
-lemma lpxs_cpxs_trans: ∀h,G. s_rs_transitive … (cpx h G) (λ_.lpxs h G).
-/3 width=3 by lfpxs_cpxs_trans, lfpxs_lpxs/ qed-.
+(* Inversion lemmas with context-sensitive ext rt-computation for terms *****)
+
+lemma cpxs_inv_abst1 (h) (G): ∀p,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{p}V1.T1 ⬈*[h] U2 →
+                              ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ⬈*[h] V2 & ⦃G, L.ⓛV1⦄ ⊢ T1 ⬈*[h] T2 &
+                                       U2 = ⓛ{p}V2.T2.
+#h #G #p #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 /2 width=5 by ex3_2_intro/
+#U0 #U2 #_ #HU02 * #V0 #T0 #HV10 #HT10 #H destruct
+elim (cpx_inv_abst1 … HU02) -HU02 #V2 #T2 #HV02 #HT02 #H destruct
+lapply (lpxs_cpx_trans … HT02 (L.ⓛV1) ?)
+/3 width=5 by lpxs_pair, cpxs_trans, cpxs_strap1, ex3_2_intro/
+qed-.
+
+lemma cpxs_inv_abbr1 (h) (G): ∀p,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{p}V1.T1 ⬈*[h] U2 →
+                              ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ⬈*[h] V2 & ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈*[h] T2 &
+                                          U2 = ⓓ{p}V2.T2
+                               | ∃∃T2. ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈*[h] T2 & ⬆*[1] U2 ≘ T2 & p = Ⓣ.
+#h #G #p #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 /3 width=5 by ex3_2_intro, or_introl/
+#U0 #U2 #_ #HU02 * *
+[ #V0 #T0 #HV10 #HT10 #H destruct
+  elim (cpx_inv_abbr1 … HU02) -HU02 *
+  [ #V2 #T2 #HV02 #HT02 #H destruct
+    lapply (lpxs_cpx_trans … HT02 (L.ⓓV1) ?)
+    /4 width=5 by lpxs_pair, cpxs_trans, cpxs_strap1, ex3_2_intro, or_introl/
+  | #T2 #HT02 #HUT2
+    lapply (lpxs_cpx_trans … HT02 (L.ⓓV1) ?) -HT02
+    /4 width=3 by lpxs_pair, cpxs_trans, ex3_intro, or_intror/
+  ]
+| #U1 #HTU1 #HU01 #Hp
+  elim (cpx_lifts_sn … HU02 (Ⓣ) … (L.ⓓV1) … HU01) -U0 /3 width=3 by drops_refl, drops_drop/ #U #HU2 #HU1
+  /4 width=3 by cpxs_strap1, ex3_intro, or_intror/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_drops.ma
new file mode 100644
index 000000000..0482e3d19
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_drops.ma
@@ -0,0 +1,34 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/relocation/drops_lex.ma".
+include "basic_2/rt_computation/cpxs_drops.ma".
+
+(* UNBOUND PARALLEL RT-COMPUTATION FOR FULL LOCAL ENVIRONMENTS **************)
+
+(* Properties with generic slicing for local environments *******************)
+
+(* Basic_2A1: was: drop_lpxs_trans *)
+lemma drops_lpxs_trans (h) (G): dedropable_sn (cpxs h G).
+/3 width=6 by lex_liftable_dedropable_sn, cpxs_lifts_sn/ qed-.
+
+(* Inversion lemmas with generic slicing for local environments *************)
+
+(* Basic_2A1: was: lpxs_drop_conf *)
+lemma lpxs_drops_conf (h) (G): dropable_sn (cpxs h G).
+/2 width=3 by lex_dropable_sn/ qed-.
+
+(* Basic_2A1: was: lpxs_drop_trans_O1 *)
+lemma lpxs_drops_trans (h) (G): dropable_dx (cpxs h G).
+/2 width=3 by lex_dropable_dx/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_ffdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_ffdeq.ma
new file mode 100644
index 000000000..530c5e15c
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_ffdeq.ma
@@ -0,0 +1,29 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/static/ffdeq.ma".
+include "basic_2/rt_computation/lpxs_lfdeq.ma".
+
+(* UNBOUND PARALLEL RT-COMPUTATION FOR FULL LOCAL ENVIRONMENTS **************)
+
+(* Properties with degree-based equivalence on closures *********************)
+
+lemma ffdeq_lpxs_trans (h) (o): ∀G1,G2,L1,L0,T1,T2. ⦃G1, L1, T1⦄ ≛[h, o] ⦃G2, L0, T2⦄ →
+                                ∀L2. ⦃G2, L0⦄ ⊢⬈*[h] L2 →
+                                ∃∃L. ⦃G1, L1⦄ ⊢⬈*[h] L & ⦃G1, L, T1⦄ ≛[h, o] ⦃G2, L2, T2⦄.
+#h #o #G1 #G2 #L1 #L0 #T1 #T2 #H1 #L2 #HL02
+elim (ffdeq_inv_gen_dx … H1) -H1 #HG #HL10 #HT12 destruct
+elim (lfdeq_lpxs_trans … HL02 … HL10) -L0 #L0 #HL10 #HL02
+/3 width=3 by ffdeq_intro_dx, ex2_intro/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_length.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_length.ma
index 40c4dc8ef..46dbd458d 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_length.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_length.ma
@@ -15,9 +15,9 @@
 include "basic_2/relocation/lex_length.ma".
 include "basic_2/rt_computation/lpxs.ma".
 
-(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENVIRONMENTS *******************)
+(* UNBOUND PARALLEL RT-COMPUTATION FOR FULL LOCAL ENVIRONMENTS **************)
 
 (* Forward lemmas with length for local environments ************************)
 
-lemma lpxs_fwd_length: ∀h,G,L1,L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → |L1| = |L2|.
+lemma lpxs_fwd_length (h) (G): ∀L1,L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → |L1| = |L2|.
 /2 width=2 by lex_fwd_length/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lfdeq.ma
new file mode 100644
index 000000000..640c52779
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lfdeq.ma
@@ -0,0 +1,50 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/rt_transition/lpx_lfdeq.ma".
+include "basic_2/rt_computation/lpxs_lpx.ma".
+
+(* UNBOUND PARALLEL RT-COMPUTATION FOR FULL LOCAL ENVIRONMENTS **************)
+
+(* Properties with degree-based equivalence on referred entries *************)
+
+(* Basic_2A1: uses: lleq_lpxs_trans *)
+lemma lfdeq_lpxs_trans (h) (o) (G) (T:term): ∀L2,K2. ⦃G, L2⦄ ⊢ ⬈*[h] K2 →
+                                             ∀L1. L1 ≛[h, o, T] L2 →
+                                             ∃∃K1. ⦃G, L1⦄ ⊢ ⬈*[h] K1 & K1 ≛[h, o, T] K2.
+#h #o #G #T #L2 #K2 #H @(lpxs_ind_sn … H) -L2 /2 width=3 by ex2_intro/
+#L #L2 #HL2 #_ #IH #L1 #HT
+elim (lfdeq_lpx_trans … HL2 … HT) -L #L #HL1 #HT
+elim (IH … HT) -L2 #K #HLK #HT
+/3 width=3 by lpxs_step_sn, ex2_intro/
+qed-.
+
+(* Basic_2A1: uses: lpxs_nlleq_inv_step_sn *)
+lemma lpxs_lfdneq_inv_step_sn (h) (o) (G) (T:term):
+                              ∀L1,L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → (L1 ≛[h, o, T] L2 → ⊥) →
+                              ∃∃L,L0. ⦃G, L1⦄ ⊢ ⬈[h] L & L1 ≛[h, o, T] L → ⊥ &
+                                      ⦃G, L⦄ ⊢ ⬈*[h] L0 & L0 ≛[h, o, T] L2.
+#h #o #G #T #L1 #L2 #H @(lpxs_ind_sn … H) -L1
+[ #H elim H -H //
+| #L1 #L #H1 #H2 #IH2 #H12 elim (lfdeq_dec h o L1 L T) #H
+  [ -H1 -H2 elim IH2 -IH2 /3 width=3 by lfdeq_trans/ -H12
+    #L0 #L3 #H1 #H2 #H3 #H4 lapply (lfdeq_lfdneq_trans … H … H2) -H2
+    #H2 elim (lfdeq_lpx_trans … H1 … H) -L
+    #L #H1 #H lapply (lfdneq_lfdeq_div … H … H2) -H2
+    #H2 elim (lfdeq_lpxs_trans … H3 … H) -L0
+    /3 width=8 by lfdeq_trans, ex4_2_intro/
+  | -H12 -IH2 /3 width=6 by ex4_2_intro/
+  ]
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lpx.ma
index d12f1fe67..7bc58ea45 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lpx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lpx.ma
@@ -16,16 +16,56 @@ include "basic_2/relocation/lex_tc.ma".
 include "basic_2/rt_computation/lpxs.ma".
 include "basic_2/rt_computation/cpxs_lpx.ma".
 
-(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENVIRONMENTS *******************)
+(* UNBOUND PARALLEL RT-COMPUTATION FOR FULL LOCAL ENVIRONMENTS **************)
 
-(* Properties with unbound rt-transition for local environments *************)
+(* Properties with unbound rt-transition for full local environments ********)
 
-(* Basic_2A1: was: lpxs_strap1 *)
-lemma lpxs_step_dx: ∀h,G,L1,L. ⦃G, L1⦄ ⊢ ⬈*[h] L →
-                    ∀L2. ⦃G, L⦄ ⊢ ⬈[h] L2 → ⦃G, L1⦄ ⊢ ⬈*[h] L2.
-/3 width=3 by lpx_cpxs_trans, lex_CTC_step_dx/ qed-.
+lemma lpx_lpxs (h) (G): ∀L1,L2. ⦃G, L1⦄ ⊢ ⬈[h] L2 → ⦃G, L1⦄ ⊢ ⬈*[h] L2.
+/3 width=3 by lpx_cpxs_trans, lex_CTC_inj/ qed.
 
 (* Basic_2A1: was: lpxs_strap2 *)
-lemma lpxs_step_sn: ∀h,G,L1,L. ⦃G, L1⦄ ⊢ ⬈[h] L →
-                    ∀L2. ⦃G, L⦄ ⊢ ⬈*[h] L2 → ⦃G, L1⦄ ⊢ ⬈*[h] L2.
+lemma lpxs_step_sn (h) (G): ∀L1,L. ⦃G, L1⦄ ⊢ ⬈[h] L →
+                            ∀L2. ⦃G, L⦄ ⊢ ⬈*[h] L2 → ⦃G, L1⦄ ⊢ ⬈*[h] L2.
 /3 width=3 by lpx_cpxs_trans, lex_CTC_step_sn/ qed-.
+
+(* Basic_2A1: was: lpxs_strap1 *)
+lemma lpxs_step_dx (h) (G): ∀L1,L. ⦃G, L1⦄ ⊢ ⬈*[h] L →
+                            ∀L2. ⦃G, L⦄ ⊢ ⬈[h] L2 → ⦃G, L1⦄ ⊢ ⬈*[h] L2.
+/3 width=3 by lpx_cpxs_trans, lex_CTC_step_dx/ qed-.
+
+(* Eliminators with unbound rt-transition for full local environments *******)
+
+(* Basic_2A1: was: lpxs_ind_dx *)
+lemma lpxs_ind_sn (h) (G) (L2): ∀R:predicate lenv. R L2 →
+                                (∀L1,L. ⦃G, L1⦄ ⊢ ⬈[h] L → ⦃G, L⦄ ⊢ ⬈*[h] L2 → R L → R L1) →
+                                ∀L1. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → R L1.
+/3 width=7 by lpx_cpxs_trans, cpx_refl, lex_CTC_ind_sn/ qed-.
+
+(* Basic_2A1: was: lpxs_ind *)
+lemma lpxs_ind_dx (h) (G) (L1): ∀R:predicate lenv. R L1 →
+                                (∀L,L2. ⦃G, L1⦄ ⊢ ⬈*[h] L → ⦃G, L⦄ ⊢ ⬈[h] L2 → R L → R L2) →
+                                ∀L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → R L2.
+/3 width=7 by lpx_cpxs_trans, cpx_refl, lex_CTC_ind_dx/ qed-.
+
+(* Properties with context-sensitive extended rt-transition for terms *******)
+
+lemma lpxs_cpx_trans (h) (G): s_r_transitive … (cpx h G) (λ_.lpxs h G).
+#h #G #L2 #T1 #T2 #HT12 #L1 #HL12
+@(s_r_trans_CTC2 ???????? HT12) -HT12
+/2 width=4 by lpx_cpxs_trans, lex_inv_CTC/
+qed-.
+
+(* Properties with context-sensitive extended rt-computation for terms ******)
+
+(* Note: alternative proof by s_r_to_s_rs_trans *)
+lemma lpxs_cpxs_trans (h) (G): s_rs_transitive … (cpx h G) (λ_.lpxs h G).
+#h #G @s_r_trans_CTC1 /2 width=3 by lpxs_cpx_trans/
+qed-.
+
+(* Advanced properties ******************************************************)
+
+(* Basic_2A1: was: lpxs_pair2 *)
+lemma lpxs_pair_dx (h) (G): ∀L1,L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 →
+                            ∀V1,V2. ⦃G, L2⦄ ⊢ V1 ⬈*[h] V2 →
+                            ∀I. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ⬈*[h] L2.ⓑ{I}V2.
+/3 width=3 by lpxs_pair, lpxs_cpxs_trans/ qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lpxs.ma
new file mode 100644
index 000000000..f4acf7091
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lpxs.ma
@@ -0,0 +1,24 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/lex_lex.ma".
+include "basic_2/rt_computation/cpxs_cpxs.ma".
+include "basic_2/rt_computation/lpxs_lpx.ma".
+
+(* UNBOUND PARALLEL RT-COMPUTATION FOR FULL LOCAL ENVIRONMENTS **************)
+
+(* Main properties **********************************************************)
+
+theorem lpxs_trans (h) (G): Transitive … (lpxs h G).
+/4 width=5 by lpxs_cpxs_trans, cpxs_trans, lex_trans/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt
index be67912d6..05ddbc263 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt
@@ -1,7 +1,6 @@
 cpxs.ma cpxs_tdeq.ma cpxs_theq.ma cpxs_theq_vector.ma cpxs_drops.ma cpxs_fqus.ma cpxs_lsubr.ma cpxs_lfdeq.ma cpxs_ffdeq.ma cpxs_aaa.ma cpxs_lpx.ma cpxs_lfpx.ma cpxs_cnx.ma cpxs_cpxs.ma
 cpxs_ext.ma
-lpxs.ma lpxs_length.ma lpxs_lpx.ma lpxs_cpxs.ma
-lfpxs.ma lfpxs_length.ma lfpxs_drops.ma lfpxs_fqup.ma lfpxs_lfdeq.ma lfpxs_ffdeq.ma lfpxs_aaa.ma lfpxs_cpxs.ma lfpxs_lpxs.ma lfpxs_lfpxs.ma
+lpxs.ma lpxs_length.ma lpxs_drops.ma lpxs_lfdeq.ma lpxs_ffdeq.ma lpxs_aaa.ma lpxs_lpx.ma lpxs_cpxs.ma lpxs_lpxs.ma
 csx.ma csx_simple.ma csx_simple_theq.ma csx_drops.ma csx_fqus.ma csx_lsubr.ma csx_lfdeq.ma csx_ffdeq.ma csx_aaa.ma csx_gcp.ma csx_gcr.ma csx_lfpx.ma csx_cnx.ma csx_fpbq.ma csx_cpxs.ma csx_lfpxs.ma csx_csx.ma
 csx_vector.ma csx_cnx_vector.ma csx_csx_vector.ma 
 lfsx.ma lfsx_drops.ma lfsx_fqup.ma lfsx_lpx.ma lfsx_lpxs.ma lfsx_lfpxs.ma lfsx_csx.ma lfsx_lfsx.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 71ca47a56..33aa9459d 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
@@ -95,7 +95,7 @@ table {
              [ [ "strongly normalizing for term vectors" ] "csx_vector" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx_vector" + "csx_csx_vector" * ]
              [ [ "strongly normalizing for terms" ] "csx" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_fqus" + "csx_lsubr" + "csx_lfdeq" + "csx_ffdeq" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_fpbq" + "csx_cpxs" + "csx_lfpxs" + "csx_csx" * ]
              [ [ "for lenvs on referred entries" ] "lfpxs" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_drops" + "lfpxs_fqup" + "lfpxs_lfdeq" + "lfpxs_ffdeq" + "lfpxs_aaa" + "lfpxs_cpxs" + "lfpxs_lpxs" + "lfpxs_lfpxs" * ]
-             [ [ "for lenvs on all entries" ] "lpxs" + "( ⦃?,?⦄ ⊢ ⬈*[?] ? )" "lpxs_length" + "lpxs_lpx" + "lpxs_cpxs" * ]
+             [ [ "for lenvs on all entries" ] "lpxs" + "( ⦃?,?⦄ ⊢ ⬈*[?] ? )" "lpxs_length" + "lpxs_drops" + "lpxs_lfdeq" + "lpxs_ffdeq" + "lpxs_aaa" + "lpxs_lpx" + "lpxs_cpxs" + "lpxs_lpxs" * ]
              [ [ "for binders" ] "cpxs_ext" + "( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" * ]
              [ [ "for terms" ] "cpxs" + "( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_theq" + "cpxs_theq_vector" + "cpxs_drops" + "cpxs_fqus" + "cpxs_lsubr" + "cpxs_lfdeq" + "cpxs_ffdeq" + "cpxs_aaa" + "cpxs_lpx" + "cpxs_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ] 
           }