From 7d2817401273978654ca725fb3794a4a465a93bb Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 10 May 2013 16:15:53 +0000
Subject: [PATCH] - partial commit: we issue the "conversion" and "equivalence"
 components - we park conversion and equivalence on local environments for the
 moment

---
 .../lambdadelta/basic_2/conversion/cpc.ma     |   2 +-
 .../lambdadelta/basic_2/equivalence/cpcs.ma   |  29 ++---
 .../basic_2/equivalence/cpcs_cpcs.ma          | 112 +++++++++---------
 .../basic_2/equivalence/cpcs_cprs.ma          |   4 +-
 .../basic_2/equivalence/cpcs_lpss.ma          |  48 ++++++++
 .../basic_2/equivalence/cpcs_ltpr.ma          |  43 -------
 .../lambdadelta/basic_2/equivalence/lsubss.ma |   4 +-
 .../cpr/cpcs_ltpss_dx.etc}                    |   0
 .../cpr/cpcs_ltpss_sn.etc}                    |   0
 .../delift/cpcs_delift.etc}                   |   0
 .../{conversion/fpc.ma => etc/fpr/fpc.etc}    |   0
 .../fpc_fpc.ma => etc/fpr/fpc_fpc.etc}        |   0
 .../{equivalence/fpcs.ma => etc/fpr/fpcs.etc} |   0
 .../fpcs_aaa.ma => etc/fpr/fpcs_aaa.etc}      |   0
 .../fpcs_cpcs.ma => etc/fpr/fpcs_cpcs.etc}    |   0
 .../fpcs_fpcs.ma => etc/fpr/fpcs_fpcs.etc}    |   0
 .../fpcs_fprs.ma => etc/fpr/fpcs_fprs.etc}    |   2 +-
 .../{conversion/lfpc.ma => etc/lpc/lfpc.etc}  |   0
 .../lfpc_lfpc.ma => etc/lpc/lfpc_lfpc.etc}    |   0
 .../lfpcs.ma => etc/lpc/lfpcs.etc}            |   0
 .../lfpcs_aaa.ma => etc/lpc/lfpcs_aaa.etc}    |   0
 .../lfpcs_fpcs.ma => etc/lpc/lfpcs_fpcs.etc}  |   0
 .../lpc/lfpcs_lfpcs.etc}                      |   0
 .../lpc/lfpcs_lfprs.etc}                      |   0
 .../lambdadelta/basic_2/web/basic_2_src.tbl   |  12 +-
 25 files changed, 122 insertions(+), 134 deletions(-)
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_lpss.ma
 delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_ltpr.ma
 rename matita/matita/contribs/lambdadelta/basic_2/{equivalence/cpcs_ltpss_dx.ma => etc/cpr/cpcs_ltpss_dx.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{equivalence/cpcs_ltpss_sn.ma => etc/cpr/cpcs_ltpss_sn.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{equivalence/cpcs_delift.ma => etc/delift/cpcs_delift.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{conversion/fpc.ma => etc/fpr/fpc.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{conversion/fpc_fpc.ma => etc/fpr/fpc_fpc.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{equivalence/fpcs.ma => etc/fpr/fpcs.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{equivalence/fpcs_aaa.ma => etc/fpr/fpcs_aaa.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{equivalence/fpcs_cpcs.ma => etc/fpr/fpcs_cpcs.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{equivalence/fpcs_fpcs.ma => etc/fpr/fpcs_fpcs.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{equivalence/fpcs_fprs.ma => etc/fpr/fpcs_fprs.etc} (99%)
 rename matita/matita/contribs/lambdadelta/basic_2/{conversion/lfpc.ma => etc/lpc/lfpc.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{conversion/lfpc_lfpc.ma => etc/lpc/lfpc_lfpc.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{equivalence/lfpcs.ma => etc/lpc/lfpcs.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{equivalence/lfpcs_aaa.ma => etc/lpc/lfpcs_aaa.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{equivalence/lfpcs_fpcs.ma => etc/lpc/lfpcs_fpcs.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{equivalence/lfpcs_lfpcs.ma => etc/lpc/lfpcs_lfpcs.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{equivalence/lfpcs_lfprs.ma => etc/lpc/lfpcs_lfprs.etc} (100%)

diff --git a/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc.ma b/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc.ma
index 5fb614a8c..ab76bac16 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/reducibility/cpr.ma".
+include "basic_2/reduction/cpr.ma".
 
 (* CONTEXT-SENSITIVE PARALLEL CONVERSION ON TERMS ***************************)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs.ma
index 44d59982c..49f490bce 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs.ma
@@ -16,8 +16,7 @@ include "basic_2/conversion/cpc.ma".
 
 (* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************)
 
-definition cpcs: lenv → relation term ≝
-                 λL. TC … (cpc L).
+definition cpcs: lenv → relation term ≝ LTC … cpc.
 
 interpretation "context-sensitive parallel equivalence (term)"
    'PConvStar L T1 T2 = (cpcs L T1 T2).
@@ -45,29 +44,23 @@ lemma cpcs_refl: ∀L. reflexive … (cpcs L).
 
 (* Basic_1: was: pc3_s *)
 lemma cpcs_sym: ∀L. symmetric … (cpcs L).
-/3 width=1/ qed.
+#L @TC_symmetric // qed.
 
 lemma cpc_cpcs: ∀L,T1,T2. L ⊢ T1 ⬌ T2 → L ⊢ T2 ⬌* T2.
 /2 width=1/ qed.
 
 lemma cpcs_strap1: ∀L,T1,T,T2. L ⊢ T1 ⬌* T → L ⊢ T ⬌ T2 → L ⊢ T1 ⬌* T2.
-/2 width=3/ qed.
+#L @step qed.
 
 lemma cpcs_strap2: ∀L,T1,T,T2. L ⊢ T1 ⬌ T → L ⊢ T ⬌* T2 → L ⊢ T1 ⬌* T2.
-/2 width=3/ qed.
+#L @TC_strap qed.
 
 (* Basic_1: was: pc3_pr2_r *)
-lemma cpcs_cpr_dx: ∀L,T1,T2. L ⊢ T1 ➡ T2 → L ⊢ T1 ⬌* T2.
-/3 width=1/ qed.
-
-lemma cpcs_tpr_dx: ∀L,T1,T2. T1 ➡ T2 → L ⊢ T1 ⬌* T2.
+lemma cpr_cpcs_dx: ∀L,T1,T2. L ⊢ T1 ➡ T2 → L ⊢ T1 ⬌* T2.
 /3 width=1/ qed.
 
 (* Basic_1: was: pc3_pr2_x *)
-lemma cpcs_cpr_sn: ∀L,T1,T2. L ⊢ T2 ➡ T1 → L ⊢ T1 ⬌* T2.
-/3 width=1/ qed.
-
-lemma cpcs_tpr_sn: ∀L,T1,T2. T2 ➡ T1 → L ⊢ T1 ⬌* T2.
+lemma cpr_cpcs_sn: ∀L,T1,T2. L ⊢ T2 ➡ T1 → L ⊢ T1 ⬌* T2.
 /3 width=1/ qed.
 
 lemma cpcs_cpr_strap1: ∀L,T1,T. L ⊢ T1 ⬌* T → ∀T2. L ⊢ T ➡ T2 → L ⊢ T1 ⬌* T2.
@@ -87,15 +80,13 @@ lemma cpr_div: ∀L,T1,T. L ⊢ T1 ➡ T → ∀T2. L ⊢ T2 ➡ T → L ⊢ T1
 lemma cpcs_cpr_conf: ∀L,T1,T. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ⬌* T2 → L ⊢ T1 ⬌* T2.
 /3 width=3/ qed.
 
-lemma cpcs_tpss_strap1: ∀L,T1,T. L ⊢ T1 ⬌* T →
-                        ∀T2,d,e. L ⊢ T ▶* [d, e] T2 → L ⊢ T1 ⬌* T2.
-#L #T1 #T #HT1 #T2 #d #e #HT2
+lemma cpcs_cpss_strap1: ∀L,T1,T. L ⊢ T1 ⬌* T → ∀T2. L ⊢ T ▶* T2 → L ⊢ T1 ⬌* T2.
+#L #T1 #T #HT1 #T2 #HT2
 @(cpcs_cpr_strap1 … HT1) -T1 /2 width=3/
 qed-.
 
-lemma cpcs_tpss_conf: ∀L,T,T1,d,e. L ⊢ T ▶* [d, e] T1 →
-                      ∀T2. L ⊢ T ⬌* T2 → L ⊢ T1 ⬌* T2.
-#L #T #T1 #d #e #HT1 #T2 #HT2
+lemma cpcs_cpss_conf: ∀L,T,T1. L ⊢ T ▶* T1 → ∀T2. L ⊢ T ⬌* T2 → L ⊢ T1 ⬌* T2.
+#L #T #T1 #HT1 #T2 #HT2
 @(cpcs_cpr_conf … HT2) -T2 /2 width=3/
 qed-.
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma
index 5d0643879..199e49b07 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma
@@ -12,7 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/computation/cprs_lift.ma".
 include "basic_2/computation/cprs_cprs.ma".
 include "basic_2/conversion/cpc_cpc.ma".
 include "basic_2/equivalence/cpcs_cprs.ma".
@@ -46,7 +45,7 @@ lemma cpcs_inv_sort_abst: ∀a,L,W,T,k. L ⊢ ⋆k ⬌* ⓛ{a}W.T → ⊥.
 #a #L #W #T #k #H
 elim (cpcs_inv_cprs … H) -H #X #H1
 >(cprs_inv_sort1 … H1) -X #H2
-elim (cprs_inv_abst1 Abst W … H2) -H2 #W0 #T0 #_ #_ #H destruct
+elim (cprs_fwd_abst1 … H2 Abst W) -H2 #W0 #T0 #_ #_ #H destruct
 qed-.
 
 (* Basic_1: was: pc3_gen_abst *)
@@ -54,8 +53,8 @@ lemma cpcs_inv_abst: ∀a1,a2,L,W1,W2,T1,T2. L ⊢ ⓛ{a1}W1.T1 ⬌* ⓛ{a2}W2.T
                      ∧∧ L ⊢ W1 ⬌* W2 & L. ②{I}V ⊢ T1 ⬌* T2 & a1 = a2.
 #a1 #a2 #L #W1 #W2 #T1 #T2 #H #I #V
 elim (cpcs_inv_cprs … H) -H #T #H1 #H2
-elim (cprs_inv_abst1 I V … H1) -H1 #W0 #T0 #HW10 #HT10 #H destruct
-elim (cprs_inv_abst1 I V … H2) -H2 #W #T #HW2 #HT2 #H destruct /3 width=3/
+elim (cprs_fwd_abst1 … H1 I V) -H1 #W0 #T0 #HW10 #HT10 #H destruct
+elim (cprs_fwd_abst1… H2 I V) -H2 #W #T #HW2 #HT2 #H destruct /3 width=3/
 qed-.
 
 (* Basic_1: was: pc3_gen_abst_shift *)
@@ -69,7 +68,7 @@ lemma cpcs_inv_abst1: ∀a,L,W1,T1,T. L ⊢ ⓛ{a}W1.T1 ⬌* T →
                       ∃∃W2,T2. L ⊢ T ➡* ⓛ{a}W2.T2 & L ⊢ ⓛ{a}W1.T1 ➡* ⓛ{a}W2.T2.
 #a #L #W1 #T1 #T #H
 elim (cpcs_inv_cprs … H) -H #X #H1 #H2
-elim (cprs_inv_abst1 Abst W1 … H1) -H1 #W2 #T2 #HW12 #HT12 #H destruct
+elim (cprs_fwd_abst1 … H1 Abst W1) -H1 #W2 #T2 #HW12 #HT12 #H destruct
 @(ex2_2_intro … H2) -H2 /2 width=2/ (**) (* explicit constructor, /3 width=6/ is slow *)
 qed-.
 
@@ -83,18 +82,18 @@ lemma cpcs_inv_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K →
                      L ⊢ U1 ⬌* U2 → K ⊢ T1 ⬌* T2.
 #L #K #d #e #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 #HU12
 elim (cpcs_inv_cprs … HU12) -HU12 #U #HU1 #HU2
-elim (cprs_inv_lift1 … HLK … HTU1 … HU1) -U1 #T #HTU #HT1
-elim (cprs_inv_lift1 … HLK … HTU2 … HU2) -L -U2 #X #HXU
+elim (cprs_inv_lift1 … HU1 … HLK … HTU1) -U1 #T #HTU #HT1
+elim (cprs_inv_lift1 … HU2 … HLK … HTU2) -L -U2 #X #HXU
 >(lift_inj … HXU … HTU) -X -U -d -e /2 width=3/
 qed-.
 
 (* Advanced properties ******************************************************)
 
-lemma ltpr_cpcs_trans: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. L2 ⊢ T1 ⬌* T2 → L1 ⊢ T1 ⬌* T2.
+lemma lpr_cpcs_trans: ∀L1,L2. L1 ⊢ ➡ L2 → ∀T1,T2. L2 ⊢ T1 ⬌* T2 → L1 ⊢ T1 ⬌* T2.
 #L1 #L2 #HL12 #T1 #T2 #H
 elim (cpcs_inv_cprs … H) -H #T #HT1 #HT2
-lapply (ltpr_cprs_trans … HL12 … HT1) -HT1
-lapply (ltpr_cprs_trans … HL12 … HT2) -L2 /2 width=3/
+lapply (lpr_cprs_trans … HT1 … HL12) -HT1
+lapply (lpr_cprs_trans … HT2 … HL12) -L2 /2 width=3/
 qed-.
 
 lemma cpr_cprs_conf_cpcs: ∀L,T,T1,T2. L ⊢ T ➡* T1 → L ⊢ T ➡ T2 → L ⊢ T1 ⬌* T2.
@@ -112,6 +111,13 @@ lemma cprs_conf_cpcs: ∀L,T,T1,T2. L ⊢ T ➡* T1 → L ⊢ T ➡* T2 → L 
 elim (cprs_conf … HT1 … HT2) /2 width=3/
 qed-.
 
+(* Basic_1: was only: pc3_pr0_pr2_t *)
+(* Basic_1: note: pc3_pr0_pr2_t should be renamed *)
+lemma lpr_cpr_conf: ∀L1,L2. L1 ⊢ ➡ L2 → ∀T1,T2. L1 ⊢ T1 ➡ T2 → L2 ⊢ T1 ⬌* T2.
+#L1 #L2 #HL12 #T1 #T2 #HT12
+elim (lpr_cpr_conf_dx … HT12 … HL12) -L1 /3 width=3/
+qed-.
+
 (* Basic_1: was only: pc3_thin_dx *)
 lemma cpcs_flat: ∀L,V1,V2. L ⊢ V1 ⬌* V2 → ∀T1,T2. L ⊢ T1 ⬌* T2 →
                  ∀I. L ⊢ ⓕ{I}V1. T1 ⬌* ⓕ{I}V2. T2.
@@ -120,56 +126,49 @@ elim (cpcs_inv_cprs … HV12) -HV12 #V #HV1 #HV2
 elim (cpcs_inv_cprs … HT12) -HT12 /3 width=5 by cprs_flat, cprs_div/ (**) (* /3 width=5/ is too slow *)
 qed.
 
-lemma cpcs_flat_dx_tpr_rev: ∀L,V1,V2. V2 ➡ V1 → ∀T1,T2. L ⊢ T1 ⬌* T2 →
+lemma cpcs_flat_dx_cpr_rev: ∀L,V1,V2. L ⊢ V2 ➡ V1 → ∀T1,T2. L ⊢ T1 ⬌* T2 →
                             ∀I. L ⊢ ⓕ{I}V1. T1 ⬌* ⓕ{I}V2. T2.
 /3 width=1/ qed.
 
-lemma cpcs_abst: ∀L,V1,V2. L ⊢ V1 ⬌* V2 → ∀V,T1,T2. L.ⓛV ⊢ T1 ⬌* T2 →
-                 ∀a,I. L ⊢ ⓑ{a,I}V1. T1 ⬌* ⓑ{a,I}V2. T2.
+lemma cpcs_ext_bind: ∀L,V1,V2. L ⊢ V1 ⬌* V2 → ∀V,T1,T2. L.ⓛV ⊢ T1 ⬌* T2 →
+                     ∀a,I. L ⊢ ⓑ{a,I}V1.T1 ⬌* ⓑ{a,I}V2.T2.
 #L #V1 #V2 #HV12 #V #T1 #T2 #HT12 #a #I
 elim (cpcs_inv_cprs … HV12) -HV12
 elim (cpcs_inv_cprs … HT12) -HT12
-/3 width=6 by cprs_div, cprs_abst/ (**) (* /3 width=6/ is a bit slow *)
-qed.
-
-lemma cpcs_abbr_dx: ∀a,L,V,T1,T2. L.ⓓV ⊢ T1 ⬌* T2 → L ⊢ ⓓ{a}V. T1 ⬌* ⓓ{a}V. T2.
-#a #L #V #T1 #T2 #HT12
-elim (cpcs_inv_cprs … HT12) -HT12 /3 width=5 by cprs_div, cprs_abbr1/ (**) (* /3 width=5/ is a bit slow *)
+/3 width=6 by cprs_div, cprs_ext_bind/ (**) (* /3 width=6/ is a bit slow *)
 qed.
 
 lemma cpcs_bind_dx: ∀a,I,L,V,T1,T2. L.ⓑ{I}V ⊢ T1 ⬌* T2 →
                     L ⊢ ⓑ{a,I}V. T1 ⬌* ⓑ{a,I}V. T2.
-#a * /2 width=1/ /2 width=2/ qed.
-
-lemma cpcs_abbr_sn: ∀a,L,V1,V2,T. L ⊢ V1 ⬌* V2 → L ⊢ ⓓ{a}V1. T ⬌* ⓓ{a}V2. T.
-#a #L #V1 #V2 #T #HV12
-elim (cpcs_inv_cprs … HV12) -HV12 /3 width=5 by cprs_div, cprs_abbr1/ (**) (* /3 width=5/ is a bit slow *)
+#a #I #L #V #T1 #T2 #HT12
+elim (cpcs_inv_cprs … HT12) -HT12 /3 width=5 by cprs_div, cprs_bind/ (**) (* /3 width=5/ is a bit slow *)
 qed.
 
 lemma cpcs_bind_sn: ∀a,I,L,V1,V2,T. L ⊢ V1 ⬌* V2 → L ⊢ ⓑ{a,I}V1. T ⬌* ⓑ{a,I}V2. T.
-#a * /2 width=1/ /2 width=2/ qed.
+#a #I #L #V1 #V2 #T #HV12
+elim (cpcs_inv_cprs … HV12) -HV12 /3 width=5 by cprs_div, cprs_bind/ (**) (* /3 width=5/ is a bit slow *)
+qed.
 
-lemma cpcs_beta_dx: ∀a,L,V1,V2,W,T1,T2.
-                    L ⊢ V1 ➡ V2 → L.ⓛW ⊢ T1 ⬌* T2 → L ⊢ ⓐV1.ⓛ{a}W.T1 ⬌* ⓓ{a}V2.T2.
+lemma cpcs_beta_dx_cpr: ∀a,L,V1,V2,W,T1,T2.
+                        L ⊢ V1 ➡ V2 → L.ⓛW ⊢ T1 ⬌* T2 → L ⊢ ⓐV1.ⓛ{a}W.T1 ⬌* ⓓ{a}V2.T2.
 #a #L #V1 #V2 #W #T1 #T2 #HV12 #HT12
 elim (cpcs_inv_cprs … HT12) -HT12 #T #HT1 #HT2
-lapply (cprs_beta_dx … HV12 HT1 a) -HV12 -HT1 #HT1
+lapply (cprs_beta_dx a … HV12 HT1) -HV12 -HT1 #HT1
 lapply (cprs_lsubr_trans … HT2 (L.ⓓV2) ?) -HT2 /2 width=1/ #HT2
 @(cprs_div … HT1) /2 width=1/
 qed.
 
-lemma cpcs_beta_dx_tpr_rev: ∀a,L,V1,V2,W,T1,T2.
-                            V1 ➡ V2 → L.ⓛW ⊢ T2 ⬌* T1 →
+lemma cpcs_beta_dx_rev_cpr: ∀a,L,V1,V2,W,T1,T2.
+                            L ⊢ V1 ➡ V2 → L.ⓛW ⊢ T2 ⬌* T1 →
                             L ⊢ ⓓ{a}V2.T2 ⬌* ⓐV1.ⓛ{a}W.T1.
 /4 width=1/ qed.
 
-(* Note: it does not hold replacing |L1| with |L2| *)
 lemma cpcs_lsubr_trans: ∀L1,T1,T2. L1 ⊢ T1 ⬌* T2 →
-                        ∀L2. L2 ⊑ [0, |L1|] L1 → L2 ⊢ T1 ⬌* T2.
+                        ∀L2. L2 ⊑ L1 → L2 ⊢ T1 ⬌* T2.
 #L1 #T1 #T2 #HT12
 elim (cpcs_inv_cprs … HT12) -HT12
 /3 width=5 by cprs_div, cprs_lsubr_trans/ (**) (* /3 width=5/ is a bit slow *)
-qed.
+qed-.
 
 (* Basic_1: was: pc3_lift *)
 lemma cpcs_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K →
@@ -178,44 +177,47 @@ lemma cpcs_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K →
 #L #K #d #e #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 #HT12
 elim (cpcs_inv_cprs … HT12) -HT12 #T #HT1 #HT2
 elim (lift_total T d e) #U #HTU
-lapply (cprs_lift … HLK … HTU1 … HT1 … HTU) -T1 #HU1
-lapply (cprs_lift … HLK … HTU2 … HT2 … HTU) -K -T2 -T -d -e /2 width=3/
+lapply (cprs_lift … HT1 … HLK … HTU1 … HTU) -T1 #HU1
+lapply (cprs_lift … HT2 … HLK … HTU2 … HTU) -K -T2 -T -d -e /2 width=3/
 qed.
 
 lemma cpcs_strip: ∀L,T1,T. L ⊢ T ⬌* T1 → ∀T2. L ⊢ T ⬌ T2 →
                   ∃∃T0. L ⊢ T1 ⬌ T0 & L ⊢ T2 ⬌* T0.
-/3 width=3/ qed.
+#L #T1 #T @TC_strip1 /2 width=3/ qed-.
 
 (* Main properties **********************************************************)
 
 (* Basic_1: was pc3_t *)
 theorem cpcs_trans: ∀L,T1,T. L ⊢ T1 ⬌* T → ∀T2. L ⊢ T ⬌* T2 → L ⊢ T1 ⬌* T2.
-/2 width=3/ qed.
+#L #T1 #T #HT1 #T2 @(trans_TC … HT1) qed-.
 
 theorem cpcs_canc_sn: ∀L,T,T1,T2. L ⊢ T ⬌* T1 → L ⊢ T ⬌* T2 → L ⊢ T1 ⬌* T2.
-/3 width=3 by cpcs_trans, cpcs_sym/ qed. (**) (* /3 width=3/ is too slow *)
+/3 width=3 by cpcs_trans, cpcs_sym/ qed-. (**) (* /3 width=3/ is too slow *)
 
 theorem cpcs_canc_dx: ∀L,T,T1,T2. L ⊢ T1 ⬌* T → L ⊢ T2 ⬌* T → L ⊢ T1 ⬌* T2.
-/3 width=3 by cpcs_trans, cpcs_sym/ qed. (**) (* /3 width=3/ is too slow *)
+/3 width=3 by cpcs_trans, cpcs_sym/ qed-. (**) (* /3 width=3/ is too slow *)
 
-lemma cpcs_abbr1: ∀a,L,V1,V2. L ⊢ V1 ⬌* V2 → ∀T1,T2. L.ⓓV1 ⊢ T1 ⬌* T2 →
-                  L ⊢ ⓓ{a}V1. T1 ⬌* ⓓ{a}V2. T2.
-#a #L #V1 #V2 #HV12 #T1 #T2 #HT12
-@(cpcs_trans … (ⓓ{a}V1.T2)) /2 width=1/
+lemma cpcs_bind1: ∀a,I,L,V1,V2. L ⊢ V1 ⬌* V2 → ∀T1,T2. L.ⓑ{I}V1 ⊢ T1 ⬌* T2 →
+                  L ⊢ ⓑ{a,I}V1. T1 ⬌* ⓑ{a,I}V2. T2.
+#a #I #L #V1 #V2 #HV12 #T1 #T2 #HT12
+@(cpcs_trans … (ⓑ{a,I}V1.T2)) /2 width=1/
 qed.
 
-lemma cpcs_abbr2: ∀a,L,V1,V2. L ⊢ V1 ⬌* V2 → ∀T1,T2. L.ⓓV2 ⊢ T1 ⬌* T2 →
-                  L ⊢ ⓓ{a}V1. T1 ⬌* ⓓ{a}V2. T2.
-#a #L #V1 #V2 #HV12 #T1 #T2 #HT12
-@(cpcs_trans … (ⓓ{a}V2.T1)) /2 width=1/
+lemma cpcs_bind2: ∀a,I,L,V1,V2. L ⊢ V1 ⬌* V2 → ∀T1,T2. L.ⓑ{I}V2 ⊢ T1 ⬌* T2 →
+                  L ⊢ ⓑ{a,I}V1. T1 ⬌* ⓑ{a,I}V2. T2.
+#a #I #L #V1 #V2 #HV12 #T1 #T2 #HT12
+@(cpcs_trans … (ⓑ{a,I}V2.T1)) /2 width=1/
 qed.
 
-lemma cpcs_bind1: ∀I,L,V1,T1,T2. L.ⓑ{I}V1 ⊢ T1 ⬌* T2 → ∀V2. L ⊢ V1 ⬌* V2 →
-                  ∀a. L ⊢ ⓑ{a,I}V1. T1 ⬌* ⓑ{a,I}V2. T2.
-* /2 width=1/ /2 width=2/
-qed.
+(* Basic_1: was: pc3_wcpr0_t *)
+(* Basic_1: note: pc3_wcpr0_t should be renamed *)
+lemma lpr_cprs_conf: ∀L1,L2. L1 ⊢ ➡ L2 → ∀T1,T2. L1 ⊢ T1 ➡* T2 → L2 ⊢ T1 ⬌* T2.
+#L1 #L2 #HL12 #T1 #T2 #H @(cprs_ind … H) -T2 //
+/3 width=5 by cpcs_trans, lpr_cpr_conf/
+qed-.
 
-lemma cpcs_bind2: ∀L,V1,V2. L ⊢ V1 ⬌* V2 → ∀I,T1,T2. L.ⓑ{I}V2 ⊢ T1 ⬌* T2 →
-                  ∀a. L ⊢ ⓑ{a,I}V1. T1 ⬌* ⓑ{a,I}V2. T2.
-#L #V1 #V2 #HV12 * /2 width=1/ /2 width=2/
-qed.
+(* Basic_1: was: pc3_wcpr0 *)
+lemma lpr_cpcs_conf: ∀L1,L2. L1 ⊢ ➡ L2 → ∀T1,T2. L1 ⊢ T1 ⬌* T2 → L2 ⊢ T1 ⬌* T2.
+#L1 #L2 #HL12 #T1 #T2 #H
+elim (cpcs_inv_cprs … H) -H /3 width=5 by cpcs_canc_dx, lpr_cprs_conf/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cprs.ma
index cb1f5d76a..8c1fec2e1 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cprs.ma
@@ -53,7 +53,7 @@ lemma cprs_div: ∀L,T1,T. L ⊢ T1 ➡* T → ∀T2. L ⊢ T2 ➡* T → L ⊢
 qed.
 
 lemma cprs_cpr_div: ∀L,T1,T. L ⊢ T1 ➡* T → ∀T2. L ⊢ T2 ➡ T → L ⊢ T1 ⬌* T2.
-/3 width=5 by step, cprs_div/ qed-.
+/3 width=5 by cpr_cprs, cprs_div/ qed-.
 
 lemma cpr_cprs_div: ∀L,T1,T. L ⊢ T1 ➡ T → ∀T2. L ⊢ T2 ➡* T → L ⊢ T1 ⬌* T2.
-/3 width=3 by step, cprs_div/ qed-.
+/3 width=3 by cpr_cprs, cprs_div/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_lpss.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_lpss.ma
new file mode 100644
index 000000000..c9bcdc83d
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_lpss.ma
@@ -0,0 +1,48 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/substitution/lpss_lpss.ma".
+include "basic_2/computation/cprs_lpss.ma".
+include "basic_2/equivalence/cpcs_cpcs.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************)
+
+(* Properties on sn parallel substitution for local environments ************)
+
+lemma cpcs_lpss_conf: ∀L1,L2. L1 ⊢ ▶* L2 → ∀T1,T2. L1 ⊢ T1 ⬌* T2 → L2 ⊢ T1 ⬌* T2.
+#L1 #L2 #HL12 #T1 #T2 #H
+elim (cpcs_inv_cprs … H) -H #T #HT1 #HT2
+elim (cprs_lpss_conf_dx … HT1 … HL12) -HT1 #U1 #H1 #HTU1
+elim (cprs_lpss_conf_dx … HT2 … HL12) -L1 #U2 #H2 #HTU2
+elim (cpss_conf … H1 … H2) -T #U #HU1 #HU2
+lapply (cprs_cpss_trans … HTU1 … HU1) -U1
+lapply (cprs_cpss_trans … HTU2 … HU2) -U2 /2 width=3/
+qed-.
+
+lemma cpcs_lpss_cpss_conf: ∀L1,L2. L1 ⊢ ▶* L2 →
+                           ∀T,T2. L1 ⊢ T ⬌* T2 →
+                           ∀T1. L2 ⊢ T ▶* T1 →
+                           L2 ⊢ T1 ⬌* T2.
+#L1 #L2 #HL12 #T #T2 #HT2 #T1 #HT1
+lapply (cpcs_lpss_conf … HL12 … HT2) -L1 #HT2
+lapply (cpcs_cpss_conf … HT1 … HT2) -T //
+qed-.
+
+lemma cpcs_lpss_cpss2_conf: ∀L1,L2. L1 ⊢ ▶* L2 → ∀T1,T2. L1 ⊢ T1 ⬌* T2 →
+                            ∀T3. L2 ⊢ T1 ▶* T3 → ∀T4. L2 ⊢ T2 ▶* T4 →
+                            L2 ⊢ T3 ⬌* T4.
+#L1 #L2 #HL12 #T1 #T2 #HT12 #T3 #HT13 #T4 #HT24
+lapply (cpcs_lpss_cpss_conf … HL12 … HT12 … HT13) -L1 -T1 #HT32
+lapply (cpcs_cpss_strap1 … HT32 … HT24) -T2 //
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_ltpr.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_ltpr.ma
deleted file mode 100644
index 13713e51e..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_ltpr.ma
+++ /dev/null
@@ -1,43 +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/reducibility/cpr_ltpr.ma".
-include "basic_2/equivalence/cpcs_cpcs.ma".
-
-(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************)
-
-(* Properties about context-free parallel reduction on local environments ***)
-
-(* Basic_1: was only: pc3_pr0_pr2_t *)
-(* Basic_1: note: pc3_pr0_pr2_t should be renamed *)
-lemma ltpr_cpr_conf: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. L1 ⊢ T1 ➡ T2 → L2 ⊢ T1 ⬌* T2.
-#L1 #L2 #HL12 #T1 #T2 #HT12
-elim (cpr_ltpr_conf_eq … HT12 … HL12) -L1 #T #HT1 #HT2
-@(cprs_div … T) /2 width=1/ /3 width=1/ (**) (* /4 width=3/ is too long *)
-qed.
-
-(* Basic_1: was: pc3_wcpr0_t *)
-(* Basic_1: note: pc3_wcpr0_t should be renamed *)
-lemma ltpr_cprs_conf: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. L1 ⊢ T1 ➡* T2 → L2 ⊢ T1 ⬌* T2.
-#L1 #L2 #HL12 #T1 #T2 #H @(cprs_ind … H) -T2 //
-#T #T2 #_ #HT2 #IHT1
-@(cpcs_trans … IHT1) -T1 /2 width=3/
-qed.
-
-(* Basic_1: was: pc3_wcpr0 *)
-lemma ltpr_cpcs_conf: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. L1 ⊢ T1 ⬌* T2 → L2 ⊢ T1 ⬌* T2.
-#L1 #L2 #HL12 #T1 #T2 #H
-elim (cpcs_inv_cprs … H) -H #T #HT1 #HT2
-@(cpcs_canc_dx … T) /2 width=3/
-qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/lsubss.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/lsubss.ma
index 364f06ade..db3d75f52 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/lsubss.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/lsubss.ma
@@ -94,11 +94,11 @@ lemma lsubss_inv_pair2: ∀h,g,I,L1,K2,W2. h ⊢ L1 •⊑[g] K2. ⓑ{I} W2 →
 
 (* Basic_forward lemmas *****************************************************)
 
-lemma lsubss_fwd_lsubr1: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → L1 ⊑[0, |L1|] L2.
+lemma lsubss_fwd_lsubr1: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → L1 ⊑ L2.
 #h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
 qed-.
 
-lemma lsubss_fwd_lsubr2: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → L1 ⊑[0, |L2|] L2.
+lemma lsubss_fwd_lsubr2: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → L1 ⊑ L2.
 #h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
 qed-.
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_ltpss_dx.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/cpcs_ltpss_dx.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_ltpss_dx.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpr/cpcs_ltpss_dx.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_ltpss_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/cpcs_ltpss_sn.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_ltpss_sn.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpr/cpcs_ltpss_sn.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_delift.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/delift/cpcs_delift.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_delift.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/delift/cpcs_delift.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/conversion/fpc.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpc.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/conversion/fpc.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpc.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/conversion/fpc_fpc.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpc_fpc.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/conversion/fpc_fpc.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpc_fpc.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpcs.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpcs.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpcs_aaa.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_aaa.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpcs_aaa.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpcs_cpcs.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_cpcs.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpcs_cpcs.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_fpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpcs_fpcs.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_fpcs.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpcs_fpcs.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_fprs.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpcs_fprs.etc
similarity index 99%
rename from matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_fprs.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpcs_fprs.etc
index 1d3f71f9e..43239eadd 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_fprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpcs_fprs.etc
@@ -19,7 +19,7 @@ include "basic_2/equivalence/fpcs.ma".
 
 (* Properties on context-free parallel computation for closures *************)
 
-(* Note: lemma 1000 *)
+(* Note: was lemma 1000 *)
 lemma fpcs_fprs_dx: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡* ⦃L2, T2⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄.
 #L1 #L2 #T1 #T2 #H @(fprs_ind … H) -L2 -T2 /width=1/ /3 width=4/
 qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/conversion/lfpc.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpc.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/conversion/lfpc.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpc.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/conversion/lfpc_lfpc.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpc_lfpc.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/conversion/lfpc_lfpc.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpc_lfpc.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpcs.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpcs.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpcs_aaa.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs_aaa.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpcs_aaa.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs_fpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpcs_fpcs.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs_fpcs.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpcs_fpcs.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs_lfpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpcs_lfpcs.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs_lfpcs.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpcs_lfpcs.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs_lfprs.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpcs_lfprs.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs_lfprs.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpcs_lfprs.etc
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 21fd5fcca..9a4a98b86 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
@@ -51,28 +51,18 @@ table {
    ]
    class "blue"
    [ { "equivalence" * } {
-        [ { "focalized equivalence" * } {
-             [ "lfpcs ( ⦃?⦄ ⬌* ⦃?⦄ )" "lfpcs_aaa" + "lfpcs_fpcs" + "lfpcs_lfprs" + "lfpcs_lfpcs" * ]
-             [ "fpcs ( ⦃?,?⦄ ⬌* ⦃?,?⦄ )" "fpcs_aaa" + "fpcs_cpcs" + "fpcs_fprs" + "fpcs_fpcs" * ]
-          }
-        ]
         [ { "local env. ref. for stratified static type assignment" * } {
              [ "lsubss ( ? •⊑[?] ? )" "lsubss_ldrop" + "lsubss_ssta" + "lsubss_cpcs" * ]
           }
         ]
         [ { "context-sensitive equivalence" * } {
-             [ "cpcs ( ? ⊢ ? ⬌* ? )" "cpcs_ltpss_dx" + "cpcs_ltpss_sn" + "cpcs_delift" + "cpcs_aaa" + "cpcs_ltpr" + "cpcs_cprs" + "cpcs_cpcs" * ]
+             [ "cpcs ( ? ⊢ ? ⬌* ? )" "cpcs_lpss" + "cpcs_aaa" + "cpcs_cprs" + "cpcs_cpcs" * ]
           }
         ]
      }
    ]
    class "sky"
    [ { "conversion" * } {
-        [ { "focalized conversion" * } {
-             [ "lfpc ( ⦃?⦄ ⬌ ⦃?⦄ )" "lfpc_lfpc" * ]
-             [ "fpc ( ⦃?,?⦄ ⬌ ⦃?,?⦄ )" "fpc_fpc" * ]
-          }
-        ]
         [ { "context-sensitive conversion" * } {
              [ "cpc ( ? ⊢ ? ⬌ ? )" "cpc_cpc" * ]
           }
-- 
2.39.2