From 21e6d5cb0c9b6d6a6b9975b78ae752120a969cd6 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
Date: Fri, 25 Oct 2019 17:59:07 +0200
Subject: [PATCH] update in basic_2

+ cpce parked for now
+ some renaming
---
 .../lambdadelta/basic_2/dynamic/cnv_lpce.ma   |  99 ---------
 .../lambdadelta/basic_2/dynamic/lsubv.ma      |   2 +-
 .../lambdadelta/basic_2/etc/cnv_cpce.etc      |  13 ++
 .../cnv_cpce.ma => etc/cpce/cnv_cpce_1.etc}   |   0
 .../etc/cpce/{cnv_cpce.etc => cnv_cpce_2.etc} |   0
 .../basic_2/etc/cpce/cnv_lpce_1.etc           | 193 ++++++++++++++++++
 .../etc/cpce/{cnv_lpce.etc => cnv_lpce_2.etc} |   0
 .../cpce.ma => etc/cpce/cpce.etc}             |   0
 .../cpce_drops.ma => etc/cpce/cpce_drops.etc} |   0
 .../cpce_ext.ma => etc/cpce/cpce_ext.etc}     |   0
 .../lpce.ma => etc/cpce/lpce.etc}             |   0
 .../lpce_drops.ma => etc/cpce/lpce_drops.etc} |   0
 .../basic_2/etc/cpce/lsubv_cpce_1.etc         |  56 +++++
 .../basic_2/etc/cpce/lsubv_cpce_2.etc         |  59 ++++++
 .../lambdadelta/basic_2/web/basic_2_src.tbl   |   4 +-
 15 files changed, 325 insertions(+), 101 deletions(-)
 delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_lpce.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/cnv_cpce.etc
 rename matita/matita/contribs/lambdadelta/basic_2/{dynamic/cnv_cpce.ma => etc/cpce/cnv_cpce_1.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/etc/cpce/{cnv_cpce.etc => cnv_cpce_2.etc} (100%)
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cnv_lpce_1.etc
 rename matita/matita/contribs/lambdadelta/basic_2/etc/cpce/{cnv_lpce.etc => cnv_lpce_2.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{rt_conversion/cpce.ma => etc/cpce/cpce.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{rt_conversion/cpce_drops.ma => etc/cpce/cpce_drops.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{rt_conversion/cpce_ext.ma => etc/cpce/cpce_ext.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{rt_conversion/lpce.ma => etc/cpce/lpce.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{rt_conversion/lpce_drops.ma => etc/cpce/lpce_drops.etc} (100%)
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/cpce/lsubv_cpce_1.etc
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/cpce/lsubv_cpce_2.etc

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_lpce.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_lpce.ma
deleted file mode 100644
index 401b10bdb..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_lpce.ma
+++ /dev/null
@@ -1,99 +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/lpr_drops.ma".
-include "basic_2/rt_computation/cpms_lpr.ma".
-include "basic_2/rt_computation/fpbg_fqup.ma".
-include "basic_2/rt_conversion/cpce_drops.ma".
-include "basic_2/rt_conversion/lpce_drops.ma".
-include "basic_2/dynamic/cnv_drops.ma".
-
-(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
-
-definition IH (h) (a): relation3 genv lenv term ≝
-           λG,L0,T0. ⦃G,L0⦄ ⊢ T0 ![h,a] →
-           ∀n,T1. ⦃G,L0⦄ ⊢ T0 ➡[n,h] T1 → ∀T2. ⦃G,L0⦄ ⊢ T0 ⬌η[h] T2 →
-           ∀L1. ⦃G,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L0⦄ ⊢ ⬌η[h] L2 →
-           ∃∃T. ⦃G,L1⦄ ⊢ T1 ⬌η[h] T & ⦃G,L2⦄ ⊢ T2 ➡[n,h] T.
-
-(* Properties with eta-conversion for full local environments ***************)  
-
-lemma pippo_aux (h) (a) (G0) (L0) (T0):
-                (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH h a G L T) →
-                IH h a G0 L0 T0.
-#h #a #G0 #L0 * *
-[ #s #_ #_ #n #X1 #HX1 #X2 #HX2 #L1 #HL01 #L2 #HL02
-  elim (cpm_inv_sort1 … HX1) -HX1 #H #Hn destruct
-  lapply (cpce_inv_sort_sn … HX2) -HX2 #H destruct
-  /3 width=3 by cpce_sort, cpm_sort, ex2_intro/
-| #i #IH #Hi #n #X1 #HX1 #X2 #HX2 #L1 #HL01 #L2 #HL02
-  elim (cnv_inv_lref_drops … Hi) -Hi #I #K0 #W0 #HLK0 #HW0
-  elim (lpr_drops_conf … HLK0 … HL01) [| // ] #Y1 #H1 #HLK1
-  elim (lpr_inv_pair_sn … H1) -H1 #K1 #W1 #HK01 #HW01 #H destruct
-  elim (lpce_drops_conf … HLK0 … HL02) [| // ] #Y2 #H2 #HLK2
-  elim (lpce_inv_pair_sn … H2) -H2 #K2 #W2 #HK02 #HW02 #H destruct
-  elim (cpm_inv_lref1_drops … HX1) -HX1 *
-  [ #H1 #H2 destruct
-    elim (cpce_inv_lref_sn_drops_pair … HX2 … HLK0) -HX2 *
-    [ #H1 #H2 destruct -L0 -K0 -W0
-      /3 width=3 by cpce_ldef_drops, ex2_intro/
-    | #H1 #HW #H2 destruct -L0 -W2 -HW0 -HK02
-      @(ex2_intro … (#i)) [| // ]
-      @(cpce_ldec_drops … HLK1) -HLK1 #n #p #V0 #U0 #HWU0
-      /4 width=10 by lpr_cpms_trans, cpms_step_sn/
-    | #n #p #W01 #W02 #V0 #V01 #V02 #U0 #H1 #HWU0 #HW001 #HW012 #HV001 #HV012 #H2 destruct 
-    ]
-  | lapply (drops_isuni_fwd_drop2 … HLK1) [ // ] -W1 #HLK1
-    #Y0 #X0 #W1 #HLY0 #HW01 #HWX1 -HL01 -HL02
-    lapply (drops_mono … HLY0 … HLK0) -HLY0 #H destruct
-    lapply (cpce_inv_lref_sn_drops_ldef … HX2 … HLK0) -HX2 #H destruct
-    elim (IH … HW0 … HW01 … HW02 … HK01 … HK02)
-    [| /3 width=2 by fqup_fpbg, fqup_lref/ ] -L0 -K0 #W #HW1 #HW2
-    elim (lifts_total W (𝐔❴↑i❵)) #V #HWV
-    /3 width=9 by cpce_lifts_bi, cpm_delta_drops, ex2_intro/
-  | lapply (drops_isuni_fwd_drop2 … HLK1) [ // ] -W1 #HLK1
-    #m #Y0 #X0 #W1 #HLY0 #HW01 #HWX1 #H destruct -HL01 -HL02
-    lapply (drops_mono … HLY0 … HLK0) -HLY0 #H destruct
-    elim (cpce_inv_lref_sn_drops_ldec … HX2 … HLK0) -HX2 *
-    [ #_ #H destruct
-      elim (IH … HW0 … HW01 … HW02 … HK01 … HK02)
-      [| /3 width=2 by fqup_fpbg, fqup_lref/ ] -L0 -K0 #W #HW1 #HW2
-      elim (lifts_total W (𝐔❴↑i❵)) #V #HWV
-      /3 width=9 by cpce_lifts_bi, cpm_ell_drops, ex2_intro/
-    | lapply (drops_isuni_fwd_drop2 … HLK2) [ // ] -W2 #HLK2
-      #n #p #W01 #W02 #V0 #V01 #V02 #U0 #_ #HW001 #HW012 #_ #_ #H destruct -V0 -V01 -U0
-      elim (IH … HW0 … HW01 … HW001 … HK01 … HK02)
-      [| /3 width=2 by fqup_fpbg, fqup_lref/ ] -L0 -K0 #W #HW1 #HW2
-      elim (lifts_total W (𝐔❴↑i❵)) #V #HWV
-      /4 width=11 by cpce_lifts_bi, cpm_lifts_bi, cpm_ee, ex2_intro/
-    ]
-  ]
-| #l #_ #_ #n #X1 #HX1 #X2 #HX2 #L1 #HL01 #L2 #HL02
-  elim (cpm_inv_gref1 … HX1) -HX1 #H1 #H2 destruct
-  lapply (cpce_inv_gref_sn … HX2) -HX2 #H destruct
-  /3 width=3 by cpce_gref, cpr_refl, ex2_intro/
-
-(*
-lemma cpce_inv_eta_drops (h) (n) (G) (L) (i):
-      ∀X. ⦃G,L⦄ ⊢ #i ⬌η[h] X →
-      ∀K,W. ⇩*[i] L ≘ K.ⓛW →
-      ∀p,V1,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V1.U →
-      ∀V2. ⦃G,K⦄ ⊢ V1 ⬌η[h] V2 →
-      ∀W2. ⇧*[↑i] V2 ≘ W2 → X = +ⓛW2.ⓐ#0.#↑i.
-
-theorem cpce_mono_cnv (h) (a) (G) (L):
-        ∀T. ⦃G,L⦄ ⊢ T ![h,a] →
-        ∀T1. ⦃G,L⦄ ⊢ T ⬌η[h] T1 → ∀T2. ⦃G,L⦄ ⊢ T ⬌η[h] T2 → T1 = T2.
-#h #a #G #L #T #HT
-*)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv.ma
index 2ff320b82..6df83d988 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv.ma
@@ -74,7 +74,7 @@ fact lsubv_inv_atom_dx_aux (h) (a) (G):
 qed-.
 
 (* Basic_2A1: uses: lsubsv_inv_atom2 *)
-lemma lsubv_inv_atom2 (h) (a) (G):
+lemma lsubv_inv_atom_dx (h) (a) (G):
       ∀L1. G ⊢ L1 ⫃![h,a] ⋆ → L1 = ⋆.
 /2 width=6 by lsubv_inv_atom_dx_aux/ qed-.
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cnv_cpce.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cnv_cpce.etc
new file mode 100644
index 000000000..c8e1d66ab
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cnv_cpce.etc
@@ -0,0 +1,13 @@
+(*
+lemma cpce_inv_eta_drops (h) (n) (G) (L) (i):
+      ∀X. ⦃G,L⦄ ⊢ #i ⬌η[h] X →
+      ∀K,W. ⇩*[i] L ≘ K.ⓛW →
+      ∀p,V1,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V1.U →
+      ∀V2. ⦃G,K⦄ ⊢ V1 ⬌η[h] V2 →
+      ∀W2. ⇧*[↑i] V2 ≘ W2 → X = +ⓛW2.ⓐ#0.#↑i.
+
+theorem cpce_mono_cnv (h) (a) (G) (L):
+        ∀T. ⦃G,L⦄ ⊢ T ![h,a] →
+        ∀T1. ⦃G,L⦄ ⊢ T ⬌η[h] T1 → ∀T2. ⦃G,L⦄ ⊢ T ⬌η[h] T2 → T1 = T2.
+#h #a #G #L #T #HT
+*)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpce.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cnv_cpce_1.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpce.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cnv_cpce_1.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cnv_cpce.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cnv_cpce_2.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cnv_cpce.etc
rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cnv_cpce_2.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cnv_lpce_1.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cnv_lpce_1.etc
new file mode 100644
index 000000000..807b9fdc7
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cnv_lpce_1.etc
@@ -0,0 +1,193 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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_conversion/cpce_drops.ma".
+include "basic_2/rt_conversion/lpce_drops.ma".
+include "basic_2/dynamic/cnv_preserve.ma".
+
+(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
+
+definition IH_cnv_cpce_cpm_conf (h) (a): relation3 genv lenv term ≝
+           λG,L0,T0. ⦃G,L0⦄ ⊢ T0 ![h,a] →
+           ∀n,T1. ⦃G,L0⦄ ⊢ T0 ➡[n,h] T1 → ∀T2. ⦃G,L0⦄ ⊢ T0 ⬌η[h] T2 →
+           ∀L1. ⦃G,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L0⦄ ⊢ ⬌η[h] L2 →
+           ∃∃T. ⦃G,L1⦄ ⊢ T1 ⬌η[h] T & ⦃G,L2⦄ ⊢ T2 ➡*[n,h] T.
+
+definition IH_cnv_cpce_cpms_conf (h) (a): relation3 genv lenv term ≝
+           λG,L0,T0. ⦃G,L0⦄ ⊢ T0 ![h,a] →
+           ∀n,T1. ⦃G,L0⦄ ⊢ T0 ➡*[n,h] T1 → ∀T2. ⦃G,L0⦄ ⊢ T0 ⬌η[h] T2 →
+           ∀L1. ⦃G,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L0⦄ ⊢ ⬌η[h] L2 →
+           ∃∃T. ⦃G,L1⦄ ⊢ T1 ⬌η[h] T & ⦃G,L2⦄ ⊢ T2 ➡*[n,h] T.
+
+(* Properties with eta-conversion for full local environments ***************)
+
+fact cnv_cpce_cpms_conf_sub (h) (a) (G0) (L0) (T0):
+     (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpce_cpm_conf h a G L T) →
+     ∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpce_cpms_conf h a G L T.
+#h #a #GX #LX #TX #HX #G #L0 #T0 #HX0 #HT0 #n #X1 #HX1
+@(cpms_ind_dx … HX1) -n -X1
+[ #T2 #HT02 #L1 #HL01 #L2 #HL02
+  /2 width=8 by/
+| #n1 #n2 #T3 #T1 #HT03 #IH #HT31 #T2 #HT02 #L1 #HL01 #L2 #HL02
+  lapply (cnv_cpms_trans … HT0 … HT03) -HT0 #HT3
+  elim (IH … HT02 … L0 … HL02) -IH -HT02 [| // ] #T4 #HT34 #HT24
+  elim (HX … HT3 … HT31 … HT34 … HL01 … HL02)
+  [| /2 width=4 by fpbg_cpms_trans/ ] -GX -LX -L0 -TX -T0 -T3 #T3 #HT13 #HT43
+  /3 width=5 by cpms_trans, ex2_intro/
+]
+qed-.
+
+fact cnv_cpce_cpm_conf_aux (h) (a) (G0) (L0) (T0):
+     (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpce_cpm_conf h a G L T) →
+     IH_cnv_cpce_cpm_conf h a G0 L0 T0.
+#h #a #G0 #L0 * * [|||| * ]
+[ #s #_ #_ #n #X1 #HX1 #X2 #HX2 #L1 #HL01 #L2 #HL02
+  elim (cpm_inv_sort1 … HX1) -HX1 #H #Hn destruct
+  lapply (cpce_inv_sort_sn … HX2) -HX2 #H destruct
+  /3 width=3 by cpce_sort, ex2_intro/
+| #i #IH #H0 #n #X1 #HX1 #X2 #HX2 #L1 #HL01 #L2 #HL02
+  elim (cnv_inv_lref_drops … H0) -H0 #I #K0 #W0 #HLK0 #HW0
+  elim (lpr_drops_conf … HLK0 … HL01) [| // ] #Y1 #H1 #HLK1
+  elim (lpr_inv_pair_sn … H1) -H1 #K1 #W1 #HK01 #HW01 #H destruct
+  elim (lpce_drops_conf … HLK0 … HL02) [| // ] #Y2 #H2 #HLK2
+  elim (lpce_inv_pair_sn … H2) -H2 #K2 #W2 #HK02 #HW02 #H destruct
+  elim (cpm_inv_lref1_drops … HX1) -HX1 *
+  [ #H1 #H2 destruct
+    elim (cpce_inv_lref_sn_drops_pair … HX2 … HLK0) -HX2 *
+    [ #H1 #H2 destruct -L0 -K0 -W0
+      /3 width=3 by cpce_ldef_drops, ex2_intro/
+    | #H1 #HW #H2 destruct -L0 -W2 -HW0 -HK02
+      @(ex2_intro … (#i)) [| // ]
+      @(cpce_ldec_drops … HLK1) -HLK1 #n #p #V0 #U0 #HWU0
+      /4 width=10 by lpr_cpms_trans, cpms_step_sn/
+    | lapply (drops_isuni_fwd_drop2 … HLK2) [ // ] -W2 #HLK2
+      #n #p #W01 #W02 #V0 #V01 #V02 #U0 #H1 #HWU0 #HW001 #HW012 #HV001 #HV012 #H2 destruct
+      lapply (cnv_cpms_trans … HW0 … HWU0) #H
+      elim (cnv_inv_bind … H) -H #HV0 #_
+      elim (cnv_cpms_conf_lpr … HW0 … HWU0 0 W1 … K0 … HK01) [| // ]
+      [| /2 width=1 by cpm_cpms/ ] <minus_O_n <minus_n_O #X #H #HWU1
+      elim (cpms_inv_abst_sn … H) -H #V1 #U1 #HV01 #HU01 #H destruct
+      elim (IH … HW0 … HW01 … HW001 … HK01 … HK02) -HW01 -HW001
+      [| /3 width=2 by fqup_fpbg, fqup_lref/ ] #W11 #HW11 #HW011
+      elim (cnv_cpce_cpms_conf_sub … IH … HV0 … HV01 … HV001 … HK01 … HK02) -HV0 -HV01 -HV001
+      [| /4 width=6 by fqup_cpms_fwd_fpbg, fpbg_fqu_trans, fqup_lref/ ] #V11 #HV11 #HV011
+      elim (cpms_lifts_sn … HW011 … HLK2 … HW012) -W01 #W12 #HW112 #HW012
+      elim (cpms_lifts_sn … HV011 … HLK2 … HV012) -V01 #V12 #HV112 #HV012
+      @(ex2_intro …(ⓝW12.+ⓛV12.ⓐ#O.#(↑i)))
+      [ /2 width=14 by cpce_eta_drops/ | /3 width=1 by cpms_cast, cpms_bind/ ]
+    ]
+  | lapply (drops_isuni_fwd_drop2 … HLK1) [ // ] -W1 #HLK1
+    #Y0 #X0 #W1 #HLY0 #HW01 #HWX1 -HL01 -HL02
+    lapply (drops_mono … HLY0 … HLK0) -HLY0 #H destruct
+    lapply (cpce_inv_lref_sn_drops_ldef … HX2 … HLK0) -HX2 #H destruct
+    elim (IH … HW0 … HW01 … HW02 … HK01 … HK02)
+    [| /3 width=2 by fqup_fpbg, fqup_lref/ ] -L0 -K0 #W #HW1 #HW2
+    elim (lifts_total W (𝐔❴↑i❵)) #V #HWV
+    /3 width=9 by cpce_lifts_bi, cpms_delta_drops, ex2_intro/
+  | lapply (drops_isuni_fwd_drop2 … HLK1) [ // ] -W1 #HLK1
+    #m #Y0 #X0 #W1 #HLY0 #HW01 #HWX1 #H destruct -HL01 -HL02
+    lapply (drops_mono … HLY0 … HLK0) -HLY0 #H destruct
+    elim (cpce_inv_lref_sn_drops_ldec … HX2 … HLK0) -HX2 *
+    [ #_ #H destruct
+      elim (IH … HW0 … HW01 … HW02 … HK01 … HK02)
+      [| /3 width=2 by fqup_fpbg, fqup_lref/ ] -L0 -K0 #W #HW1 #HW2
+      elim (lifts_total W (𝐔❴↑i❵)) #V #HWV
+      /3 width=9 by cpce_lifts_bi, cpms_ell_drops, ex2_intro/
+    | lapply (drops_isuni_fwd_drop2 … HLK2) [ // ] -W2 #HLK2
+      #n #p #W01 #W02 #V0 #V01 #V02 #U0 #_ #HW001 #HW012 #_ #_ #H destruct -V0 -V01 -U0
+      elim (IH … HW0 … HW01 … HW001 … HK01 … HK02)
+      [| /3 width=2 by fqup_fpbg, fqup_lref/ ] -L0 -K0 #W #HW1 #HW2
+      elim (lifts_total W (𝐔❴↑i❵)) #V #HWV
+      /4 width=11 by cpce_lifts_bi, cpms_lifts_bi, cpms_ee, ex2_intro/
+    ]
+  ]
+| #l #_ #_ #n #X1 #HX1 #X2 #HX2 #L1 #HL01 #L2 #HL02
+  elim (cpm_inv_gref1 … HX1) -HX1 #H1 #H2 destruct
+  lapply (cpce_inv_gref_sn … HX2) -HX2 #H destruct
+  /3 width=3 by cpce_gref, cpm_cpms, ex2_intro/
+| #p #I #V0 #T0 #IH #H0 #n #X1 #HX1 #X2 #HX2 #L1 #HL01 #L2 #HL02
+  elim (cnv_inv_bind … H0) -H0 #HV0 #HT0
+  elim (cpce_inv_bind_sn … HX2) -HX2 #V2 #T2 #HV02 #HT02 #H destruct
+  elim (cpm_inv_bind1 … HX1) -HX1 *
+  [ #V1 #T1 #HV01 #HT01 #H destruct
+    elim (IH … HV0 … HV01 … HV02 … HL01 … HL02) -HV0
+    [| /2 width=1 by fqup_fpbg/ ] #V #HV1 #HV2
+    elim (IH … HT0 … HT01 … HT02 … (L1.ⓑ{I}V1) … (L2.ⓑ{I}V2)) -HT0 -HT01 -HT02
+    [|*: /2 width=1 by lpce_pair, fqup_fpbg, lpr_pair/ ] -L0 -V0 -T0 #T #HT1 #HT2
+    /3 width=5 by cpce_bind, cpms_bind, ex2_intro/
+  | #X0 #HXT0 #HX01 #H1 #H2 destruct -HV0 -HV02
+    lapply (cnv_inv_lifts … HT0 (Ⓣ) … L0 … HXT0) -HT0
+    [ /3 width=1 by drops_refl, drops_drop/ ] #HX0
+    elim (cpce_inv_lifts_sn … HT02 (Ⓣ) … L0 … HXT0) -HT02
+    [| /3 width=1 by drops_refl, drops_drop/ ] #X2 #HXT2 #HX02
+    elim (IH … HX0 … HX01 … HX02 … HL01 … HL02) -HX0 -HX01 -HX02
+    [| /3 width=1 by fqup_fpbg, fqup_zeta/ ] -V0 -T0 -X0 #X #HX1 #HX2
+    /3 width=5 by cpms_zeta, ex2_intro/
+  ]
+| #V0 #T0 #IH #H0 #n #X1 #HX1 #X2 #HX2 #L1 #HL01 #L2 #HL02
+  elim (cnv_inv_appl … H0) -H0 #m #p #W0 #U0 #_ #HV0 #HT0 #_ #_ -m -p -W0 -U0
+  elim (cpce_inv_flat_sn … HX2) -HX2 #V2 #T2 #HV02 #HT02 #H destruct
+  elim (cpm_inv_appl1 … HX1) -HX1 *
+  [ #V1 #T1 #HV01 #HT01 #H destruct
+    elim (IH … HV0 … HV01 … HV02 … HL01 … HL02) -HV0 -HV01 -HV02
+    [| /2 width=1 by fqup_fpbg/ ] #V #HV1 #HV2
+    elim (IH … HT0 … HT01 … HT02 … HL01 … HL02) -HT0 -HT01 -HT02
+    [|*: /2 width=1 by fqup_fpbg/ ] -L0 -V0 -T0 #T #HT1 #HT2
+    /3 width=5 by cpce_flat, cpms_appl, ex2_intro/
+  | #p #V1 #W0 #W1 #X0 #T1 #HV01 #HW01 #HT01 #H1 #H2 destruct
+    elim (cnv_inv_bind … HT0) -HT0 #HW0 #HT0
+    elim (cpce_inv_bind_sn … HT02) -HT02 #W2 #X2 #HW02 #HT02 #H destruct
+    elim (IH … HV0 … HV01 … HV02 … HL01 … HL02) -HV0 -HV01 -HV02
+    [| /2 width=1 by fqup_fpbg/ ] #V #HV1 #HV2
+    elim (IH … HW0 … HW01 … HW02 … HL01 … HL02) -HW0
+    [| /2 width=1 by fqup_fpbg/ ] #W #HW1 #HW2
+    elim (IH … HT0 … HT01 … HT02 … (L1.ⓛW1) … (L2.ⓛW2)) -HT0 -HT01 -HT02
+    [|*: /2 width=1 by lpce_pair, fqup_fpbg, lpr_pair/ ] -L0 -V0 -X0 #T #HT1 #HT2
+    @(ex2_intro … (ⓓ{p}ⓝW.V.T))
+    [ @cpce_bind [ /2 width=1 by cpce_flat/ ]
+    | @(cpms_beta) //
+    ]
+  | #p #V1 #U1 #W0 #W1 #X0 #T1 #HV01 #HVU1 #HW01 #HT01 #H1 #H2 destruct
+    elim (cnv_inv_bind … HT0) -HT0 #HW0 #HT0
+    elim (cpce_inv_bind_sn … HT02) -HT02 #W2 #X2 #HW02 #HT02 #H destruct
+    elim (IH … HV0 … HV01 … HV02 … HL01 … HL02) -HV0 -HV01 -HV02
+    [| /2 width=1 by fqup_fpbg/ ] #V #HV1 #HV2
+    elim (IH … HW0 … HW01 … HW02 … HL01 … HL02) -HW0
+    [| /2 width=1 by fqup_fpbg/ ] #W #HW1 #HW2
+    elim (IH … HT0 … HT01 … HT02 … (L1.ⓓW1) … (L2.ⓓW2)) -HT0 -HT01 -HT02
+    [|*: /2 width=1 by lpce_pair, fqup_fpbg, lpr_pair/ ] -L0 -V0 -X0 #T #HT1 #HT2
+    elim (cpce_lifts_sn … HV1 (Ⓣ) … (L1.ⓓW1) … HVU1) -V1
+    [| /3 width=1 by drops_refl, drops_drop/ ] #U #HVU #HU1
+    /4 width=9 by cpms_theta, cpce_bind, cpce_flat, ex2_intro/
+  ]
+| #V0 #T0 #IH #H0 #n #X1 #HX1 #X2 #HX2 #L1 #HL01 #L2 #HL02
+  elim (cnv_inv_cast … H0) -H0 #U0 #HV0 #HT0 #_ #_ -U0
+  elim (cpce_inv_flat_sn … HX2) -HX2 #V2 #T2 #HV02 #HT02 #H destruct
+  elim (cpm_inv_cast1 … HX1) -HX1 [ * || * ]
+  [ #V1 #T1 #HV01 #HT01 #H destruct
+    elim (IH … HV0 … HV01 … HV02 … HL01 … HL02) -HV0 -HV01 -HV02
+    [| /2 width=1 by fqup_fpbg/ ] #V #HV1 #HV2
+    elim (IH … HT0 … HT01 … HT02 … HL01 … HL02) -HT0 -HT01 -HT02
+    [|*: /2 width=1 by fqup_fpbg/ ] -L0 -V0 -T0 #T #HT1 #HT2
+    /3 width=5 by cpce_flat, cpms_cast, ex2_intro/
+  | #HT01 -HV0 -HV02
+    elim (IH … HT0 … HT01 … HT02 … HL01 … HL02) -HT0 -HT01 -HT02
+    [|*: /2 width=1 by fqup_fpbg/ ] -L0 -V0 -T0 #T #HT1 #HT2
+    /3 width=3 by cpms_eps, ex2_intro/
+  | #m #HV01 #H destruct -HT0 -HT02
+    elim (IH … HV0 … HV01 … HV02 … HL01 … HL02) -HV0 -HV01 -HV02
+    [| /2 width=1 by fqup_fpbg/ ] -L0 -V0 -T0 #V #HV1 #HV2
+    /3 width=3 by cpms_ee, ex2_intro/
+  ]
+]
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cnv_lpce.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cnv_lpce_2.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cnv_lpce.etc
rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cnv_lpce_2.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cpce.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cpce.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cpce_drops.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce_drops.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cpce_drops.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce_ext.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cpce_ext.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce_ext.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cpce_ext.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/lpce.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/lpce.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/rt_conversion/lpce.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpce/lpce.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/lpce_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/lpce_drops.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/rt_conversion/lpce_drops.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpce/lpce_drops.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/lsubv_cpce_1.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/lsubv_cpce_1.etc
new file mode 100644
index 000000000..4c8e38a03
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/lsubv_cpce_1.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/rt_conversion/cpce.ma".
+include "basic_2/rt_equivalence/cpcs.ma".
+include "basic_2/dynamic/lsubv.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE VALIDITY *************************)
+
+lemma lsubv_inv_unit_dx (h) (a) (G):
+      ∀I,L1,K2. G ⊢ L1 ⫃![h,a] K2.ⓤ{I} →
+      ∃∃K1. G ⊢ K1 ⫃![h,a] K2 & L1 = K1.ⓤ{I}.
+#h #a #G #I #L1 #K2 #H
+elim (lsubv_inv_bind_dx … H) -H // *
+#K1 #XW #XV #_ #_ #H1 #H2 destruct
+qed-.
+
+lemma lsubv_inv_abbr_dx (h) (a) (G):
+      ∀L1,K2,V. G ⊢ L1 ⫃![h,a] K2.ⓓV →
+      ∃∃K1. G ⊢ K1 ⫃![h,a] K2 & L1 = K1.ⓓV.
+#h #a #G #L1 #K2 #V #H
+elim (lsubv_inv_bind_dx … H) -H // *
+#K1 #XW #XV #_ #_ #H1 #H2 destruct
+qed-.
+
+lemma lsubv_cpce_trans_cpcs (h) (a) (G) (T0):
+      ∀L2,T2. ⦃G,L2⦄ ⊢ T0 ⬌η[h] T2 → ∀L1. G ⊢ L1 ⫃![h,a] L2 →
+      ∃∃T1. ⦃G,L1⦄ ⊢ T0 ⬌η[h] T1 & ⦃G,L1⦄ ⊢ T1 ⬌*[h] T2.
+#h #a #G #T0 #L2 #T2 #H elim H -G -L2 -T0 -T2
+[ #G #L2 #s #L1 #HL12
+  /2 width=3 by cpce_sort, ex2_intro/
+| #G #i #Y1 #HY1
+  lapply (lsubv_inv_atom2 … HY1) -HY1 #H destruct
+   /2 width=3 by cpce_atom, ex2_intro/
+| #I #G #K2 #Y1 #HY1
+  elim (lsubv_inv_unit_dx … HY1) -HY1 #K2 #_ #H destruct
+  /2 width=3 by cpce_unit, ex2_intro/
+| #G #K2 #V2 #Y1 #HY1
+  elim (lsubv_inv_abbr_dx … HY1) -HY1 #K2 #_ #H destruct
+  /2 width=3 by cpce_ldef, ex2_intro/
+| #G #K2 #W2 #HW2 #Y1 #HY1
+  elim (lsubv_inv_bind_dx … HY1) -HY1 *
+  [ #K1 #HK12 #H destruct
+    @(ex2_intro … (#0)) [| // ]
+    @cpce_ldec #n #p #V2 #U2 #HWU2
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/lsubv_cpce_2.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/lsubv_cpce_2.etc
new file mode 100644
index 000000000..4b5ac0061
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/lsubv_cpce_2.etc
@@ -0,0 +1,59 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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_equivalence/cpes.ma". *)
+include "basic_2/dynamic/cnv_cpmuwe.ma".
+(* include "basic_2/dynamic/lsubv.ma". *)
+
+(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-EQUIVALENCE FOR TERMS **************)
+
+(* Properties with restricted refinement for local environments *************)
+
+lemma lsubr_cnuw_trans (h) (G):
+      ∀L2,T. ⦃G,L2⦄ ⊢ ➡𝐍𝐖*[h] T → ∀L1. L1 ⫃ L2 → ⦃G,L1⦄ ⊢ ➡𝐍𝐖*[h] T.
+#h #G #L2 #T1 #HT1 #L1 #HL12 #n #T2 #HT12 
+
+lemma lsubv_cpmuwe_trans (h) (a) (n) (G):
+      lsub_trans … (cpmuwe h n G) (lsubv h a G).
+#h #a #n #G #L2 #T1 #T2 * #HT12 #HT2 #L1 #HL12
+lapply (lsubv_cpms_trans … HT12 … HL12) -HT12 #HT12
+@(cpmuwe_intro … HT12) -HT12
+
+lemma cnv_cpmuwe_cpms_conf (h) (a) (G) (L):
+      ∀T. ⦃G,L⦄ ⊢ T ![h,a] → ∀n1,T1. ⦃G,L⦄ ⊢ T ➡*[n1,h] T1 →
+      ∀n2,T2. ⦃G,L⦄ ⊢ T ➡*𝐍𝐖*[h,n2] T2 →
+      ∃∃T0. ⦃G,L⦄ ⊢ T1 ➡*[n2-n1,h] T0 & T0 ≅ T2 & ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] T2.
+#h #a #G #L #T0 #HT0 #n1 #T1 #HT01 #n2 #T2 * #HT02 #HT2
+elim (cnv_cpms_conf … HT0 … HT01 … HT02) -T0 #T0 #HT10 #HT20
+lapply (HT2 … HT20) -HT20 #HT20
+/3 width=3 by tweq_sym, ex3_intro/
+qed-.
+
+lemma lsubv_cpms_abst_conf_cnv (h) (a) (G) (L1) (T0):
+      ∀n1,p1,W1,T1. ⦃G,L1⦄ ⊢ T0 ➡*[n1,h] ⓛ{p1}W1.T1 →
+      ∀L2. ⦃G,L2⦄ ⊢ T0 ![h,a] → G ⊢ L1 ⫃![h,a] L2 →
+      ∃∃n2,p2,W2,T2. ⦃G,L2⦄ ⊢ T0 ➡*[n2,h] ⓛ{p2}W2.T2.
+#h #a #G #L1 #T0 #n1 #p1 #W1 #T1 #HT01 #L2 #HT0 #HL12
+elim (cnv_R_cpmuwe_total … HT0) #n2 * #X2 #HT02
+elim (abst_dec X2) [ * | #HnX2 ]
+[ #p2 #W2 #T2 #H destruct
+  /3 width=5 by cpmuwe_fwd_cpms, ex1_4_intro/
+| lapply (lsubv_cnv_trans … HT0 … HL12) -HT0 #HT0
+  lapply (lsubv_cpmuwe_trans … HT02 … HL12) -HT02 -HL12 #HT02
+  elim (cnv_cpmuwe_cpms_conf … HT0 … HT01 … HT02) -HT0 -HT01 -HT02 #U2 #H1 #H2 #_ 
+  elim (cpms_inv_abst_sn … H1) -H1 #W2 #T2 #_ #_ #H destruct
+  elim (tweq_inv_abst_sn … H2) -W2 -T2 #W2 #T2 #H destruct
+  elim (HnX2 p1 W2 T2) -HnX2 //
+]
+qed-.
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 3422c89b3..6bf92c3c1 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
@@ -25,7 +25,7 @@ table {
         ]
         [ { "context-sensitive native validity" * } {
              [ [ "restricted refinement for lenvs" ] "lsubv ( ? ⊢ ? ⫃![?,?] ? )" "lsubv_drops" + "lsubv_lsubr" + "lsubv_lsuba" + "lsubv_cpms" + "lsubv_cpcs" + "lsubv_cnv" + "lsubv_lsubv" * ]
-             [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "cnv_acle" + "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpm_tdeq" + "cnv_cpm_tdeq_trans" + "cnv_cpm_tdeq_conf" + "cnv_cpms_tdeq" + "cnv_cpms_conf" + "cnv_cpms_tdeq_conf" + "cnv_cpme" + "cnv_cpmuwe" + "cnv_cpmuwe_cpme" + "cnv_eval" + "cnv_cpce" + "cnv_lpce" + "cnv_cpes" + "cnv_cpcs" + "cnv_preserve_sub" + "cnv_preserve" + "cnv_preserve_cpes" + "cnv_preserve_cpcs" * ]
+             [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "cnv_acle" + "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpm_tdeq" + "cnv_cpm_tdeq_trans" + "cnv_cpm_tdeq_conf" + "cnv_cpms_tdeq" + "cnv_cpms_conf" + "cnv_cpms_tdeq_conf" + "cnv_cpme" + "cnv_cpmuwe" + "cnv_cpmuwe_cpme" + "cnv_eval" + "cnv_cpes" + "cnv_cpcs" + "cnv_preserve_sub" + "cnv_preserve" + "cnv_preserve_cpes" + "cnv_preserve_cpcs" * ]
           }
         ]
      }
@@ -44,12 +44,14 @@ table {
    ]
    class "blue"
    [ { "rt-conversion" * } {
+(*
         [ { "context-sensitive parallel eta-conversion" * } {
              [ [ "for lenvs on all entries" ] "lpce ( ⦃?,?⦄ ⊢ ⬌η[?] ? )" "lpce_drops" * ]
              [ [ "for binders" ] "cpce_ext" + "( ⦃?,?⦄ ⊢ ? ⬌η[?] ? )" * ]
              [ [ "for terms" ] "cpce" + "( ⦃?,?⦄ ⊢ ? ⬌η[?] ? )" "cpce_drops" * ]
           }
         ]
+*)
         [ { "context-sensitive parallel r-conversion" * } {
              [ [ "for terms" ] "cpc" + "( ⦃?,?⦄ ⊢ ? ⬌[?] ? )" "cpc_cpc" * ]
           }
-- 
2.39.2