From: Ferruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
Date: Wed, 19 Sep 2018 18:31:44 +0000 (+0200)
Subject: update in ground_2, static_2, basic_2
X-Git-Tag: make_still_working~279
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=945b096d007f70e8336847f07b174c48f26467e0;p=helm.git

update in ground_2, static_2, basic_2

+ confluence for restricted rt_transition under hyps
+ positive terms wrt the system of reference parked
---

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq_conf.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq_conf.ma
new file mode 100644
index 000000000..f45bf4d42
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq_conf.ma
@@ -0,0 +1,136 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "ground_2/xoa/ex_4_1_props.ma".
+include "basic_2/dynamic/cnv_cpm_tdeq.ma".
+
+(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
+
+definition IH_cnv_cpm_tdeq_conf_lpr (a) (h) (o): relation3 genv lenv term ≝
+                                    λG,L0,T0. ⦃G, L0⦄ ⊢ T0 ![a,h] →
+                                    ∀n1,T1. ⦃G, L0⦄ ⊢ T0 ➡[n1,h] T1 → T0 ≛[h,o] T1 →
+                                    ∀n2,T2. ⦃G, L0⦄ ⊢ T0 ➡[n2,h] T2 → T0 ≛[h,o] T2 →
+                                    ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 →
+                                    ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡[n2-n1,h] T & T1 ≛[h,o] T & ⦃G, L2⦄ ⊢ T2 ➡[n1-n2,h] T & T2 ≛[h,o] T.
+
+(* Diamond propery with restricted rt-transition for terms ******************)
+
+fact cnv_cpm_tdeq_conf_lpr_atom_atom_aux (h) (o) (G0) (L1) (L2) (I):
+     ∃∃T. ⦃G0,L1⦄ ⊢ ⓪{I} ➡[h] T & ⓪{I} ≛[h,o] T & ⦃G0, L2⦄ ⊢ ⓪{I} ➡[h] T & ⓪{I} ≛[h,o] T.
+#h #o #G0 #L1 #L2 #I
+/2 width=5 by ex4_intro/
+qed-.
+
+fact cnv_cpm_tdeq_conf_lpr_atom_ess_aux (h) (o) (G0) (L1) (L2) (s):
+     deg h o s 0 →
+     ∃∃T. ⦃G0,L1⦄ ⊢ ⋆s ➡[1,h] T & ⋆s ≛[h,o] T & ⦃G0,L2⦄ ⊢ ⋆(next h s) ➡[h] T & ⋆(next h s) ≛[h,o] T.
+#h #o #G0 #L1 #L2 #s #Hs
+/4 width=5 by tdeq_sort, deg_next, ex4_intro/
+qed-.
+
+fact cnv_cpm_tdeq_conf_lpr_bind_bind_aux (a) (h) (o) (p) (I) (G0) (L0) (V0) (T0):
+     (∀G,L,T. ⦃G0,L0,ⓑ{p,I}V0.T0⦄ ⊐+ ⦃G,L,T⦄ → IH_cnv_cpm_tdeq_conf_lpr a h o G L T) →
+     ⦃G0,L0⦄ ⊢ ⓑ{p,I}V0.T0 ![a,h] →
+     ∀n1,T1. ⦃G0,L0.ⓑ{I}V0⦄ ⊢ T0 ➡[n1,h] T1 → T0 ≛[h,o] T1 →
+     ∀n2,T2. ⦃G0,L0.ⓑ{I}V0⦄ ⊢ T0 ➡[n2,h] T2 → T0 ≛[h,o] T2 →
+     ∀L1. ⦃G0,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0,L0⦄ ⊢ ➡[h] L2 →
+     ∃∃T. ⦃G0,L1⦄ ⊢ ⓑ{p,I}V0.T1 ➡[n2-n1,h] T & ⓑ{p,I}V0.T1 ≛[h,o] T & ⦃G0,L2⦄ ⊢ ⓑ{p,I}V0.T2 ➡[n1-n2,h] T & ⓑ{p,I}V0.T2 ≛[h,o] T.
+#a #h #o #p #I #G0 #L0 #V0 #T0 #IH #H0
+#n1 #T1 #H1T01 #H2T01 #n2 #T2 #H1T02 #H2T02
+#L1 #HL01 #L2 #HL02
+elim (cnv_inv_bind … H0) -H0 #_ #HT0
+elim (IH … H1T01 H2T01 … H1T02 H2T02 (L1.ⓑ{I}V0) … (L2.ⓑ{I}V0)) [|*: /2 width=1 by lpr_bind_refl_dx/ ]
+#T #H1T1 #H2T1 #H1T2 #H2T2 -L0 -T0
+/3 width=7 by cpm_bind, tdeq_pair, ex4_intro/
+qed-.
+
+fact cnv_cpm_tdeq_conf_lpr_appl_appl_aux (a) (h) (o) (G0) (L0) (V0) (T0):
+     (∀G,L,T. ⦃G0,L0,ⓐV0.T0⦄ ⊐+ ⦃G,L,T⦄ → IH_cnv_cpm_tdeq_conf_lpr a h o G L T) →
+     ⦃G0,L0⦄ ⊢ ⓐV0.T0 ![a,h] →
+     ∀n1,T1. ⦃G0,L0⦄ ⊢ T0 ➡[n1,h] T1 → T0 ≛[h,o] T1 →
+     ∀n2,T2. ⦃G0,L0⦄ ⊢ T0 ➡[n2,h] T2 → T0 ≛[h,o] T2 →
+     ∀L1. ⦃G0,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0,L0⦄ ⊢ ➡[h] L2 →
+     ∃∃T. ⦃G0,L1⦄ ⊢ ⓐV0.T1 ➡[n2-n1,h] T & ⓐV0.T1 ≛[h,o] T & ⦃G0,L2⦄ ⊢ ⓐV0.T2 ➡[n1-n2,h] T & ⓐV0.T2 ≛[h,o] T.
+#a #h #o #G0 #L0 #V0 #T0 #IH #H0
+#n1 #T1 #H1T01 #H2T01 #n2 #T2 #H1T02 #H2T02
+#L1 #HL01 #L2 #HL02
+elim (cnv_inv_appl … H0) -H0 #n0 #p0 #X01 #X02 #_ #_ #HT0 #_ #_ -n0 -p0 -X01 -X02
+elim (IH … H1T01 H2T01 … H1T02 H2T02 … HL01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
+#T #H1T1 #H2T1 #H1T2 #H2T2 -L0 -T0
+/3 width=7 by cpm_appl, tdeq_pair, ex4_intro/
+qed-.
+
+fact cnv_cpm_tdeq_conf_lpr_cast_cast_aux (a) (h) (o) (G0) (L0) (V0) (T0):
+     (∀G,L,T. ⦃G0,L0,ⓝV0.T0⦄ ⊐+ ⦃G,L,T⦄ → IH_cnv_cpm_tdeq_conf_lpr a h o G L T) →
+     ⦃G0,L0⦄ ⊢ ⓝV0.T0 ![a,h] →
+     ∀n1,V1. ⦃G0,L0⦄ ⊢ V0 ➡[n1,h] V1 → V0 ≛[h,o] V1 →
+     ∀n2,V2. ⦃G0,L0⦄ ⊢ V0 ➡[n2,h] V2 → V0 ≛[h,o] V2 →
+     ∀T1. ⦃G0,L0⦄ ⊢ T0 ➡[n1,h] T1 → T0 ≛[h,o] T1 →
+     ∀T2. ⦃G0,L0⦄ ⊢ T0 ➡[n2,h] T2 → T0 ≛[h,o] T2 →
+     ∀L1. ⦃G0,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0,L0⦄ ⊢ ➡[h] L2 →
+     ∃∃T. ⦃G0,L1⦄ ⊢ ⓝV1.T1 ➡[n2-n1,h] T & ⓝV1.T1≛[h,o]T & ⦃G0,L2⦄ ⊢ ⓝV2.T2 ➡[n1-n2,h] T & ⓝV2.T2≛[h,o]T.
+#a #h #o #G0 #L0 #V0 #T0 #IH #H0
+#n1 #V1 #H1V01 #H2V01 #n2 #V2 #H1V02 #H2V02 #T1 #H1T01 #H2T01 #T2 #H1T02 #H2T02
+#L1 #HL01 #L2 #HL02
+elim (cnv_inv_cast … H0) -H0 #X0 #HV0 #HT0 #_ #_ -X0
+elim (IH … H1V01 H2V01 … H1V02 H2V02 … HL01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
+elim (IH … H1T01 H2T01 … H1T02 H2T02 … HL01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
+#T #H1T1 #H2T1 #H1T2 #H2T2 #V #H1V1 #H2V1 #H1V2 #H2V2 -L0 -V0 -T0
+/3 width=7 by cpm_cast, tdeq_pair, ex4_intro/
+qed-.
+
+fact cnv_cpm_tdeq_conf_lpr_aux (a) (h) (o) (G0) (L0) (T0):
+     (∀G,L,T. ⦃G0,L0,T0⦄ ⊐+ ⦃G,L,T⦄ → IH_cnv_cpm_tdeq_conf_lpr a h o G L T) →
+     ∀G,L,T. G0 = G → L0 = L → T0 = T → IH_cnv_cpm_tdeq_conf_lpr a h o G L T.
+#a #h #o #G0 #L0 #T0 #IH1 #G #L * [| * [| * ]]
+[ #I #HG0 #HL0 #HT0 #HT #n1 #X1 #H1X1 #H2X1 #n2 #X2 #H1X2 #H2X2 #L1 #HL1 #L2 #HL2 destruct
+  elim (cpm_tdeq_inv_atom_sn … H1X1 H2X1) -H1X1 -H2X1 *
+  elim (cpm_tdeq_inv_atom_sn … H1X2 H2X2) -H1X2 -H2X2 *
+  [ #H21 #H22 #H11 #H12 destruct -a -L
+    <minus_O_n
+    /2 width=1 by cnv_cpm_tdeq_conf_lpr_atom_atom_aux/
+  | #s2 #H21 #H22 #H23 #Hs2 #H11 #H12 destruct -a -L
+    <minus_O_n <minus_n_O
+    /2 width=1 by cnv_cpm_tdeq_conf_lpr_atom_ess_aux/
+  | #H21 #H22 #s1 #H11 #H12 #H13 #Hs1 destruct -a -L
+    <minus_O_n <minus_n_O
+    @ex4_commute /2 width=1 by cnv_cpm_tdeq_conf_lpr_atom_ess_aux/
+  | #s2 #H21 #H22 #H23 #_ #s1 #H11 #H12 #H13 #_ destruct -a -L
+    <minus_n_n
+    /2 width=1 by cnv_cpm_tdeq_conf_lpr_atom_atom_aux/
+  ]
+| #p #I #V #T #HG0 #HL0 #HT0 #HT #n1 #X1 #H1X1 #H2X1 #n2 #X2 #H1X2 #H2X2 #L1 #HL1 #L2 #HL2 destruct
+  elim (cpm_tdeq_inv_bind_sn … HT … H1X1 H2X1) -H1X1 -H2X1
+  elim (cpm_tdeq_inv_bind_sn … HT … H1X2 H2X2) -H1X2 -H2X2
+  #T2 #_ #_ #H1T2 #H2T2 #H21 #T1 #_ #_ #H1T1 #H2T1 #H11 destruct
+  @(cnv_cpm_tdeq_conf_lpr_bind_bind_aux … IH1) -IH1 /1 width=1 by/
+| #V #T #HG0 #HL0 #HT0 #HT #n1 #X1 #H1X1 #H2X1 #n2 #X2 #H1X2 #H2X2 #L1 #HL1 #L2 #HL2 destruct
+  elim (cpm_tdeq_inv_appl_sn … HT … H1X1 H2X1) -H1X1 -H2X1
+  elim (cpm_tdeq_inv_appl_sn … HT … H1X2 H2X2) -H1X2 -H2X2
+  #m2 #q2 #W2 #U2 #T2 #_ #_ #_ #_ #_ #H1T2 #H2T2 #H21 #m1 #q1 #W1 #U1 #T1 #_ #_ #_ #_ #_ #H1T1 #H2T1 #H11 destruct -m1 -m2 -q1 -q2 -W1 -W2 -U1 -U2
+  @(cnv_cpm_tdeq_conf_lpr_appl_appl_aux … IH1) -IH1 /1 width=1 by/
+| #V #T #HG0 #HL0 #HT0 #HT #n1 #X1 #H1X1 #H2X1 #n2 #X2 #H1X2 #H2X2 #L1 #HL1 #L2 #HL2 destruct
+  elim (cpm_tdeq_inv_cast_sn … HT … H1X1 H2X1) -H1X1 -H2X1
+  elim (cpm_tdeq_inv_cast_sn … HT … H1X2 H2X2) -H1X2 -H2X2
+  #U2 #V2 #T2 #_ #_ #_ #H1V2 #H2V2 #_ #H1T2 #H2T2 #H21 #U1 #V1 #T1 #_ #_ #_ #H1V1 #H2V1 #_ #H1T1 #H2T1 #H11 destruct -U1 -U2
+  @(cnv_cpm_tdeq_conf_lpr_cast_cast_aux … IH1) -IH1 /1 width=1 by/
+]
+qed-.
+
+lemma cnv_cpm_tdeq_conf_lpr (a) (h) (o) (G0) (L0) (T0):
+      IH_cnv_cpm_tdeq_conf_lpr a h o G0 L0 T0.
+#a #h #o #G0 #L0 #T0
+@(fqup_wf_ind (Ⓣ) … G0 L0 T0) -G0 -L0 -T0 #G0 #L0 #T0 #IH
+/3 width=17 by cnv_cpm_tdeq_conf_lpr_aux/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdpos.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdpos.ma
deleted file mode 100644
index 4cb320959..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdpos.ma
+++ /dev/null
@@ -1,55 +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 "static_2/syntax/tdpos.ma".
-include "basic_2/dynamic/cnv_cpm_tdeq.ma".
-
-(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
-
-(* Forward lemmas with positive rt-transition for terms *********************)
-
-lemma cpm_tdeq_fwd_tdpos_sn (a) (h) (o) (n) (G):
-                            ∀L,T1. ⦃G,L⦄ ⊢ T1 ![a,h] →
-                            ∀T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 → T1 ≛[h,o] T2 → 𝐏[h,o]⦃T1⦄ →
-                            ∧∧ T1 = T2 & 0 = n.
-#a #h #o #n #G #L #T1 #H0 #T2 #H1 #H2
-@(cpm_tdeq_ind … H0 … H1 H2) -L -T1 -T2
-[ /2 width=1 by conj/
-| #L #s #_ #H1 #H
-  elim (tdpos_inv_sort … H) -H #d #H2
-  lapply (deg_mono … H2 H1) -H1 -H2 #H destruct
-| #p #I #L #V #T1 #_ #_ #T2 #_ #_ #IH #H
-  elim (tdpos_inv_pair … H) -H #_ #HT1
-  elim IH // -IH -HT1 #H1 #H2 destruct
-  /2 width=1 by conj/
-| #m #_ #L #V #_ #W #_ #q #T1 #U1 #_ #_ #T2 #_ #_ #IH #H -a -m -q -G -L -W -U1
-  elim (tdpos_inv_pair … H) -H #_ #HT1
-  elim IH // -IH -HT1 #H1 #H2 destruct
-  /2 width=1 by conj/
-| #L #U0 #U1 #T1 #_ #_ #U2 #_ #_ #_ #T2 #_ #_ #_ #IHU #IHT #H
-  elim (tdpos_inv_pair … H) -H #HU1 #HT1
-  elim IHU // -IHU -HU1 #H1 #H2 destruct
-  elim IHT // -IHT -HT1 #H1 #H2 destruct
-  /2 width=1 by conj/
-]
-qed-.
-
-lemma cpm_fwd_tdpos_sn (a) (h) (o) (n) (G) (L):
-                       ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] → 𝐏[h,o]⦃T1⦄ →
-                       ∀T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 →
-                       ∨∨ ∧∧ T1 = T2 & 0 = n | (T1 ≛[h,o] T2 → ⊥).
-#a #h #o #n #G #L #T1 #H1T1 #H2T1 #T2 #HT12
-elim (tdeq_dec h o T1 T2) #H
-/3 width=9 by cpm_tdeq_fwd_tdpos_sn, or_intror, or_introl/
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_conf.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_conf.ma
index a86d5c311..729159536 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_conf.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_conf.ma
@@ -12,14 +12,69 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basic_2/dynamic/cnv_cpm_tdeq_conf.ma".
+include "basic_2/dynamic/cnv_cpms_tdeq.ma".
+(*
 include "basic_2/dynamic/cnv_cpm_trans.ma".
 include "basic_2/dynamic/cnv_cpm_conf.ma".
-include "basic_2/dynamic/cnv_cpms_tdpos.ma".
+*)
 
 (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
 
 (* Sub confluence propery with t-bound rt-computation for terms *************)
 
+fact cnv_cpms_tdeq_strip_lpr_aux (a) (h) (o) (G0) (L0) (T0):
+     (∀G,L,T. ⦃G0,L0,T0⦄ >[h,o] ⦃G,L,T⦄ → IH_cnv_cpm_trans_lpr a h G L T) →
+     (∀G,L,T. ⦃G0,L0,T0⦄ >[h,o] ⦃G,L,T⦄ → IH_cnv_cpms_conf_lpr a h G L T) →
+     ∀n1,T1. ⦃G0,L0⦄ ⊢ T0 ➡*[n1,h] T1 → ⦃G0,L0⦄ ⊢ T0 ![a,h] → T0 ≛[h,o] T1 →
+     ∀n2,T2. ⦃G0,L0⦄ ⊢ T0 ➡[n2,h] T2 → T0 ≛[h,o] T2 →
+     ∀L1. ⦃G0,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0,L0⦄ ⊢ ➡[h] L2 →
+     ∃∃T. ⦃G0,L1⦄ ⊢ T1 ➡[n2-n1,h] T & T1 ≛[h,o] T & ⦃G0,L2⦄ ⊢ T2 ➡*[n1-n2,h] T & T2 ≛[h,o] T.
+#a #h #o #G #L0 #T0 #IH2 #IH1 #n1 #T1 #H1T01 #H0T0 #H2T01
+@(cpms_tdeq_ind_sn … H1T01 H0T0 H2T01 IH1 IH2) -n1 -T0
+[ #H0T1 #n2 #T2 #H1T12 #H2T12 #L1 #HL01 #L2 #HL02
+  <minus_O_n <minus_n_O
+  elim (cnv_cpm_tdeq_conf_lpr … H0T1 0 T1 … H1T12 H2T12 … HL01 … HL02) // -L0 -H2T12
+  <minus_O_n <minus_n_O #T #H1T1 #H2T1 #H1T2 #H2T2
+  /3 width=5 by cpm_cpms, ex4_intro/
+| #m1 #m2 #T0 #T3 #H1T03 #H0T0 #H2T03 #_ #_ #_ #IH
+  #n2 #T2 #H1T02 #H2T02 #L1 #HL01 #L2 #HL02
+  elim (cnv_cpm_tdeq_conf_lpr … H0T0 … H1T03 H2T03 … H1T02 H2T02 … L0 … HL02) -T0 //
+  #T0 #H1T30 #H2T30 #H1T20 #H2T20
+  elim (IH … H1T30 H2T30 … HL01 … HL02) -L0 -T3
+  #T3 #H1T13 #H2T13 #H1T03 #H2T03
+  <minus_plus >arith_l3
+  /3 width=7 by cpms_step_sn, tdeq_trans, ex4_intro/
+]
+qed-.
+
+fact cnv_cpms_tdeq_conf_lpr_aux (a) (h) (o) (G0) (L0) (T0):
+     (∀G,L,T. ⦃G0,L0,T0⦄ >[h,o] ⦃G,L,T⦄ → IH_cnv_cpm_trans_lpr a h G L T) →
+     (∀G,L,T. ⦃G0,L0,T0⦄ >[h,o] ⦃G,L,T⦄ → IH_cnv_cpms_conf_lpr a h G L T) →
+     ∀n1,T1. ⦃G0,L0⦄ ⊢ T0 ➡*[n1,h] T1 → ⦃G0,L0⦄ ⊢ T0 ![a,h] → T0 ≛[h,o] T1 →
+     ∀n2,T2. ⦃G0,L0⦄ ⊢ T0 ➡*[n2,h] T2 → T0 ≛[h,o] T2 →
+     ∀L1. ⦃G0,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0,L0⦄ ⊢ ➡[h] L2 →
+     ∃∃T. ⦃G0,L1⦄ ⊢ T1 ➡*[n2-n1,h] T & T1 ≛[h,o] T & ⦃G0,L2⦄ ⊢ T2 ➡*[n1-n2,h] T & T2 ≛[h,o] T.
+#a #h #o #G #L0 #T0 #IH2 #IH1 #n1 #T1 #H1T01 #H0T0 #H2T01
+generalize in match IH1; generalize in match IH2;
+@(cpms_tdeq_ind_sn … H1T01 H0T0 H2T01 IH1 IH2) -n1 -T0
+[ #H0T1 #IH2 #IH1 #n2 #T2 #H1T12 #H2T12 #L1 #HL01 #L2 #HL02
+  <minus_O_n <minus_n_O
+  elim (cnv_cpms_tdeq_strip_lpr_aux … IH2 IH1 … H1T12 H0T1 H2T12 0 T1 … HL02 … HL01) // -L0 -H2T12
+  <minus_O_n <minus_n_O #T #H1T2 #H2T2 #H1T1 #H2T1
+  /3 width=5 by cpm_cpms, ex4_intro/
+| #m1 #m2 #T0 #T3 #H1T03 #H0T0 #H2T03 #_ #_ #_ #IH #IH2 #IH1
+  #n2 #T2 #H1T02 #H2T02 #L1 #HL01 #L2 #HL02
+  elim (cnv_cpms_tdeq_strip_lpr_aux … IH2 IH1 … H1T02 H0T0 H2T02 … H1T03 H2T03 … HL02 L0) -H0T0 -H2T03 //
+  #T4 #H1T24 #H2T24 #H1T34 #H2T34
+  elim (IH … H1T34 H2T34 … HL01 … HL02) [|*: /4 width=5 by cpm_fpbq, fpbq_fpbg_trans/ ] -L0 -T0 -T3 (**)
+  #T3 #H1T13 #H2T13 #H1T43 #H2T43
+  <minus_plus >arith_l3
+  /3 width=7 by cpms_step_sn, tdeq_trans, ex4_intro/
+]
+qed-.
+
+(*
 fact cnv_cpms_conf_lpr_refl_refl_aux (h) (G0) (L1) (L2) (T0:term):
      ∃∃T. ⦃G0,L1⦄ ⊢ T0 ➡*[h] T & ⦃G0,L2⦄ ⊢ T0 ➡*[h] T.
 /2 width=3 by ex2_intro/ qed-.
@@ -94,3 +149,4 @@ elim (cpms_fwd_tdpos_sn … HT0 H0 … HT02) *
   @(cnv_cpms_conf_lpr_step_step_aux … IH2 IH1) -IH2 -IH1 /2 width=4 by/
 ]
 qed-.
+*)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_tdeq.ma
index 3950479e1..b46d12d54 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_tdeq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_tdeq.ma
@@ -31,7 +31,7 @@ fact cpms_tdneq_fwd_step_sn_aux (a) (h) (n) (o) (G) (L) (T1):
   [ elim (tdeq_dec h o T T2) #H2T2
     [ -IH -IH2 -IH1 -H0T1 /4 width=7 by tdeq_trans, ex4_3_intro/
     | lapply (cnv_cpm_trans_lpr_aux … IH2 IH1 … H1T1 L ?) [6:|*: // ] -H1T2 -H2T12 #H0T
-      elim (IH H0T H2T2) [|*: /4 width=5 by cpm_fpbq, fpbq_fpbg_trans/ ] -IH -IH2 -H0T -H2T2
+      elim (IH H0T H2T2) [|*: /4 width=5 by cpm_fpbq, fpbq_fpbg_trans/ ] -IH -IH2 -H0T -H2T2 (**)
       #m1 #m2 #T0 #H1T0 #H2T0 #H1T02 #H destruct
       elim (cnv_cpm_tdeq_cpm_trans_aux … IH1 … H0T1 … H1T1 H2T1 … H1T0) -IH1 -H0T1 -H1T1 -H1T0
       #T3 #H1T13 #H1T30 #H2T30
@@ -56,7 +56,7 @@ fact cpms_tdeq_ind_sn (a) (h) (o) (G) (L) (T2) (Q:relation2 …):
   elim (tdeq_dec h o T1 T) #H2T1
   [ lapply (cnv_cpm_trans_lpr_aux … IH2 IH1 … H1T1 L ?) [6:|*: // ] #H0T
     lapply (tdeq_canc_sn … H2T1 … H2T12) -H2T12 #H2T2
-    /6 width=7 by cpm_fpbq, fpbq_fpbg_trans/
+    /6 width=7 by cpm_fpbq, fpbq_fpbg_trans/ (**)
   | -IB2 -IH -IH2 -IH1
     elim (cnv_fpbg_refl_false … o … H0T1) -a -Q
     /3 width=8 by cpm_tdneq_cpm_cpms_tdeq_sym_fwd_fpbg/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_tdpos.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_tdpos.ma
deleted file mode 100644
index 049e0727f..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_tdpos.ma
+++ /dev/null
@@ -1,39 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/dynamic/cnv_cpm_tdpos.ma".
-
-(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
-
-(* Forward lemmas with positive rt-computation for terms ********************)
-
-lemma cpms_fwd_tdpos_sn (a) (h) (o) (n) (G) (L):
-                        ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] → 𝐏[h,o]⦃T1⦄ →
-                        ∀T2. ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 →
-                        ∨∨ ∧∧ T1 = T2 & 0 = n
-                         | ∃∃n1,n2,T. ⦃G,L⦄ ⊢ T1 ➡[n1,h] T & (T1 ≛[h,o] T → ⊥) & ⦃G,L⦄ ⊢ T ➡*[n2,h] T2 & n1+n2=n.
-#a #h #o #n #G #L #T1 #H1T1 #H2T1 #T2 #H
-@(cpms_ind_dx … H) -n -T2
-[ /3 width=1 by or_introl, conj/
-| #n1 #n2 #T #T2 #HT1 * *
-  [ #H1 #H2 #HT2 destruct -HT1
-    elim (cpm_fwd_tdpos_sn … H1T1 H2T1 … HT2) -H1T1 -H2T1
-    [ * #H1 #H2 destruct -HT2 /3 width=1 by or_introl, conj/
-    | #HnT2 >commutative_plus in ⊢ (??%); /4 width=7 by ex4_3_intro, or_intror/
-    ]
-  | #m1 #m2 #T0 #H1T10 #H2T10 #HT0 #H #HT2 destruct -H1T1 -H2T1 -HT1
-    >associative_plus in ⊢ (??%); /4 width=7 by cpms_step_dx, ex4_3_intro, or_intror/
-  ]
-]
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve.ma
new file mode 100644
index 000000000..9e372bb3e
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve.ma
@@ -0,0 +1,104 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/dynamic/cnv_cpms_conf.ma".
+
+(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
+
+(* Main preservation properties *********************************************)
+(*
+(* Basic_2A1: uses: snv_preserve *)
+lemma cnv_preserve (a) (h): ∀G,L,T. ⦃G,L⦄ ⊢ T ![a,h] →
+                            ∧∧ IH_cnv_cpms_conf_lpr a h G L T
+                             & IH_cnv_cpm_trans_lpr a h G L T.
+#a #h #G #L #T #HT
+elim (tdpos_total h … T) #o
+lapply (cnv_fwd_fsb … o … HT) -HT #H
+@(fsb_ind_fpbg … H) -G -L -T #G #L #T #_ #IH #Ho
+@conj [ letin aux ≝ cnv_cpms_conf_lpr_aux | letin aux ≝ cnv_cpm_trans_lpr_aux ]
+@(aux … o … G L T) // #G0 #L0 #T0 #H
+elim (IH … H) -IH -H //
+
+
+lemma snv_preserve: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, o] →
+                    ∧∧ IH_da_cpr_lpr h o G L T
+                     & IH_snv_cpr_lpr h o G L T
+                     & IH_snv_lstas h o G L T
+                     & IH_lstas_cpr_lpr h o G L T.
+#h #o #G #L #T #HT elim (snv_fwd_aaa … HT) -HT
+#A #HT @(aaa_ind_fpbg h o … HT) -G -L -T -A
+#G #L #T #A #_ #IH -A @and4_intro
+[ letin aux ≝ da_cpr_lpr_aux | letin aux ≝ snv_cpr_lpr_aux
+| letin aux ≝ snv_lstas_aux | letin aux ≝ lstas_cpr_lpr_aux
+]
+@(aux … G L T) // #G0 #L0 #T0 #H elim (IH … H) -IH -H //
+qed-.
+
+theorem da_cpr_lpr: ∀h,o,G,L,T. IH_da_cpr_lpr h o G L T.
+#h #o #G #L #T #HT elim (snv_preserve … HT) /2 width=1 by/
+qed-.
+
+theorem snv_cpr_lpr: ∀h,o,G,L,T. IH_snv_cpr_lpr h o G L T.
+#h #o #G #L #T #HT elim (snv_preserve … HT) /2 width=1 by/
+qed-.
+
+theorem snv_lstas: ∀h,o,G,L,T. IH_snv_lstas h o G L T.
+#h #o #G #L #T #HT elim (snv_preserve … HT) /2 width=5 by/
+qed-.
+
+theorem lstas_cpr_lpr: ∀h,o,G,L,T. IH_lstas_cpr_lpr h o G L T.
+#h #o #G #L #T #HT elim (snv_preserve … HT) /2 width=3 by/
+qed-.
+
+(* Advanced preservation properties *****************************************)
+
+lemma snv_cprs_lpr: ∀h,o,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
+                    ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, o].
+#h #o #G #L1 #T1 #HT1 #T2 #H
+@(cprs_ind … H) -T2 /3 width=5 by snv_cpr_lpr/
+qed-.
+
+lemma da_cprs_lpr: ∀h,o,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
+                   ∀d. ⦃G, L1⦄ ⊢ T1 ▪[h, o] d →
+                   ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ▪[h, o] d.
+#h #o #G #L1 #T1 #HT1 #d #Hd #T2 #H
+@(cprs_ind … H) -T2 /3 width=6 by snv_cprs_lpr, da_cpr_lpr/
+qed-.
+
+lemma lstas_cprs_lpr: ∀h,o,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
+                      ∀d1,d2. d2 ≤ d1 → ⦃G, L1⦄ ⊢ T1 ▪[h, o] d1 →
+                      ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, d2] U1 →
+                      ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
+                      ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, d2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2.
+#h #o #G #L1 #T1 #HT1 #d1 #d2 #Hd21 #Hd1 #U1 #HTU1 #T2 #H
+@(cprs_ind … H) -T2 [ /2 width=10 by lstas_cpr_lpr/ ]
+#T #T2 #HT1T #HTT2 #IHT1 #L2 #HL12
+elim (IHT1 L1) // -IHT1 #U #HTU #HU1
+elim (lstas_cpr_lpr … o … Hd21 … HTU … HTT2 … HL12) -HTU -HTT2
+[2,3: /2 width=7 by snv_cprs_lpr, da_cprs_lpr/ ] -T1 -T -d1
+/4 width=5 by lpr_cpcs_conf, cpcs_trans, ex2_intro/
+qed-.
+
+lemma lstas_cpcs_lpr: ∀h,o,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
+                      ∀d,d1. d ≤ d1 → ⦃G, L1⦄ ⊢ T1 ▪[h, o] d1 → ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, d] U1 →
+                      ∀T2. ⦃G, L1⦄ ⊢ T2 ¡[h, o] →
+                      ∀d2. d ≤ d2 → ⦃G, L1⦄ ⊢ T2 ▪[h, o] d2 → ∀U2. ⦃G, L1⦄ ⊢ T2 •*[h, d] U2 →
+                      ⦃G, L1⦄ ⊢ T1 ⬌* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ U1 ⬌* U2.
+#h #o #G #L1 #T1 #HT1 #d #d1 #Hd1 #HTd1 #U1 #HTU1 #T2 #HT2 #d2 #Hd2 #HTd2 #U2 #HTU2 #H #L2 #HL12
+elim (cpcs_inv_cprs … H) -H #T #H1 #H2
+elim (lstas_cprs_lpr … HT1 … Hd1 HTd1 … HTU1 … H1 … HL12) -T1 #W1 #H1 #HUW1
+elim (lstas_cprs_lpr … HT2 … Hd2 HTd2 … HTU2 … H2 … HL12) -T2 #W2 #H2 #HUW2
+lapply (lstas_mono … H1 … H2) -h -T -d #H destruct /2 width=3 by cpcs_canc_dx/
+qed-.
+*)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_preserve.etc b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_preserve.etc
deleted file mode 100644
index 482b94451..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_preserve.etc
+++ /dev/null
@@ -1,94 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/computation/fsb_aaa.ma".
-include "basic_2/dynamic/snv_da_lpr.ma".
-include "basic_2/dynamic/snv_lstas.ma".
-include "basic_2/dynamic/snv_lstas_lpr.ma".
-include "basic_2/dynamic/snv_lpr.ma".
-
-(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
-
-(* Main preservation properties *********************************************)
-
-lemma snv_preserve: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, o] →
-                    ∧∧ IH_da_cpr_lpr h o G L T
-                     & IH_snv_cpr_lpr h o G L T
-                     & IH_snv_lstas h o G L T
-                     & IH_lstas_cpr_lpr h o G L T.
-#h #o #G #L #T #HT elim (snv_fwd_aaa … HT) -HT
-#A #HT @(aaa_ind_fpbg h o … HT) -G -L -T -A
-#G #L #T #A #_ #IH -A @and4_intro
-[ letin aux ≝ da_cpr_lpr_aux | letin aux ≝ snv_cpr_lpr_aux
-| letin aux ≝ snv_lstas_aux | letin aux ≝ lstas_cpr_lpr_aux
-]
-@(aux … G L T) // #G0 #L0 #T0 #H elim (IH … H) -IH -H //
-qed-.
-
-theorem da_cpr_lpr: ∀h,o,G,L,T. IH_da_cpr_lpr h o G L T.
-#h #o #G #L #T #HT elim (snv_preserve … HT) /2 width=1 by/
-qed-.
-
-theorem snv_cpr_lpr: ∀h,o,G,L,T. IH_snv_cpr_lpr h o G L T.
-#h #o #G #L #T #HT elim (snv_preserve … HT) /2 width=1 by/
-qed-.
-
-theorem snv_lstas: ∀h,o,G,L,T. IH_snv_lstas h o G L T.
-#h #o #G #L #T #HT elim (snv_preserve … HT) /2 width=5 by/
-qed-.
-
-theorem lstas_cpr_lpr: ∀h,o,G,L,T. IH_lstas_cpr_lpr h o G L T.
-#h #o #G #L #T #HT elim (snv_preserve … HT) /2 width=3 by/
-qed-.
-
-(* Advanced preservation properties *****************************************)
-
-lemma snv_cprs_lpr: ∀h,o,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
-                    ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, o].
-#h #o #G #L1 #T1 #HT1 #T2 #H
-@(cprs_ind … H) -T2 /3 width=5 by snv_cpr_lpr/
-qed-.
-
-lemma da_cprs_lpr: ∀h,o,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
-                   ∀d. ⦃G, L1⦄ ⊢ T1 ▪[h, o] d →
-                   ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ▪[h, o] d.
-#h #o #G #L1 #T1 #HT1 #d #Hd #T2 #H
-@(cprs_ind … H) -T2 /3 width=6 by snv_cprs_lpr, da_cpr_lpr/
-qed-.
-
-lemma lstas_cprs_lpr: ∀h,o,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
-                      ∀d1,d2. d2 ≤ d1 → ⦃G, L1⦄ ⊢ T1 ▪[h, o] d1 →
-                      ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, d2] U1 →
-                      ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
-                      ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, d2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2.
-#h #o #G #L1 #T1 #HT1 #d1 #d2 #Hd21 #Hd1 #U1 #HTU1 #T2 #H
-@(cprs_ind … H) -T2 [ /2 width=10 by lstas_cpr_lpr/ ]
-#T #T2 #HT1T #HTT2 #IHT1 #L2 #HL12
-elim (IHT1 L1) // -IHT1 #U #HTU #HU1
-elim (lstas_cpr_lpr … o … Hd21 … HTU … HTT2 … HL12) -HTU -HTT2
-[2,3: /2 width=7 by snv_cprs_lpr, da_cprs_lpr/ ] -T1 -T -d1
-/4 width=5 by lpr_cpcs_conf, cpcs_trans, ex2_intro/
-qed-.
-
-lemma lstas_cpcs_lpr: ∀h,o,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
-                      ∀d,d1. d ≤ d1 → ⦃G, L1⦄ ⊢ T1 ▪[h, o] d1 → ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, d] U1 →
-                      ∀T2. ⦃G, L1⦄ ⊢ T2 ¡[h, o] →
-                      ∀d2. d ≤ d2 → ⦃G, L1⦄ ⊢ T2 ▪[h, o] d2 → ∀U2. ⦃G, L1⦄ ⊢ T2 •*[h, d] U2 →
-                      ⦃G, L1⦄ ⊢ T1 ⬌* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ U1 ⬌* U2.
-#h #o #G #L1 #T1 #HT1 #d #d1 #Hd1 #HTd1 #U1 #HTU1 #T2 #HT2 #d2 #Hd2 #HTd2 #U2 #HTU2 #H #L2 #HL12
-elim (cpcs_inv_cprs … H) -H #T #H1 #H2
-elim (lstas_cprs_lpr … HT1 … Hd1 HTd1 … HTU1 … H1 … HL12) -T1 #W1 #H1 #HUW1
-elim (lstas_cprs_lpr … HT2 … Hd2 HTd2 … HTU2 … H2 … HL12) -T2 #W2 #H2 #HUW2
-lapply (lstas_mono … H1 … H2) -h -T -d #H destruct /2 width=3 by cpcs_canc_dx/
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cnv/cnv_cpm_tdeq1_conf.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cnv/cnv_cpm_tdeq1_conf.etc
deleted file mode 100644
index 01de9e4d1..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/cnv/cnv_cpm_tdeq1_conf.etc
+++ /dev/null
@@ -1,377 +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/cpm_lsubr.ma".
-include "basic_2/rt_transition/lpr_drops.ma".
-include "basic_2/dynamic/cnv_drops.ma".
-include "basic_2/dynamic/cnv_cpm_tdeq.ma".
-include "basic_2/dynamic/cnv_preserve_sub.ma".
-
-(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
-
-definition IH_cnv_cpm_tdeq1_conf_lpr (a) (h) (o): relation3 genv lenv term ≝
-                                     λG,L0,T0. ⦃G, L0⦄ ⊢ T0 ![a,h] →
-                                     ∀n1,T1. ⦃G, L0⦄ ⊢ T0 ➡[n1,h] T1 → T0 ≛[h,o] T1 →
-                                     ∀n2,T2. ⦃G, L0⦄ ⊢ T0 ➡[n2,h] T2 →
-                                     ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → L0 ≛[h, o, T0] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 →
-                                     ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡[n2-n1,h] T & ⦃G, L2⦄ ⊢ T2 ➡[n1-n2,h] T & T2 ≛[h,o] T.
-
-definition IH_cnv_cpms_tdeq1_strip_lpr (a) (h) (o): relation3 genv lenv term ≝
-                                       λG,L0,T0. ⦃G, L0⦄ ⊢ T0 ![a,h] →
-                                       ∀n1,T1. ⦃G, L0⦄ ⊢ T0 ➡[n1,h] T1 → T0 ≛[h,o] T1 →
-                                       ∀n2,T2. ⦃G, L0⦄ ⊢ T0 ➡*[n2,h] T2 →
-                                       ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → L0 ≛[h, o, T0] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 →
-                                       ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡*[n2-n1,h] T & ⦃G, L2⦄ ⊢ T2 ➡[n1-n2,h] T & T2 ≛[h,o] T.
-
-definition IH_cnv_cpm_tdeq2_conf_lpr (a) (h) (o): relation3 genv lenv term ≝
-                                     λG,L0,T0. ⦃G, L0⦄ ⊢ T0 ![a,h] →
-                                     ∀n1,T1. ⦃G, L0⦄ ⊢ T0 ➡[n1,h] T1 → T0 ≛[h,o] T1 →
-                                     ∀n2,T2. ⦃G, L0⦄ ⊢ T0 ➡[n2,h] T2 → T0 ≛[h,o] T2 →
-                                     ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 →
-                                     ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡[n2-n1,h] T & T1 ≛[h,o] T & ⦃G, L2⦄ ⊢ T2 ➡[n1-n2,h] T & T2 ≛[h,o] T.
-
-definition IH_cnv_cpm_tdeq2_strip_lpr (a) (h) (o): relation3 genv lenv term ≝
-                                      λG,L0,T0. ⦃G, L0⦄ ⊢ T0 ![a,h] →
-                                      ∀n1,T1. ⦃G, L0⦄ ⊢ T0 ➡[n1,h] T1 → T0 ≛[h,o] T1 →
-                                      ∀n2,T2. ⦃G, L0⦄ ⊢ T0 ➡*[n2,h] T2 → T0 ≛[h,o] T2 →
-                                      ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 →
-                                      ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡*[n2-n1,h] T & T1 ≛[h,o] T & ⦃G, L2⦄ ⊢ T2 ➡[n1-n2,h] T & T2 ≛[h,o] T.
-
-include "ground_2/lib/arith_2b.ma".
-include "basic_2/rt_computation/cpms_rdeq.ma".
-include "basic_2/rt_computation/cpms_fpbg.ma".
-
-fact cnv_cpms_tdeq1_strip_lpr_sub (a) (h) (o):
-                                  ∀G0,L0,T0.
-                                  (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_trans_lpr a h G1 L1 T1) →
-                                  (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_tdeq1_conf_lpr a h o G1 L1 T1) →
-                                  ∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_tdeq1_strip_lpr a h o G1 L1 T1.
-#a #h #o #G #L #T #IH2 #IH1 #G0 #L0 #T0 #H0 #HT0 #n1 #T1 #H1T01 #H2T01 #n2 #T2 #H @(cpms_ind_dx … H) -n2 -T2
-[ #L1 #H1L01 #H2L01 #L2 #HL02 -IH2
-  elim (IH1 … H1T01 H2T01 0 T0 … L1 … L2) // -L0 -IH1 -H2T01 #T3 #HT13 #H1T03 #H2T03
-  /3 width=4 by cpm_cpms, ex3_intro/
-| #n #n2 #X2 #T2 #HX2 #IHX2 #HXT2 #L1 #H1L01 #H2L01 #L2 #HL02 -H1T01 -H2T01
-  elim (IHX2 L1 … L0) -IHX2 // #X1 #HTX1 #H1X21 #H2X21
-  elim (IH1 … H1X21 H2X21 … HXT2 L1 … L2)
-  [|*: /3 width=12 by cnv_cpms_trans_lpr_sub, fpbg_cpms_trans, cpms_rdeq_conf_sn/ ] -X2 -IH1 -IH2 #X2 #HX12 #H1TX2 #H2TX2
-  >arith_l3 @(ex3_intro … H2TX2) /2 width=3 by cpms_step_dx/ (**) (* explict constructor *)
-]
-qed-.
-
-(* Sub diamond propery with restricted rt-transition for terms **************)
-
-fact cnv_cpm_tdeq1_conf_lpr_atom_atom_aux (h) (o) (G) (L1) (L2) (I):
-     ∃∃T. ⦃G,L1⦄ ⊢ ⓪{I} ➡[0,h] T & ⦃G, L2⦄ ⊢ ⓪{I} ➡[O,h] T & ⓪{I} ≛[h,o] T.
-/2 width=4 by ex3_intro/ qed-.
-
-fact cnv_cpm_tdeq1_conf_lpr_atom_ess_aux (h) (o) (G) (L1) (L2) (s):
-     ∃∃T. ⦃G,L1⦄ ⊢ ⋆s ➡[1,h] T & ⦃G,L2⦄ ⊢ ⋆(next h s) ➡[h] T & ⋆(next h s) ≛[h,o] T.
-/2 width=4 by ex3_intro/ qed-.
-
-fact cnv_cpm_tdeq1_conf_lpr_ess_atom_aux (h) (o) (G) (L1) (L2) (s):
-     deg h o s 0 →
-     ∃∃T. ⦃G,L1⦄ ⊢ ⋆(next h s) ➡[h] T & ⦃G,L2⦄ ⊢⋆s ➡[1,h] T & ⋆s ≛[h,o] T.
-/4 width=6 by tdeq_sort, deg_next, ex3_intro/ qed-.
-
-fact cnv_cpm_tdeq1_conf_lpr_atom_delta_aux (a) (h) (o) (G) (L) (i):
-     (∀G0,L0,T0. ⦃G,L,#i⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpm_tdeq1_conf_lpr a h o G0 L0 T0) →
-     ⦃G,L⦄ ⊢ #i ![a,h] →
-     ∀K,V. ⬇*[i]L ≘ K.ⓓV →
-     ∀n,XV. ⦃G,K⦄ ⊢ V ➡[n,h] XV →
-     ∀X. ⬆*[↑i]XV ≘ X →
-     ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → L ≛[h,o,#i] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
-     ∃∃T. ⦃G,L1⦄ ⊢ #i ➡[n,h] T & ⦃G,L2⦄ ⊢ X ➡[h] T & X ≛[h,o] T.
-#a #h #o #G #L #i #IH #HT #K #V #HLK #n #XV #HVX #X #HXV #L1 #H1L1 #H2L1 #L2 #HL2
-lapply (cnv_lref_fwd_drops … HT … HLK) -HT #HV
-elim (lpr_drops_conf … HLK … H1L1) -H1L1 // #Y1 #H1 #HLK1
-elim (lpr_inv_pair_sn … H1) -H1 #K1 #V1 #H1K1 #H1V1 #H destruct
-elim (rdeq_inv_lref_pair_bi … H2L1 … HLK … HLK1) -H2L1 #H2K1 #H2V1 #_
-elim (lpr_drops_conf … HLK … HL2) -HL2 // #Y2 #H2 #HLK2
-elim (lpr_inv_pair_sn … H2) -H2 #K2 #V2 #HK2 #_ #H destruct
-lapply (drops_isuni_fwd_drop2 … HLK2) -V2 // #HLK2
-lapply (fqup_lref (Ⓣ) … G … HLK) -HLK #HLK
-elim (IH … H1V1 H2V1 … HVX … H1K1 H2K1 … HK2) [|*: /2 width=1 by fqup_fpbg/ ] -L -K -V
-<minus_O_n <minus_n_O #V #HV1 #H1VX #H2VX
-elim (cpm_lifts_sn … H1VX … HLK2 … HXV) -H1VX -HLK2 #VX #HVX #HXVX
-lapply (tdeq_lifts_bi … H2VX … HXV … HVX) -H2VX -HXV #H2VX
-/3 width=6 by cpm_delta_drops, ex3_intro/
-qed-.
-
-fact cnv_cpm_tdeq1_conf_lpr_atom_ell_aux (a) (h) (o) (G) (L) (i):
-     (∀G0,L0,T0. ⦃G,L,#i⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpm_tdeq1_conf_lpr a h o G0 L0 T0) →
-     ⦃G,L⦄⊢#i![a,h] →
-     ∀K,W. ⬇*[i]L ≘ K.ⓛW →
-     ∀n,XW. ⦃G,K⦄ ⊢ W ➡[n,h] XW →
-     ∀X. ⬆*[↑i]XW ≘ X →
-     ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → L ≛[h,o,#i] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
-     ∃∃T. ⦃G,L1⦄ ⊢ #i ➡[↑n,h] T & ⦃G,L2⦄ ⊢ X ➡[h] T & X ≛[h,o] T.
-#a #h #o #G #L #i #IH #HT #K #W #HLK #n #XW #HWX #X #HXW #L1 #H1L1 #H2L1 #L2 #HL2
-lapply (cnv_lref_fwd_drops … HT … HLK) -HT #HW
-elim (lpr_drops_conf … HLK … H1L1) -H1L1 // #Y1 #H1 #HLK1
-elim (lpr_inv_pair_sn … H1) -H1 #K1 #W1 #H1K1 #H1W1 #H destruct
-elim (rdeq_inv_lref_pair_bi … H2L1 … HLK … HLK1) -H2L1 #H2K1 #H2W1 #_
-elim (lpr_drops_conf … HLK … HL2) -HL2 // #Y2 #H2 #HLK2
-elim (lpr_inv_pair_sn … H2) -H2 #K2 #W2 #HK2 #_ #H destruct
-lapply (drops_isuni_fwd_drop2 … HLK2) -W2 // #HLK2
-lapply (fqup_lref (Ⓣ) … G … HLK) -HLK #HLK
-elim (IH … H1W1 H2W1 … HWX … H1K1 H2K1 … HK2) [|*: /2 width=1 by fqup_fpbg/ ] -L -K -W
-<minus_O_n <minus_n_O #W #HW1 #H1WX #H2WX
-elim (cpm_lifts_sn … H1WX … HLK2 … HXW) -H1WX -HLK2 #WX #HWX #HXWX
-lapply (tdeq_lifts_bi … H2WX … HXW … HWX) -H2WX -HXW #H2WX
-/3 width=6 by cpm_ell_drops, ex3_intro/
-qed-.
-
-fact cnv_cpm_tdeq1_conf_lpr_bind_bind_aux (a) (h) (o) (p) (I) (G) (L) (V) (T):
-     (∀G0,L0,T0. ⦃G,L,ⓑ{p,I}V.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpm_tdeq1_conf_lpr a h o G0 L0 T0) →
-     ⦃G,L⦄ ⊢ ⓑ{p,I}V.T ![a,h] →
-     ∀V2. ⦃G,L⦄ ⊢ V ➡[h] V2 →
-     ∀n1,T1. ⦃G,L.ⓑ{I}V⦄ ⊢ T ➡[n1,h] T1 → T ≛[h,o] T1 →
-     ∀n2,T2. ⦃G,L.ⓑ{I}V⦄ ⊢ T ➡[n2,h] T2 →
-     ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → L ≛[h,o,ⓑ{p,I}V.T] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
-     ∃∃T. ⦃G,L1⦄ ⊢ ⓑ{p,I}V.T1 ➡[n2-n1,h] T & ⦃G,L2⦄ ⊢ ⓑ{p,I}V2.T2 ➡[n1-n2,h] T & ⓑ{p,I}V2.T2 ≛[h,o] T.
-#a #h #o #p #I #G0 #L0 #V0 #T0 #IH #H0
-#V2 #HV02 #n1 #T1 #H1T01 #H2T01 #n2 #T2 #HT02
-#L1 #H1L01 #H2L01 #L2 #HL02
-elim (cnv_inv_bind … H0) -H0 #HV0 #HT0
-elim (rdeq_inv_bind … H2L01) -H2L01 #H0L01 #H2L01
-elim (IH … V0 … 0 V0 … HV02 … H1L01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
--H0L01 <minus_n_O #V #HV1 #H1V2 #H2V2
-elim (IH … H1T01 H2T01 … HT02 (L1.ⓑ{I}V0) … (L2.ⓑ{I}V2)) [|*: /2 width=1 by fqup_fpbg, lpr_pair/ ]
-#T #HT1 #H1T2 #H2T2 -L0 -T0
-/3 width=6 by cpm_bind, tdeq_pair, ex3_intro/
-qed-.
-
-fact cnv_cpm_tdeq1_conf_lpr_bind_zeta_aux (a) (h) (o) (G) (L) (V) (T):
-     (∀G0,L0,T0. ⦃G,L,+ⓓV.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpm_tdeq1_conf_lpr a h o G0 L0 T0) →
-     ⦃G,L⦄ ⊢ +ⓓV.T ![a,h] →
-     ∀n1,T1. ⦃G,L.ⓓV⦄ ⊢ T ➡[n1,h] T1 → T ≛[h,o] T1 →
-     ∀T2. ⬆*[1]T2 ≘ T → ∀n2,XT2. ⦃G,L⦄ ⊢ T2 ➡[n2,h] XT2 →
-     ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → L ≛[h,o,+ⓓV.T]L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
-     ∃∃T. ⦃G,L1⦄ ⊢ +ⓓV.T1 ➡[n2-n1,h] T & ⦃G,L2⦄ ⊢ XT2 ➡[n1-n2,h] T & XT2 ≛[h,o] T.
-#a #h #o #G0 #L0 #V0 #T0 #IH #H0
-#n1 #T1 #H1T01 #H2T01 #T2 #HT20 #n2 #XT2 #HXT2
-#L1 #H1L01 #H2L01 #L2 #HL02
-elim (cnv_inv_bind … H0) -H0 #_ #HT0
-elim (rdeq_inv_bind … H2L01) -H2L01 #_ #H2L01
-lapply (cnv_inv_lifts … HT0 (Ⓣ) … L0 … HT20) -HT0
-[ /3 width=3 by drops_refl, drops_drop/ ] #HT2
-elim (cpm_inv_lifts_sn … H1T01 (Ⓣ) … L0 … HT20) -H1T01
-[| /3 width=1 by drops_refl, drops_drop/ ] #XT1 #HXT1 #H1XT12
-lapply (tdeq_inv_lifts_bi … H2T01 … HT20 … HXT1) -H2T01 #H2XT12
-lapply (rdeq_inv_lifts_bi … H2L01 (Ⓣ) … L0 L1 … HT20) -H2L01
-[4:|*: /3 width=1 by drops_refl, drops_drop/ ] #H2L01
-elim (IH … H1XT12 H2XT12 … HXT2 … H1L01 … HL02)
-[|*: /3 width=1 by fqup_fpbg, fqup_zeta/ ] -L0 -T0 #T #HT1 #H1T2 #H2T2
-/3 width=4 by cpm_zeta, ex3_intro/
-qed-.
-
-fact cnv_cpm_tdeq1_conf_lpr_appl_appl_aux (a) (h) (o) (G) (L) (V) (T):
-     (∀G0,L0,T0. ⦃G,L,ⓐV.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpm_tdeq1_conf_lpr a h o G0 L0 T0) →
-     ⦃G,L⦄ ⊢ ⓐV.T ![a,h] →
-     ∀V2. ⦃G,L⦄ ⊢ V ➡[h] V2 →
-     ∀n1,T1. ⦃G,L⦄ ⊢ T ➡[n1,h] T1 → T ≛[h,o] T1 →
-     ∀n2,T2. ⦃G,L⦄ ⊢ T ➡[n2,h] T2 →
-     ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → L ≛[h,o,ⓐV.T] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
-     ∃∃T. ⦃G,L1⦄ ⊢ ⓐV.T1 ➡[n2-n1,h] T & ⦃G,L2⦄ ⊢ ⓐV2.T2 ➡[n1-n2,h] T & ⓐV2.T2 ≛[h,o] T.
-#a #h #o #G0 #L0 #V0 #T0 #IH #H0
-#V2 #HV02 #n1 #T1 #H1T01 #H2T01 #n2 #T2 #HT02
-#L1 #H1L01 #H2L01 #L2 #HL02
-elim (cnv_inv_appl … H0) -H0 #n0 #p0 #X01 #X02 #_ #HV0 #HT0 #_ #_ -n0 -p0 -X01 -X02
-elim (rdeq_inv_flat … H2L01) -H2L01 #H0L01 #H2L01
-elim (IH … V0 … 0 V0 … HV02 … H1L01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
--H0L01 <minus_n_O #V #HV1 #H1V2 #H2V2
-elim (IH … H1T01 H2T01 … HT02 … H1L01 H2L01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
-#T #HT1 #H1T2 #H2T2 -L0 -T0
-/3 width=6 by cpm_appl, tdeq_pair, ex3_intro/
-qed-.
-
-fact cnv_cpm_tdeq1_conf_lpr_appl_beta_aux (a) (h) (o) (p) (G) (L) (V) (W) (T):
-     (∀G0,L0,T0. ⦃G,L,ⓐV.ⓛ{p}W.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpm_tdeq1_conf_lpr a h o G0 L0 T0) →
-     ⦃G,L⦄ ⊢ ⓐV.ⓛ{p}W.T ![a,h] →
-     ∀V2. ⦃G,L⦄ ⊢ V ➡[h] V2 → ∀W2. ⦃G,L⦄ ⊢ W ➡[h] W2 →
-     ∀n1,T1. ⦃G,L⦄ ⊢ ⓛ{p}W.T ➡[n1,h] T1 → ⓛ{p}W.T ≛[h,o] T1 →
-     ∀n2,T2. ⦃G,L.ⓛW⦄ ⊢ T ➡[n2,h] T2 →
-     ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → L ≛[h,o,ⓐV.ⓛ{p}W.T] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
-     ∃∃T. ⦃G,L1⦄ ⊢ ⓐV.T1 ➡[n2-n1,h] T & ⦃G,L2⦄ ⊢ ⓓ{p}ⓝW2.V2.T2 ➡[n1-n2,h] T & ⓓ{p}ⓝW2.V2.T2 ≛[h,o] T.
-#a #h #o #p #G0 #L0 #V0 #W0 #T0 #IH #H0
-#V2 #HV02 #W2 #HW02 #n1 #X #H1X #H2X #n2 #T2 #HT02
-#L1 #H1L01 #H2L01 #L2 #HL02
-elim (cnv_inv_appl … H0) -H0 #n0 #p0 #X01 #X02 #_ #HV0 #H0 #_ #_ -n0 -p0 -X01 -X02
-elim (cnv_inv_bind … H0) -H0 #HW0 #HT0
-elim (cpm_inv_abst1 … H1X) -H1X #W1 #T1 #H1W01 #H1T01 #H destruct
-elim (tdeq_inv_pair … H2X) -H2X #_ #H2W01 #H2T01
-elim (rdeq_inv_flat … H2L01) -H2L01 #H0L01 #H2L01
-elim (rdeq_inv_bind … H2L01) -H2L01 #H3L01 #H2L01
-elim (IH … V0 … 0 V0 … HV02 … H1L01 H0L01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
--HV0 -HV02 -H0L01 <minus_n_O #V #HV1 #H1V2 #H2V2
-elim (IH … H1W01 H2W01 … HW02 … H1L01 H3L01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
--HW0 <minus_n_O #W #HW1 #H1W2 #H2W2
-elim (IH … H1T01 H2T01 … HT02 (L1.ⓛW1) … (L2.ⓛW2))
-[|*: /3 width=2 by fqup_fpbg, lpr_pair, rdeq_bind_repl_dx, ext2_pair/ ]
-#T #HT1 #H1T2 #H2T02 -L0 -W0 -T0
-lapply (lsubr_cpm_trans … H1T2 (L2.ⓓⓝW2.V2) ?) -H1T2 [ /2 width=1 by lsubr_beta/ ] #H1T2
-/4 width=6 by cpm_beta, cpm_cast, cpm_bind, tdeq_pair, ex3_intro/
-qed-.
-
-fact cnv_cpm_tdeq1_conf_lpr_appl_theta_aux (a) (h) (o) (p) (G) (L) (V) (W) (T):
-     (∀G0,L0,T0. ⦃G,L,ⓐV.ⓓ{p}W.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpm_tdeq1_conf_lpr a h o G0 L0 T0) →
-     ⦃G,L⦄ ⊢ ⓐV.ⓓ{p}W.T ![a,h] →
-     ∀V2. ⦃G,L⦄ ⊢ V ➡[h] V2 → ∀W2. ⦃G,L⦄ ⊢ W ➡[h] W2 →
-     ∀n1,T1. ⦃G,L⦄ ⊢ ⓓ{p}W.T ➡[n1,h] T1 → ⓓ{p}W.T ≛[h,o] T1 →
-     ∀n2,T2. ⦃G,L.ⓓW⦄ ⊢ T ➡[n2,h] T2 → ∀U2. ⬆*[1]V2 ≘ U2 →
-     ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → L ≛[h,o,ⓐV.ⓓ{p}W.T] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
-     ∃∃T. ⦃G,L1⦄ ⊢ ⓐV.T1 ➡[n2-n1,h] T & ⦃G,L2⦄ ⊢ ⓓ{p}W2.ⓐU2.T2 ➡[n1-n2,h] T & ⓓ{p}W2.ⓐU2.T2 ≛[h,o] T.
-#a #h #o #p #G0 #L0 #V0 #W0 #T0 #IH #H0
-#V2 #HV02 #W2 #HW02 #n1 #X #H1X #H2X #n2 #T2 #HT02 #U2 #HVU2
-#L1 #H1L01 #H2L01 #L2 #HL02
-elim (cnv_inv_appl … H0) -H0 #n0 #p0 #X01 #X02 #_ #HV0 #H0 #_ #_ -n0 -p0 -X01 -X02
-elim (cpm_tdeq_inv_bind_sn … H0 … H1X H2X) -H0 -H1X -H2X #T1 #HW0 #HT0 #H1T01 #H2T01 #H destruct
-elim (rdeq_inv_flat … H2L01) -H2L01 #H0L01 #H2L01
-elim (rdeq_inv_bind … H2L01) -H2L01 #H3L01 #H2L01
-elim (IH … V0 … 0 V0 … HV02 … H1L01 H0L01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
--HV0 -HV02 -H0L01 <minus_n_O #V #HV1 #H1V2 #H2V2
-elim (IH … W0 … 0 W0 … HW02 … H1L01 H3L01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
--HW0 <minus_n_O #W #HW1 #H1W2 #H2W2
-elim (IH … H1T01 H2T01 … HT02 (L1.ⓓW0) … (L2.ⓓW2))
-[|*: /3 width=2 by fqup_fpbg, lpr_bind_refl_dx, lpr_bind, ext2_pair/ ]
-#T #HT1 #H1T2 #H2T02 -L0 -T0
-elim (cpm_lifts_sn … H1V2 (Ⓣ) … (L2.ⓓW2) … HVU2) -H1V2
-[| /3 width=1 by drops_refl, drops_drop/ ] #U #HVU #H1U2
-lapply (tdeq_lifts_bi … H2V2 … HVU2 … HVU) -H2V2 #H2U2
-/4 width=8 by cpm_theta, cpm_appl, cpm_bind, tdeq_pair, ex3_intro/
-qed-.
-
-fact cnv_cpm_tdeq1_conf_lpr_cast_cast_aux (a) (h) (o) (G) (L) (V) (T):
-     (∀G0,L0,T0. ⦃G,L,ⓝV.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpm_tdeq1_conf_lpr a h o G0 L0 T0) →
-     ⦃G,L⦄ ⊢ ⓝV.T ![a,h] →
-     ∀n1,V1. ⦃G,L⦄ ⊢ V ➡[n1,h] V1 → V ≛[h,o] V1 →
-     ∀n2,V2. ⦃G,L⦄ ⊢ V ➡[n2,h] V2 →
-     ∀T1. ⦃G,L⦄ ⊢ T ➡[n1,h] T1 → T ≛[h,o] T1 →
-     ∀T2. ⦃G,L⦄ ⊢ T ➡[n2,h] T2 →
-     ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → L ≛[h,o,ⓝV.T] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
-     ∃∃T. ⦃G,L1⦄ ⊢ ⓝV1.T1 ➡[n2-n1,h] T & ⦃G,L2⦄ ⊢ ⓝV2.T2 ➡[n1-n2,h] T & ⓝV2.T2≛[h,o]T.
-#a #h #o #G0 #L0 #V0 #T0 #IH #H0
-#n1 #V1 #H1V01 #H2V01 #n2 #V2 #HV02 #T1 #H1T01 #H2T01 #T2 #HT02
-#L1 #H1L01 #H2L01 #L2 #HL02
-elim (cnv_inv_cast … H0) -H0 #X0 #HV0 #HT0 #_ #_ -X0
-elim (rdeq_inv_flat … H2L01) -H2L01 #H0L01 #H2L01
-elim (IH … H1V01 H2V01 … HV02 … H1L01 H0L01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
-elim (IH … H1T01 H2T01 … HT02 … H1L01 H2L01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
-#T #HT1 #H1T2 #H2T2 #V #HV1 #H1V2 #H2V2 -L0 -V0 -T0
-/3 width=6 by cpm_cast, tdeq_pair, ex3_intro/
-qed-.
-(*
-fact cnv_cpm_tdeq1_conf_lpr_cast_epsilon_aux (a) (h) (o) (G) (L) (V) (T):
-     (∀G0,L0,T0. ⦃G,L,ⓝV.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpm_tdeq1_conf_lpr a h o G0 L0 T0) →
-     ⦃G,L⦄ ⊢ ⓝV.T ![a,h] →
-     ∀n1,V1. ⦃G,L⦄ ⊢ V ➡[n1,h] V1 → V ≛[h,o] V1 →
-     ∀T1. ⦃G,L⦄ ⊢ T ➡[n1,h] T1 → T ≛[h,o] T1 → 
-     ∀n2,T2. ⦃G,L⦄ ⊢ T ➡[n2,h] T2 →
-     ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → L ≛[h,o,ⓝV.T] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
-     ∃∃T. ⦃G,L1⦄ ⊢ ⓝV1.T1 ➡[n2-n1,h] T & ⦃G,L2⦄ ⊢ T2 ➡[n1-n2,h] T & T2 ≛[h,o] T.
-#a #h #o #G0 #L0 #V0 #T0 #IH #H0
-#n1 #V1 #HV01 #T1 #HT01 #n2 #T2 #HT02
-#L1 #HL01 #L2 #HL02
-elim (cnv_inv_cast … H0) -H0 #X0 #HV0 #HT0 #_ #_ -X0
-elim (cnv_cpm_conf_lpr_sub … IH … HT01 … HT02 … HL01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
-#T #HT1 #HT2 -L0 -V0 -T0
-/3 width=3 by cpms_eps, ex2_intro/
-qed-.
-*)
-fact cnv_cpm_tdeq1_conf_lpr_cast_ee_aux (a) (h) (o) (G) (L) (V) (T):
-     (∀G0,L0,T0. ⦃G,L,ⓝV.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpm_trans_lpr a h G0 L0 T0) →
-     (∀G0,L0,T0. ⦃G,L,ⓝV.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpm_tdeq1_conf_lpr a h o G0 L0 T0) →
-     ⦃G,L⦄ ⊢ ⓝV.T ![a,h] →
-     ∀n1,V1. ⦃G,L⦄ ⊢ V ➡[n1,h] V1 → V ≛[h,o] V1 →
-     ∀n2,V2. ⦃G,L⦄ ⊢ V ➡[n2,h] V2 →
-     ∀T1. ⦃G,L⦄ ⊢ T ➡[n1,h] T1 → T ≛[h,o]T1 →
-     ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → L ≛[h,o,ⓝV.T]L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
-     ∃∃T. ⦃G,L1⦄ ⊢ ⓝV1.T1 ➡[↑n2-n1,h] T & ⦃G,L2⦄ ⊢ V2 ➡[n1-↑n2,h] T & V2 ≛[h,o] T.
-#a #h #o #G0 #L0 #V0 #T0 #IH2 #IH1 #H0
-#n1 #V1 #H1V01 #H2V01 #n2 #V2 #HV02 #T1 #H1T01 #H2T01
-#L1 #H1L01 #H2L01 #L2 #HL02
-(* n2=0 n1=1 *)
- -H1V01 -H2V01
-elim (cnv_inv_cast … H0) -H0 #X0 #HV0 #HT0 #HVX0 #HTX0
-elim (rdeq_inv_flat … H2L01) -H2L01 #H0L01 #H2L01
-lapply (cnv_cpms_trans_lpr_sub … IH2 … HVX0 … L0 ?) [4:|*: /2 width=1 by fqup_fpbg/ ] #HX0
-elim (cnv_cpms_strip_lpr_sub … IH1 … HVX0 … HV02 … L0 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
-elim (cnv_cpms_strip_lpr_sub … IH1 … HTX0 … HT01 … L0 … HL01) [|*: /2 width=1 by fqup_fpbg/ ]
--HV02 -HTX0 -HT01 <minus_O_n <minus_n_O #T #HT2 #HT1 #V #HV1 #HV2
-elim (IH1 … HV1 … HT2 … HL02 … HL01) [|*: /2 width=4 by fqup_cpms_fwd_fpbg/ ]
--L0 -V0 -T0 -X0 #U #HVU #HTU
-lapply (cpms_trans … HV2 … HVU) -V <plus_O_n >minus_plus #H2
-lapply (cpms_trans … HT1 … HTU) -T <arith_l2 #H1
-/3 width=3 by cpms_eps, ex2_intro/
-qed-.
-
-fact cnv_cpm_tdeq1_conf_lpr_aux (a) (h) (o):
-                                ∀G0,L0,T0.
-                                (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_trans_lpr a h G1 L1 T1) →
-                                (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_tdeq1_conf_lpr a h o G1 L1 T1) →
-                                ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_cnv_cpm_tdeq1_conf_lpr a h o G1 L1 T1.
-#a #h #o #G0 #L0 #T0 #IH2 #IH1 #G #L * [| * [| * ]]
-[ #I #HG0 #HL0 #HT0 #HT #n1 #X1 #H1X1 #H2X1 #n2 #X2 #HX2 #L1 #H1L1 #H2L1 #L2 #HL2 destruct
-  elim (cpm_tdeq_inv_atom_sn … H1X1 H2X1) -H1X1 -H2X1 *
-  elim (cpm_inv_atom1_drops … HX2) -HX2 *
-  [ #H21 #H22 #H11 #H12 destruct -a -L
-    <minus_O_n
-    /2 width=1 by cnv_cpm_tdeq1_conf_lpr_atom_atom_aux/
-  | #s2 #H21 #H22 #H23 #H11 #H12 destruct -a -L
-    <minus_O_n <minus_n_O
-    /2 width=1 by cnv_cpm_tdeq1_conf_lpr_atom_ess_aux/
-  | #K2 #V2 #XV2 #i #HLK2 #HVX2 #HXV2 #H21 #H11 #H12 destruct -IH2
-    <minus_O_n <minus_n_O
-    @(cnv_cpm_tdeq1_conf_lpr_atom_delta_aux … IH1) -IH1 /1 width=6 by/
-  | #m2 #K2 #W2 #XW2 #i #HLK2 #HWX2 #HXW2 #H21 #H22 #H11 #H12 destruct -IH2
-    <minus_O_n <minus_n_O
-    @(cnv_cpm_tdeq1_conf_lpr_atom_ell_aux … IH1) -IH1 /1 width=6 by/
-  | #H21 #H22 #s1 #H11 #H12 #H13 #H14 destruct -a -L
-    <minus_O_n <minus_n_O
-    /2 width=1 by cnv_cpm_tdeq1_conf_lpr_ess_atom_aux/
-  | #s2 #H21 #H22 #H23 #s1 #H11 #H12 #H13 #_ destruct -a -L
-    <minus_n_n
-    /2 width=1 by cnv_cpm_tdeq1_conf_lpr_atom_atom_aux/
-  | #K2 #V2 #XV2 #i2 #_ #_ #_ #H21 #s1 #H11 #H12 #H13 #_ destruct
-  | #m2 #K2 #W2 #XW2 #i2 #_ #_ #_ #H21 #H22 #s1 #H11 #H12 #H13 #_ destruct
-  ]
-| #p #I #V #T #HG0 #HL0 #HT0 #HT #n1 #X1 #H1X1 #H2X1 #n2 #X2 #HX2 #L1 #H1L1 #H2L1 #L2 #HL2 destruct
-  elim (cpm_tdeq_inv_bind_sn … HT … H1X1 H2X1) -H1X1 -H2X1
-  elim (cpm_inv_bind1 … HX2) -HX2 *
-  [ #V2 #T2 #HV2 #HT2 #H21 #T1 #_ #_ #H1T1 #H2T1 #H11 destruct -IH2
-    @(cnv_cpm_tdeq1_conf_lpr_bind_bind_aux … IH1) -IH1 /1 width=1 by/
-  | #T2 #HT2 #HTX2 #H21 #H22 #T1 #_ #_ #H1T1 #H2T1 #H11 destruct -IH2
-    @(cnv_cpm_tdeq1_conf_lpr_bind_zeta_aux … IH1) -IH1 /1 width=3 by/
-  ]
-| #V #T #HG0 #HL0 #HT0 #HT #n1 #X1 #H1X1 #H2X1 #n2 #X2 #HX2 #L1 #H1L1 #H2L1 #L2 #HL2 destruct
-  elim (cpm_tdeq_inv_appl_sn … HT … H1X1 H2X1) -H1X1 -H2X1
-  elim (cpm_inv_appl1 … HX2) -HX2 *
-  [ #V2 #T2 #HV2 #HT2 #H21 #m #q #W1 #U1 #T1 #_ #_ #_ #_ #_ #H1T1 #H2T1 #H11 destruct -IH2 -m -q -W1 -U1
-    @(cnv_cpm_tdeq1_conf_lpr_appl_appl_aux … IH1) -IH1 /1 width=1 by/
-  | #p2 #V2 #XW2 #W2 #XT2 #T2 #HV2 #HW2 #HT2 #H21 #H22 #m #q #W1 #U1 #T1 #_ #_ #_ #_ #_ #H1T1 #H2T1 #H11 destruct -IH2 -m -q -W1 -U1
-    @(cnv_cpm_tdeq1_conf_lpr_appl_beta_aux … IH1) -IH1 /1 width=1 by/
-  | #p2 #V2 #XV2 #XW2 #W2 #XT2 #T2 #HV2 #HXV2 #HW2 #HT2 #H21 #H22 #m #q #W1 #U1 #T1 #_ #_ #_ #_ #_ #H1T1 #H2T1 #H11 destruct -IH2 -m -q -W1 -U1
-    @(cnv_cpm_tdeq1_conf_lpr_appl_theta_aux … IH1) -IH1 /1 width=3 by/
-  ]
-| #V #T #HG0 #HL0 #HT0 #HT #n1 #X1 #H1X1 #H2X1 #n2 #X2 #HX2 #L1 #H1L1 #H2L1 #L2 #HL2 destruct
-  elim (cpm_tdeq_inv_cast_sn … HT … H1X1 H2X1) -H1X1 -H2X1
-  elim (cpm_inv_cast1 … HX2) -HX2 [ * || * ]
-  [ #V2 #T2 #HV2 #HT2 #H21 #U1 #V1 #T1 #_ #_ #_ #H1V1 #H2V1 #_ #H1T1 #H2T1 #H11 destruct -IH2 -U1
-    @(cnv_cpm_tdeq1_conf_lpr_cast_cast_aux … IH1) -IH1 /1 width=1 by/
-  | #HT2 #U1 #V1 #T1 #_ #_ #_ #H1V1 #H2V1 #_ #H1T1 #H2T1 #H11 destruct -IH2 -U1
-(*    @(cnv_cpm_tdeq1_conf_lpr_cast_epsilon_aux … IH1) -IH1 /1 width=1 by/ *)
-  | #m2 #HV2 #H21 #U1 #V1 #T1 #_ #_ #_ #H1V1 #H2V1 #_ #H1T1 #H2T1 #H11 destruct -U1
-    @(cnv_cpm_tdeq1_conf_lpr_cast_ee_aux … IH2 IH1) -IH2 -IH1 /1 width=1 by/
-  ]
-]
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cnv/cnv_cpms_tdeq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cnv/cnv_cpms_tdeq.etc
deleted file mode 100644
index da155423c..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/cnv/cnv_cpms_tdeq.etc
+++ /dev/null
@@ -1,52 +0,0 @@
-(*
-axiom cpms_tdneq_fwd_step_sn (n) (h) (o) (G) (L):
-                             ∀T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[n,h] T2 → (T1 ≛[h,o] T2 → ⊥) →
-                             ∃∃n1,n2,T,T0. ⦃G, L⦄ ⊢ T1 ➡[n1,h] T & T1 ≛[h,o] T → ⊥ & ⦃G, L⦄ ⊢ T ➡*[n2,h] T0 & T0 ≛[h,o] T2 & n1+n2 = n.
-axiom plus_Sxy_y_false: ∀y,x. ↑(x+y) = y → ⊥.
-
-lemma cnv_cpm_tdeq_trans (a) (h) (o) (G) (L):
-                         ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] →
-                         ∀n,T2.  ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 → T1 ≛[h,o] T2 → ⦃G,L⦄ ⊢ T2 ![a,h].
-#a #h #o #G #L #T1 @(fqup_wf_ind_eq (Ⓣ) … G L T1) -G -L -T1
-#G0 #L0 #T0 #IH #G #L * [| * [| * ]]
-[ #I #_ #_ #_ #H0 #n #X #H1X #H2X -G0 -L0 -T0
-  elim (cpm_tdeq_inv_atom_sn … H1X H2X) -H1X -H2X *
-  [ #H #_ destruct //
-  | #s #H #_ #_ #_ destruct //
-  ]
-| #p #I #V1 #T1 #HG #HL #HT #H0 #n #X #H1X #H2X destruct
-  elim (cnv_inv_bind … H0) #HV1 #_
-  elim (cpm_tdeq_inv_bind_sn … H0 … H1X H2X) -H0 -H1X -H2X #T2 #H1T #H2T #H3T #H destruct
-  /3 width=6 by cnv_bind/
-| #V1 #T1 #HG #HL #HT #H0 #n #X #H1X #H2X destruct
-  elim (cnv_inv_appl … H0) #m #p #W1 #U1 #Hm #HV1 #_ #HVW1 #HTU1
-  elim (cpm_tdeq_inv_appl_sn … H0 … H1X H2X) -H0 -H1X -H2X #T2 #H1T #H2T #H3T #H destruct
-  @(cnv_appl … Hm … HVW1)
-
-(* Properties with restricted rt-transition for terms ***********************)
-
-lemma pippo (a) (h) (o) (G) (L):
-            ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] →
-            ∀n1,T.  ⦃G,L⦄ ⊢ T1 ➡[n1,h] T → T1 ≛[h,o] T →
-            ∀n2,T2. ⦃G,L⦄ ⊢ T ➡[n2,h] T2 →
-            ∃∃T0. ⦃G,L⦄ ⊢ T1 ➡[n2,h] T0 & ⦃G,L⦄ ⊢ T0 ➡[n1,h] T2 & T0 ≛[h,o] T2.
-#a #h #o #G #L #T1 @(fqup_wf_ind_eq (Ⓣ) … G L T1) -G -L -T1
-#G0 #L0 #T0 #IH #G #L * [| * [| * ]]
-[ #I #_ #_ #_ #_ #n1 #X1 #H1X #H2X #n2 #X2 #HX2 -G0 -L0 -T0
-  elim (cpm_tdeq_inv_atom_sn … H1X H2X) -H1X -H2X *
-  [ #H1 #H2 destruct /2 width=4 by ex3_intro/
-  | #s #H1 #H2 #H3 #Hs destruct
-    elim (cpm_inv_sort1 … HX2) -HX2 #H #Hn2 destruct >iter_n_Sm
-    /5 width=6 by cpm_sort_iter, tdeq_sort, deg_iter, deg_next, ex3_intro/
-  ]
-| #p #I #V1 #T1 #HG #HL #HT #H0 #n1 #X1 #H1X #H2X #n2 #X2 #HX2 destruct
-  elim (cpm_tdeq_inv_bind_sn … H0 … H1X H2X) -H0 -H1X -H2X #T #H1T1 #H2T1 #H3T1 #H destruct
-  elim (cpm_inv_bind1 … HX2) -HX2 *
-  [ #V2 #T2 #HV12 #HT2 #H destruct
-    elim (IH … H1T1 … H2T1 H3T1 … HT2) -IH -H1T1 -H2T1 -H3T1 -HT2 [2: // ] #T0 #HT10 #H1T02 #H2T02
-    @(ex3_intro … (ⓑ{p,I}V2.T0))
-    [ /2 width=1 by cpm_bind/
-    | 
-    | /2 width=1 by tdeq_pair/
-
-*)
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 e10340776..e34970bbe 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
@@ -31,7 +31,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_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpm_tdeq" + "cnv_cpm_tfeq_trans" + "cnv_cpms_tdeq" + "cnv_cpms_conf" + "cnv_preserve_sub" + "cnv_preserve" * ]
+             [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "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_preserve_sub" + "cnv_preserve" * ]
           }
         ]
      }
diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa/ex_4_1_props.ma b/matita/matita/contribs/lambdadelta/ground_2/xoa/ex_4_1_props.ma
new file mode 100644
index 000000000..fe081386b
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground_2/xoa/ex_4_1_props.ma
@@ -0,0 +1,22 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "ground_2/xoa/xoa.ma".
+
+(* Properties with multiple existental quantifier (5, 1) ********************)
+
+lemma ex4_commute (A0) (P0,P1,P2,P3:A0→Prop):
+                  (∃∃x0. P0 x0 & P1 x0 & P2 x0 & P3 x0) → ∃∃x0. P2 x0 & P3 x0 & P0 x0 & P1 x0.
+#A0 #P0 #P1 #P2 #P3 * /2 width=5 by ex4_intro/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/static_2/notation/relations/positive_3.ma b/matita/matita/contribs/lambdadelta/static_2/notation/relations/positive_3.ma
deleted file mode 100644
index e73de4930..000000000
--- a/matita/matita/contribs/lambdadelta/static_2/notation/relations/positive_3.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 h, term 46 o ] ⦃ term 46 T ⦄ )"
-   non associative with precedence 45
-   for @{ 'Positive $h $o $T }.
diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/tdpos.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/tdpos.ma
deleted file mode 100644
index 1b6b1197e..000000000
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/tdpos.ma
+++ /dev/null
@@ -1,63 +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 "static_2/notation/relations/positive_3.ma".
-include "static_2/syntax/item_sd.ma".
-include "static_2/syntax/term.ma".
-
-(* DEGREE POSITIVITY ON TERMS ***********************************************)
-
-inductive tdpos (h) (o): predicate term ≝
-| tdpos_sort: ∀s,d. deg h o s (↑d) → tdpos h o (⋆s)
-| tdpos_lref: ∀i. tdpos h o (#i)
-| tdpos_gref: ∀l. tdpos h o (§l)
-| tdpos_pair: ∀I,V,T. tdpos h o V → tdpos h o T → tdpos h o (②{I}V.T)
-.
-
-interpretation
-   "context-free degree positivity (term)"
-   'Positive h o T = (tdpos h o T).
-
-(* Basic inversion lemmas ***************************************************)
-
-fact tdpos_inv_sort_aux (h) (o): 
-                        ∀X. 𝐏[h,o]⦃X⦄ → ∀s. X = ⋆s → ∃d. deg h o s (↑d).
-#h #o #H *
-[ #s #d #Hsd #x #H destruct /2 width=2 by ex_intro/
-| #i #x #H destruct
-| #l #x #H destruct
-| #I #V #T #_ #_ #x #H destruct
-]
-qed-.
-
-lemma tdpos_inv_sort (h) (o): ∀s. 𝐏[h,o]⦃⋆s⦄ → ∃d. deg h o s (↑d).
-/2 width=3 by tdpos_inv_sort_aux/ qed-.
-
-fact tdpos_inv_pair_aux (h) (o): ∀X. 𝐏[h,o]⦃X⦄ → ∀I,V,T. X = ②{I}V.T →
-                                 ∧∧ 𝐏[h,o]⦃V⦄ & 𝐏[h,o]⦃T⦄.
-#h #o #H *
-[ #s #d #_ #Z #X1 #X2 #H destruct
-| #i #Z #X1 #X2 #H destruct
-| #l #Z #X1 #X2 #H destruct
-| #I #V #T #HV #HT #Z #X1 #X2 #H destruct /2 width=1 by conj/
-]
-qed-.
-
-lemma tdpos_inv_pair (h) (o): ∀I,V,T. 𝐏[h,o]⦃②{I}V.T⦄ →
-                              ∧∧ 𝐏[h,o]⦃V⦄ & 𝐏[h,o]⦃T⦄.
-/2 width=4 by tdpos_inv_pair_aux/ qed-.
-
-(* Basic properties *********************************************************)
-
-axiom tdpos_total (h): ∀T. ∃o. 𝐏[h,o]⦃T⦄.