From: Ferruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
Date: Fri, 15 Nov 2019 15:22:29 +0000 (+0100)
Subject: update in static_2 and basic_2 for the article
X-Git-Tag: make_still_working~220
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f677b4ef7fa20f1ab36c5ee59598865d5c1b719b;p=helm.git

update in static_2 and basic_2 for the article

+ commented theorems activated or parked
+ some renaming to match the article
---

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cnuw_simple.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cnuw_simple.etc
new file mode 100644
index 000000000..5b63e8d6d
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cnuw_simple.etc
@@ -0,0 +1,7 @@
+(* Advanced forward lemma with with simple terms ****************************)
+(*
+lemma cnuw_fwd_appl_simple (h) (G) (L):
+      ∀V,T. ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] ⓐV.T → 𝐒⦃T⦄.
+#h #G #L #V #T #HT
+elim (simple_dec_ex T) [ // ] * #p #I #W #U #H destruct
+*)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpx_req.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpx_req.etc
new file mode 100644
index 000000000..8b0fdeb69
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpx_req.etc
@@ -0,0 +1,13 @@
+(* req_req is missing, with req_sym *)
+
+(* Basic_2A1: was: cpx_lleq_conf *)
+lemma cpx_req_conf (h) (G):
+      ∀L2,T1,T2. ⦃G,L2⦄ ⊢ T1 ⬈[h] T2 →
+      ∀L1. L2 ≡[T1] L1 → ⦃G,L1⦄ ⊢ T1 ⬈[h] T2.
+/3 width=3 by req_cpx_trans, req_sym/ qed-.
+
+(* Basic_2A1: was: cpx_lleq_conf_dx *)
+lemma cpx_req_conf_dx (h) (G):
+      ∀L2,T1,T2. ⦃G,L2⦄ ⊢ T1 ⬈[h] T2 →
+      ∀L1. L1 ≡[T1] L2 → L1 ≡[T2] L2.
+/4 width=6 by cpx_req_conf_sn, req_sym/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/ntas_nta.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/ntas_nta.etc
new file mode 100644
index 000000000..3bfa93807
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/ntas_nta.etc
@@ -0,0 +1,11 @@
+lapply (nta_ntas … H) -H #H
+elim (ntas_inv_appl_sn … H) -H * #n #p #W #U #U0 #Hn #Ha #HVW #HTU #HU #HUX #HX
+[ elim (eq_or_gt n) #H destruct
+  [ <minus_n_O in HU; #HU -Hn
+    /4 width=8 by ntas_inv_nta, ex6_4_intro, or_introl/
+  | lapply (le_to_le_to_eq … Hn H) -Hn -H #H destruct
+    <minus_n_n in HU; #HU
+    @or_intror
+    @(ex6_5_intro … Ha … HUX HX) -Ha -X
+    [2,4: /2 width=2 by ntas_inv_nta/
+    |6: @ntas_refl
diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_nta.ma b/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_nta.ma
index 865de8042..c7fd9cb26 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_nta.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_nta.ma
@@ -99,19 +99,7 @@ lemma nta_inv_appl_sn_ntas (h) (a) (G) (L) (V) (T):
       ∨∨ ∃∃p,W,U,U0. ad a 0 & ⦃G,L⦄ ⊢ V :[h,a] W & ⦃G,L⦄ ⊢ T :*[h,a,0] ⓛ{p}W.U0 & ⦃G,L.ⓛW⦄ ⊢ U0 :[h,a] U & ⦃G,L⦄ ⊢ ⓐV.ⓛ{p}W.U ⬌*[h] X & ⦃G,L⦄ ⊢ X ![h,a]
        | ∃∃n,p,W,U,U0. ad a (↑n) & ⦃G,L⦄ ⊢ V :[h,a] W & ⦃G,L⦄ ⊢ T :[h,a] U & ⦃G,L⦄ ⊢ U :*[h,a,n] ⓛ{p}W.U0 & ⦃G,L⦄ ⊢ ⓐV.U ⬌*[h] X & ⦃G,L⦄ ⊢ X ![h,a].
 #h #a #G #L #V #T #X #H
-(*
-lapply (nta_ntas … H) -H #H
-elim (ntas_inv_appl_sn … H) -H * #n #p #W #U #U0 #Hn #Ha #HVW #HTU #HU #HUX #HX
-[ elim (eq_or_gt n) #H destruct
-  [ <minus_n_O in HU; #HU -Hn
-    /4 width=8 by ntas_inv_nta, ex6_4_intro, or_introl/
-  | lapply (le_to_le_to_eq … Hn H) -Hn -H #H destruct
-    <minus_n_n in HU; #HU
-    @or_intror
-    @(ex6_5_intro … Ha … HUX HX) -Ha -X
-    [2,4: /2 width=2 by ntas_inv_nta/
-    |6: @ntas_refl
-*)
+(* Note: insert here: alternate proof in ntas_nta.etc *)
 elim (cnv_inv_cast … H) -H #X0 #HX #HVT #HX0 #HTX0
 elim (cnv_inv_appl … HVT) #n #p #W #U0 #Ha #HV #HT #HVW #HTU0
 elim (eq_or_gt n) #Hn destruct
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw_simple.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw_simple.ma
index d32e1b1d6..2e193c21f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw_simple.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw_simple.ma
@@ -18,13 +18,6 @@ include "basic_2/rt_computation/cnuw.ma".
 
 (* NORMAL TERMS FOR T-UNUNBOUND WHD RT-TRANSITION ***************************)
 
-(* Advanced forward lemma with with simple terms ****************************)
-(*
-lemma cnuw_fwd_appl_simple (h) (G) (L):
-      ∀V,T. ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] ⓐV.T → 𝐒⦃T⦄.
-#h #G #L #V #T #HT
-elim (simple_dec_ex T) [ // ] * #p #I #W #U #H destruct
-*)
 (* Advanced properties with simple terms ************************************)
 
 lemma cnuw_appl_simple (h) (G) (L):
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqo.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqo.ma
new file mode 100644
index 000000000..1de400dad
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqo.ma
@@ -0,0 +1,102 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/teqo_tdeq.ma".
+include "basic_2/rt_computation/cpxs_lsubr.ma".
+include "basic_2/rt_computation/cpxs_cnx.ma".
+include "basic_2/rt_computation/lpxs_cpxs.ma".
+
+(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
+
+(* Forward lemmas with sort-irrelevant outer equivalence for terms **********)
+
+lemma cpxs_fwd_sort (h) (G) (L):
+      ∀X2,s1. ⦃G,L⦄ ⊢ ⋆s1 ⬈*[h] X2 → ⋆s1 ⩳ X2.
+#h #G #L #X2 #s1 #H
+elim (cpxs_inv_sort1 … H) -H #s2 #H destruct //
+qed-.
+
+(* Note: probably this is an inversion lemma *)
+(* Basic_2A1: was: cpxs_fwd_delta *)
+lemma cpxs_fwd_delta_drops (h) (I) (G) (L) (K):
+      ∀V1,i. ⇩*[i] L ≘ K.ⓑ{I}V1 →
+      ∀V2. ⇧*[↑i] V1 ≘ V2 →
+      ∀X2. ⦃G,L⦄ ⊢ #i ⬈*[h] X2 →
+      ∨∨ #i ⩳ X2 | ⦃G,L⦄ ⊢ V2 ⬈*[h] X2.
+#h #I #G #L #K #V1 #i #HLK #V2 #HV12 #X2 #H
+elim (cpxs_inv_lref1_drops … H) -H /2 width=1 by or_introl/
+* #I0 #K0 #V0 #U0 #HLK0 #HVU0 #HU0
+lapply (drops_mono … HLK0 … HLK) -HLK0 #H destruct
+/4 width=9 by cpxs_lifts_bi, drops_isuni_fwd_drop2, or_intror/
+qed-.
+
+(* Basic_1: was just: pr3_iso_beta *)
+lemma cpxs_fwd_beta (h) (p) (G) (L):
+      ∀V,W,T,X2. ⦃G,L⦄ ⊢ ⓐV.ⓛ{p}W.T ⬈*[h] X2 →
+      ∨∨ ⓐV.ⓛ{p}W.T ⩳ X2 | ⦃G,L⦄ ⊢ ⓓ{p}ⓝW.V.T ⬈*[h] X2.
+#h #p #G #L #V #W #T #X2 #H elim (cpxs_inv_appl1 … H) -H *
+[ #V0 #T0 #_ #_ #H destruct /2 width=1 by teqo_pair, or_introl/
+| #b #W0 #T0 #HT0 #HU
+  elim (cpxs_inv_abst1 … HT0) -HT0 #W1 #T1 #HW1 #HT1 #H destruct
+  lapply (lsubr_cpxs_trans … HT1 (L.ⓓⓝW.V) ?) -HT1
+  /5 width=3 by cpxs_trans, cpxs_bind, cpxs_pair_sn, lsubr_beta, or_intror/
+| #b #V1 #V2 #V0 #T1 #_ #_ #HT1 #_
+  elim (cpxs_inv_abst1 … HT1) -HT1 #W2 #T2 #_ #_ #H destruct
+]
+qed-.
+
+lemma cpxs_fwd_theta (h) (p) (G) (L):
+           ∀V1,V,T,X2. ⦃G,L⦄ ⊢ ⓐV1.ⓓ{p}V.T ⬈*[h] X2 →
+           ∀V2. ⇧*[1] V1 ≘ V2 →
+           ∨∨ ⓐV1.ⓓ{p}V.T ⩳ X2 | ⦃G,L⦄ ⊢ ⓓ{p}V.ⓐV2.T ⬈*[h] X2.
+#h #p #G #L #V1 #V #T #X2 #H #V2 #HV12
+elim (cpxs_inv_appl1 … H) -H *
+[ -HV12 #V0 #T0 #_ #_ #H destruct /2 width=1 by teqo_pair, or_introl/
+| #q #W #T0 #HT0 #HU
+  elim (cpxs_inv_abbr1_dx … HT0) -HT0 *
+  [ #V3 #T3 #_ #_ #H destruct
+  | #X #HT2 #H #H0 destruct
+    elim (lifts_inv_bind1 … H) -H #W2 #T2 #HW2 #HT02 #H destruct
+    @or_intror @(cpxs_trans … HU) -X2 (**) (* explicit constructor *)
+    @(cpxs_trans … (+ⓓV.ⓐV2.ⓛ{q}W2.T2)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T
+    @(cpxs_strap2 … (ⓐV1.ⓛ{q}W.T0)) [2: /2 width=1 by cpxs_beta_dx/ ]
+    /4 width=7 by cpx_zeta, lifts_bind, lifts_flat/
+  ]
+| #q #V3 #V4 #V0 #T0 #HV13 #HV34 #HT0 #HU
+  @or_intror @(cpxs_trans … HU) -X2 (**) (* explicit constructor *)
+  elim (cpxs_inv_abbr1_dx … HT0) -HT0 *
+  [ #V5 #T5 #HV5 #HT5 #H destruct
+    /6 width=9 by cpxs_lifts_bi, drops_refl, drops_drop, cpxs_flat, cpxs_bind/
+  | #X #HT1 #H #H0 destruct
+    elim (lifts_inv_bind1 … H) -H #V5 #T5 #HV05 #HT05 #H destruct
+    lapply (cpxs_lifts_bi … HV13 (Ⓣ) … (L.ⓓV0) … HV12 … HV34) -V3 /3 width=1 by drops_refl, drops_drop/ #HV24
+    @(cpxs_trans … (+ⓓV.ⓐV2.ⓓ{q}V5.T5)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T
+    @(cpxs_strap2 … (ⓐV1.ⓓ{q}V0.T0)) [ /4 width=7 by cpx_zeta, lifts_bind, lifts_flat/ ] -V -V5 -T5
+    @(cpxs_strap2 … (ⓓ{q}V0.ⓐV2.T0)) /3 width=3 by cpxs_pair_sn, cpxs_bind_dx, cpx_theta/
+  ]
+]
+qed-.
+
+lemma cpxs_fwd_cast (h) (G) (L):
+      ∀W,T,X2. ⦃G,L⦄ ⊢ ⓝW.T ⬈*[h] X2 →
+      ∨∨ ⓝW. T ⩳ X2 | ⦃G,L⦄ ⊢ T ⬈*[h] X2 | ⦃G,L⦄ ⊢ W ⬈*[h] X2.
+#h #G #L #W #T #X2 #H
+elim (cpxs_inv_cast1 … H) -H /2 width=1 by or3_intro1, or3_intro2/ *
+#W0 #T0 #_ #_ #H destruct /2 width=1 by teqo_pair, or3_intro0/
+qed-.
+
+lemma cpxs_fwd_cnx (h) (G) (L):
+      ∀T1. ⦃G,L⦄ ⊢ ⬈[h] 𝐍⦃T1⦄ →
+      ∀X2. ⦃G,L⦄ ⊢ T1 ⬈*[h] X2 → T1 ⩳ X2.
+/3 width=5 by cpxs_inv_cnx1, tdeq_teqo/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqo_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqo_vector.ma
new file mode 100644
index 000000000..5b7135b01
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqo_vector.ma
@@ -0,0 +1,188 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/teqo_simple_vector.ma".
+include "static_2/relocation/lifts_vector.ma".
+include "basic_2/rt_computation/cpxs_teqo.ma".
+
+(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
+
+(* Vector form of forward lemmas with outer equivalence for terms ***********)
+
+lemma cpxs_fwd_sort_vector (h) (G) (L):
+      ∀s,Vs,X2. ⦃G,L⦄ ⊢ ⒶVs.⋆s ⬈*[h] X2 → ⒶVs.⋆s ⩳ X2.
+#h #G #L #s #Vs elim Vs -Vs /2 width=4 by cpxs_fwd_sort/
+#V #Vs #IHVs #X2 #H
+elim (cpxs_inv_appl1 … H) -H *
+[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1 by teqo_pair/
+| #p #W1 #T1 #HT1 #HU
+  lapply (IHVs … HT1) -IHVs -HT1 #HT1
+  elim (teqo_inv_applv_bind_simple … HT1) //
+| #p #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU
+  lapply (IHVs … HT1) -IHVs -HT1 #HT1
+  elim (teqo_inv_applv_bind_simple … HT1) //
+]
+qed-.
+
+(* Basic_2A1: was: cpxs_fwd_delta_vector *)
+lemma cpxs_fwd_delta_drops_vector (h) (I) (G) (L) (K):
+      ∀V1,i. ⇩*[i] L ≘ K.ⓑ{I}V1 →
+      ∀V2. ⇧*[↑i] V1 ≘ V2 →
+      ∀Vs,X2. ⦃G,L⦄ ⊢ ⒶVs.#i ⬈*[h] X2 →
+      ∨∨ ⒶVs.#i ⩳ X2 | ⦃G,L⦄ ⊢ ⒶVs.V2 ⬈*[h] X2.
+#h #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs
+elim Vs -Vs /2 width=5 by cpxs_fwd_delta_drops/
+#V #Vs #IHVs #X2 #H -K -V1
+elim (cpxs_inv_appl1 … H) -H *
+[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by teqo_pair, or_introl/
+| #q #W0 #T0 #HT0 #HU
+  elim (IHVs … HT0) -IHVs -HT0 #HT0
+  [ elim (teqo_inv_applv_bind_simple … HT0) //
+  | @or_intror -i (**) (* explicit constructor *)
+    @(cpxs_trans … HU) -X2
+    @(cpxs_strap1 … (ⓐV.ⓛ{q}W0.T0)) /3 width=1 by cpxs_flat_dx, cpx_beta/
+  ]
+| #q #V0 #V1 #V3 #T0 #HV0 #HV01 #HT0 #HU
+  elim (IHVs … HT0) -IHVs -HT0 #HT0
+  [ elim (teqo_inv_applv_bind_simple … HT0) //
+  | @or_intror -i (**) (* explicit constructor *)
+    @(cpxs_trans … HU) -X2
+    @(cpxs_strap1 … (ⓐV0.ⓓ{q}V3.T0)) /3 width=3 by cpxs_flat, cpx_theta/
+  ]
+]
+qed-.
+
+(* Basic_1: was just: pr3_iso_appls_beta *)
+lemma cpxs_fwd_beta_vector (h) (p) (G) (L):
+      ∀Vs,V,W,T,X2. ⦃G,L⦄ ⊢ ⒶVs.ⓐV.ⓛ{p}W.T ⬈*[h] X2 →
+      ∨∨ ⒶVs.ⓐV.ⓛ{p}W. T ⩳ X2 | ⦃G,L⦄ ⊢ ⒶVs.ⓓ{p}ⓝW.V.T ⬈*[h] X2.
+#h #p #G #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_beta/
+#V0 #Vs #IHVs #V #W #T #X2 #H
+elim (cpxs_inv_appl1 … H) -H *
+[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1 by teqo_pair, or_introl/
+| #q #W1 #T1 #HT1 #HU
+  elim (IHVs … HT1) -IHVs -HT1 #HT1
+  [ elim (teqo_inv_applv_bind_simple … HT1) //
+  | @or_intror (**) (* explicit constructor *)
+    @(cpxs_trans … HU) -X2
+    @(cpxs_strap1 … (ⓐV0.ⓛ{q}W1.T1)) /3 width=1 by cpxs_flat_dx, cpx_beta/
+  ]
+| #q #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU
+  elim (IHVs … HT1) -IHVs -HT1 #HT1
+  [ elim (teqo_inv_applv_bind_simple … HT1) //
+  | @or_intror (**) (* explicit constructor *)
+    @(cpxs_trans … HU) -X2
+    @(cpxs_strap1 … (ⓐV1.ⓓ{q}V3.T1)) /3 width=3 by cpxs_flat, cpx_theta/
+  ]
+]
+qed-.
+
+(* Basic_1: was just: pr3_iso_appls_abbr *)
+lemma cpxs_fwd_theta_vector (h) (G) (L):
+      ∀V1b,V2b. ⇧*[1] V1b ≘ V2b →
+      ∀p,V,T,X2. ⦃G,L⦄ ⊢ ⒶV1b.ⓓ{p}V.T ⬈*[h] X2 →
+      ∨∨ ⒶV1b.ⓓ{p}V.T ⩳ X2 | ⦃G,L⦄ ⊢ ⓓ{p}V.ⒶV2b.T ⬈*[h] X2.
+#h #G #L #V1b #V2b * -V1b -V2b /3 width=1 by or_intror/
+#V1b #V2b #V1a #V2a #HV12a #HV12b #p
+generalize in match HV12a; -HV12a
+generalize in match V2a; -V2a
+generalize in match V1a; -V1a
+elim HV12b -V1b -V2b /2 width=1 by cpxs_fwd_theta/
+#V1b #V2b #V1b #V2b #HV12b #_ #IHV12b #V1a #V2a #HV12a #V #T #X2 #H
+elim (cpxs_inv_appl1 … H) -H *
+[ -IHV12b -HV12a -HV12b #V0 #T0 #_ #_ #H destruct /2 width=1 by teqo_pair, or_introl/
+| #q #W0 #T0 #HT0 #HU
+  elim (IHV12b … HV12b … HT0) -IHV12b -HT0 #HT0
+  [ -HV12a -HV12b -HU
+    elim (teqo_inv_pair1 … HT0) #V1 #T1 #H destruct
+  | @or_intror -V1b (**) (* explicit constructor *)
+    @(cpxs_trans … HU) -X2
+    elim (cpxs_inv_abbr1_dx … HT0) -HT0 *
+    [ -HV12a #V1 #T1 #_ #_ #H destruct
+    | -V1b #X #HT1 #H #H0 destruct
+      elim (lifts_inv_bind1 … H) -H #W1 #T1 #HW01 #HT01 #H destruct
+      @(cpxs_trans … (+ⓓV.ⓐV2a.ⓛ{q}W1.T1)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T -V2b -V2b
+      @(cpxs_strap2 … (ⓐV1a.ⓛ{q}W0.T0))
+      /4 width=7 by cpxs_beta_dx, cpx_zeta, lifts_bind, lifts_flat/
+    ]
+  ]
+| #q #V0a #Va #V0 #T0 #HV10a #HV0a #HT0 #HU
+  elim (IHV12b … HV12b … HT0) -HV12b -IHV12b -HT0 #HT0
+  [ -HV12a -HV10a -HV0a -HU
+    elim (teqo_inv_pair1 … HT0) #V1 #T1 #H destruct
+  | @or_intror -V1b -V1b (**) (* explicit constructor *)
+    @(cpxs_trans … HU) -X2
+    elim (cpxs_inv_abbr1_dx … HT0) -HT0 *
+    [ #V1 #T1 #HV1 #HT1 #H destruct
+      lapply (cpxs_lifts_bi … HV10a (Ⓣ) … (L.ⓓV) … HV12a … HV0a) -V1a -V0a /3 width=1 by drops_refl, drops_drop/ #HV2a
+      @(cpxs_trans … (ⓓ{p}V.ⓐV2a.T1)) /3 width=1 by cpxs_bind, cpxs_pair_sn, cpxs_flat_dx, cpxs_bind_dx/
+    | #X #HT1 #H #H0 destruct
+      elim (lifts_inv_bind1 … H) -H #V1 #T1 #HW01 #HT01 #H destruct
+      lapply (cpxs_lifts_bi … HV10a (Ⓣ) … (L.ⓓV0) … HV12a … HV0a) -V0a /3 width=1 by drops_refl, drops_drop/ #HV2a
+      @(cpxs_trans … (+ⓓV.ⓐV2a.ⓓ{q}V1.T1)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T -V2b -V2b
+      @(cpxs_strap2 … (ⓐV1a.ⓓ{q}V0.T0)) [ /4 width=7 by cpx_zeta, lifts_bind, lifts_flat/ ] -V -V1 -T1
+      @(cpxs_strap2 … (ⓓ{q}V0.ⓐV2a.T0)) /3 width=3 by cpxs_pair_sn, cpxs_bind_dx, cpx_theta/
+    ]
+  ]
+]
+qed-.
+
+(* Basic_1: was just: pr3_iso_appls_cast *)
+lemma cpxs_fwd_cast_vector (h) (G) (L):
+      ∀Vs,W,T,X2. ⦃G,L⦄ ⊢ ⒶVs.ⓝW.T ⬈*[h] X2 →
+      ∨∨ ⒶVs. ⓝW. T ⩳ X2
+       | ⦃G,L⦄ ⊢ ⒶVs.T ⬈*[h] X2
+       | ⦃G,L⦄ ⊢ ⒶVs.W ⬈*[h] X2.
+#h #G #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_cast/
+#V #Vs #IHVs #W #T #X2 #H
+elim (cpxs_inv_appl1 … H) -H *
+[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by teqo_pair, or3_intro0/
+| #q #W0 #T0 #HT0 #HU elim (IHVs … HT0) -IHVs -HT0 #HT0
+  [ elim (teqo_inv_applv_bind_simple … HT0) //
+  | @or3_intro1 -W (**) (* explicit constructor *)
+    @(cpxs_trans … HU) -X2
+    @(cpxs_strap1 … (ⓐV.ⓛ{q}W0.T0)) /2 width=1 by cpxs_flat_dx, cpx_beta/
+  | @or3_intro2 -T (**) (* explicit constructor *)
+    @(cpxs_trans … HU) -X2
+    @(cpxs_strap1 … (ⓐV.ⓛ{q}W0.T0)) /2 width=1 by cpxs_flat_dx, cpx_beta/
+  ]
+| #q #V0 #V1 #V2 #T0 #HV0 #HV01 #HT0 #HU
+  elim (IHVs … HT0) -IHVs -HT0 #HT0
+  [ elim (teqo_inv_applv_bind_simple … HT0) //
+  | @or3_intro1 -W (**) (* explicit constructor *)
+    @(cpxs_trans … HU) -X2
+    @(cpxs_strap1 … (ⓐV0.ⓓ{q}V2.T0)) /2 width=3 by cpxs_flat, cpx_theta/
+  | @or3_intro2 -T (**) (* explicit constructor *)
+    @(cpxs_trans … HU) -X2
+    @(cpxs_strap1 … (ⓐV0.ⓓ{q}V2.T0)) /2 width=3 by cpxs_flat, cpx_theta/
+  ]
+]
+qed-.
+
+(* Basic_1: was just: nf2_iso_appls_lref *)
+lemma cpxs_fwd_cnx_vector (h) (G) (L):
+      ∀T. 𝐒⦃T⦄ → ⦃G,L⦄ ⊢ ⬈[h] 𝐍⦃T⦄ →
+      ∀Vs,X2. ⦃G,L⦄ ⊢ ⒶVs.T ⬈*[h] X2 → ⒶVs.T ⩳ X2.
+#h #G #L #T #H1T #H2T #Vs elim Vs -Vs [ @(cpxs_fwd_cnx … H2T) ] (**) (* /2 width=3 by cpxs_fwd_cnx/ does not work *)
+#V #Vs #IHVs #X2 #H
+elim (cpxs_inv_appl1 … H) -H *
+[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by teqo_pair/
+| #p #W0 #T0 #HT0 #HU
+  lapply (IHVs … HT0) -IHVs -HT0 #HT0
+  elim (teqo_inv_applv_bind_simple … HT0) //
+| #p #V1 #V2 #V0 #T0 #HV1 #HV12 #HT0 #HU
+  lapply (IHVs … HT0) -IHVs -HT0 #HT0
+  elim (teqo_inv_applv_bind_simple … HT0) //
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_toeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_toeq.ma
deleted file mode 100644
index 8b6725af0..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_toeq.ma
+++ /dev/null
@@ -1,102 +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/toeq_tdeq.ma".
-include "basic_2/rt_computation/cpxs_lsubr.ma".
-include "basic_2/rt_computation/cpxs_cnx.ma".
-include "basic_2/rt_computation/lpxs_cpxs.ma".
-
-(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
-
-(* Forward lemmas with sort-irrelevant outer equivalence for terms **********)
-
-lemma cpxs_fwd_sort (h) (G) (L):
-      ∀X2,s1. ⦃G,L⦄ ⊢ ⋆s1 ⬈*[h] X2 → ⋆s1 ⩳ X2.
-#h #G #L #X2 #s1 #H
-elim (cpxs_inv_sort1 … H) -H #s2 #H destruct //
-qed-.
-
-(* Note: probably this is an inversion lemma *)
-(* Basic_2A1: was: cpxs_fwd_delta *)
-lemma cpxs_fwd_delta_drops (h) (I) (G) (L) (K):
-      ∀V1,i. ⇩*[i] L ≘ K.ⓑ{I}V1 →
-      ∀V2. ⇧*[↑i] V1 ≘ V2 →
-      ∀X2. ⦃G,L⦄ ⊢ #i ⬈*[h] X2 →
-      ∨∨ #i ⩳ X2 | ⦃G,L⦄ ⊢ V2 ⬈*[h] X2.
-#h #I #G #L #K #V1 #i #HLK #V2 #HV12 #X2 #H
-elim (cpxs_inv_lref1_drops … H) -H /2 width=1 by or_introl/
-* #I0 #K0 #V0 #U0 #HLK0 #HVU0 #HU0
-lapply (drops_mono … HLK0 … HLK) -HLK0 #H destruct
-/4 width=9 by cpxs_lifts_bi, drops_isuni_fwd_drop2, or_intror/
-qed-.
-
-(* Basic_1: was just: pr3_iso_beta *)
-lemma cpxs_fwd_beta (h) (p) (G) (L):
-      ∀V,W,T,X2. ⦃G,L⦄ ⊢ ⓐV.ⓛ{p}W.T ⬈*[h] X2 →
-      ∨∨ ⓐV.ⓛ{p}W.T ⩳ X2 | ⦃G,L⦄ ⊢ ⓓ{p}ⓝW.V.T ⬈*[h] X2.
-#h #p #G #L #V #W #T #X2 #H elim (cpxs_inv_appl1 … H) -H *
-[ #V0 #T0 #_ #_ #H destruct /2 width=1 by toeq_pair, or_introl/
-| #b #W0 #T0 #HT0 #HU
-  elim (cpxs_inv_abst1 … HT0) -HT0 #W1 #T1 #HW1 #HT1 #H destruct
-  lapply (lsubr_cpxs_trans … HT1 (L.ⓓⓝW.V) ?) -HT1
-  /5 width=3 by cpxs_trans, cpxs_bind, cpxs_pair_sn, lsubr_beta, or_intror/
-| #b #V1 #V2 #V0 #T1 #_ #_ #HT1 #_
-  elim (cpxs_inv_abst1 … HT1) -HT1 #W2 #T2 #_ #_ #H destruct
-]
-qed-.
-
-lemma cpxs_fwd_theta (h) (p) (G) (L):
-           ∀V1,V,T,X2. ⦃G,L⦄ ⊢ ⓐV1.ⓓ{p}V.T ⬈*[h] X2 →
-           ∀V2. ⇧*[1] V1 ≘ V2 →
-           ∨∨ ⓐV1.ⓓ{p}V.T ⩳ X2 | ⦃G,L⦄ ⊢ ⓓ{p}V.ⓐV2.T ⬈*[h] X2.
-#h #p #G #L #V1 #V #T #X2 #H #V2 #HV12
-elim (cpxs_inv_appl1 … H) -H *
-[ -HV12 #V0 #T0 #_ #_ #H destruct /2 width=1 by toeq_pair, or_introl/
-| #q #W #T0 #HT0 #HU
-  elim (cpxs_inv_abbr1_dx … HT0) -HT0 *
-  [ #V3 #T3 #_ #_ #H destruct
-  | #X #HT2 #H #H0 destruct
-    elim (lifts_inv_bind1 … H) -H #W2 #T2 #HW2 #HT02 #H destruct
-    @or_intror @(cpxs_trans … HU) -X2 (**) (* explicit constructor *)
-    @(cpxs_trans … (+ⓓV.ⓐV2.ⓛ{q}W2.T2)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T
-    @(cpxs_strap2 … (ⓐV1.ⓛ{q}W.T0)) [2: /2 width=1 by cpxs_beta_dx/ ]
-    /4 width=7 by cpx_zeta, lifts_bind, lifts_flat/
-  ]
-| #q #V3 #V4 #V0 #T0 #HV13 #HV34 #HT0 #HU
-  @or_intror @(cpxs_trans … HU) -X2 (**) (* explicit constructor *)
-  elim (cpxs_inv_abbr1_dx … HT0) -HT0 *
-  [ #V5 #T5 #HV5 #HT5 #H destruct
-    /6 width=9 by cpxs_lifts_bi, drops_refl, drops_drop, cpxs_flat, cpxs_bind/
-  | #X #HT1 #H #H0 destruct
-    elim (lifts_inv_bind1 … H) -H #V5 #T5 #HV05 #HT05 #H destruct
-    lapply (cpxs_lifts_bi … HV13 (Ⓣ) … (L.ⓓV0) … HV12 … HV34) -V3 /3 width=1 by drops_refl, drops_drop/ #HV24
-    @(cpxs_trans … (+ⓓV.ⓐV2.ⓓ{q}V5.T5)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T
-    @(cpxs_strap2 … (ⓐV1.ⓓ{q}V0.T0)) [ /4 width=7 by cpx_zeta, lifts_bind, lifts_flat/ ] -V -V5 -T5
-    @(cpxs_strap2 … (ⓓ{q}V0.ⓐV2.T0)) /3 width=3 by cpxs_pair_sn, cpxs_bind_dx, cpx_theta/
-  ]
-]
-qed-.
-
-lemma cpxs_fwd_cast (h) (G) (L):
-      ∀W,T,X2. ⦃G,L⦄ ⊢ ⓝW.T ⬈*[h] X2 →
-      ∨∨ ⓝW. T ⩳ X2 | ⦃G,L⦄ ⊢ T ⬈*[h] X2 | ⦃G,L⦄ ⊢ W ⬈*[h] X2.
-#h #G #L #W #T #X2 #H
-elim (cpxs_inv_cast1 … H) -H /2 width=1 by or3_intro1, or3_intro2/ *
-#W0 #T0 #_ #_ #H destruct /2 width=1 by toeq_pair, or3_intro0/
-qed-.
-
-lemma cpxs_fwd_cnx (h) (G) (L):
-      ∀T1. ⦃G,L⦄ ⊢ ⬈[h] 𝐍⦃T1⦄ →
-      ∀X2. ⦃G,L⦄ ⊢ T1 ⬈*[h] X2 → T1 ⩳ X2.
-/3 width=5 by cpxs_inv_cnx1, tdeq_toeq/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_toeq_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_toeq_vector.ma
deleted file mode 100644
index 20702a354..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_toeq_vector.ma
+++ /dev/null
@@ -1,188 +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/toeq_simple_vector.ma".
-include "static_2/relocation/lifts_vector.ma".
-include "basic_2/rt_computation/cpxs_toeq.ma".
-
-(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
-
-(* Vector form of forward lemmas with outer equivalence for terms ***********)
-
-lemma cpxs_fwd_sort_vector (h) (G) (L):
-      ∀s,Vs,X2. ⦃G,L⦄ ⊢ ⒶVs.⋆s ⬈*[h] X2 → ⒶVs.⋆s ⩳ X2.
-#h #G #L #s #Vs elim Vs -Vs /2 width=4 by cpxs_fwd_sort/
-#V #Vs #IHVs #X2 #H
-elim (cpxs_inv_appl1 … H) -H *
-[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1 by toeq_pair/
-| #p #W1 #T1 #HT1 #HU
-  lapply (IHVs … HT1) -IHVs -HT1 #HT1
-  elim (toeq_inv_applv_bind_simple … HT1) //
-| #p #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU
-  lapply (IHVs … HT1) -IHVs -HT1 #HT1
-  elim (toeq_inv_applv_bind_simple … HT1) //
-]
-qed-.
-
-(* Basic_2A1: was: cpxs_fwd_delta_vector *)
-lemma cpxs_fwd_delta_drops_vector (h) (I) (G) (L) (K):
-      ∀V1,i. ⇩*[i] L ≘ K.ⓑ{I}V1 →
-      ∀V2. ⇧*[↑i] V1 ≘ V2 →
-      ∀Vs,X2. ⦃G,L⦄ ⊢ ⒶVs.#i ⬈*[h] X2 →
-      ∨∨ ⒶVs.#i ⩳ X2 | ⦃G,L⦄ ⊢ ⒶVs.V2 ⬈*[h] X2.
-#h #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs
-elim Vs -Vs /2 width=5 by cpxs_fwd_delta_drops/
-#V #Vs #IHVs #X2 #H -K -V1
-elim (cpxs_inv_appl1 … H) -H *
-[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by toeq_pair, or_introl/
-| #q #W0 #T0 #HT0 #HU
-  elim (IHVs … HT0) -IHVs -HT0 #HT0
-  [ elim (toeq_inv_applv_bind_simple … HT0) //
-  | @or_intror -i (**) (* explicit constructor *)
-    @(cpxs_trans … HU) -X2
-    @(cpxs_strap1 … (ⓐV.ⓛ{q}W0.T0)) /3 width=1 by cpxs_flat_dx, cpx_beta/
-  ]
-| #q #V0 #V1 #V3 #T0 #HV0 #HV01 #HT0 #HU
-  elim (IHVs … HT0) -IHVs -HT0 #HT0
-  [ elim (toeq_inv_applv_bind_simple … HT0) //
-  | @or_intror -i (**) (* explicit constructor *)
-    @(cpxs_trans … HU) -X2
-    @(cpxs_strap1 … (ⓐV0.ⓓ{q}V3.T0)) /3 width=3 by cpxs_flat, cpx_theta/
-  ]
-]
-qed-.
-
-(* Basic_1: was just: pr3_iso_appls_beta *)
-lemma cpxs_fwd_beta_vector (h) (p) (G) (L):
-      ∀Vs,V,W,T,X2. ⦃G,L⦄ ⊢ ⒶVs.ⓐV.ⓛ{p}W.T ⬈*[h] X2 →
-      ∨∨ ⒶVs.ⓐV.ⓛ{p}W. T ⩳ X2 | ⦃G,L⦄ ⊢ ⒶVs.ⓓ{p}ⓝW.V.T ⬈*[h] X2.
-#h #p #G #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_beta/
-#V0 #Vs #IHVs #V #W #T #X2 #H
-elim (cpxs_inv_appl1 … H) -H *
-[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1 by toeq_pair, or_introl/
-| #q #W1 #T1 #HT1 #HU
-  elim (IHVs … HT1) -IHVs -HT1 #HT1
-  [ elim (toeq_inv_applv_bind_simple … HT1) //
-  | @or_intror (**) (* explicit constructor *)
-    @(cpxs_trans … HU) -X2
-    @(cpxs_strap1 … (ⓐV0.ⓛ{q}W1.T1)) /3 width=1 by cpxs_flat_dx, cpx_beta/
-  ]
-| #q #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU
-  elim (IHVs … HT1) -IHVs -HT1 #HT1
-  [ elim (toeq_inv_applv_bind_simple … HT1) //
-  | @or_intror (**) (* explicit constructor *)
-    @(cpxs_trans … HU) -X2
-    @(cpxs_strap1 … (ⓐV1.ⓓ{q}V3.T1)) /3 width=3 by cpxs_flat, cpx_theta/
-  ]
-]
-qed-.
-
-(* Basic_1: was just: pr3_iso_appls_abbr *)
-lemma cpxs_fwd_theta_vector (h) (G) (L):
-      ∀V1b,V2b. ⇧*[1] V1b ≘ V2b →
-      ∀p,V,T,X2. ⦃G,L⦄ ⊢ ⒶV1b.ⓓ{p}V.T ⬈*[h] X2 →
-      ∨∨ ⒶV1b.ⓓ{p}V.T ⩳ X2 | ⦃G,L⦄ ⊢ ⓓ{p}V.ⒶV2b.T ⬈*[h] X2.
-#h #G #L #V1b #V2b * -V1b -V2b /3 width=1 by or_intror/
-#V1b #V2b #V1a #V2a #HV12a #HV12b #p
-generalize in match HV12a; -HV12a
-generalize in match V2a; -V2a
-generalize in match V1a; -V1a
-elim HV12b -V1b -V2b /2 width=1 by cpxs_fwd_theta/
-#V1b #V2b #V1b #V2b #HV12b #_ #IHV12b #V1a #V2a #HV12a #V #T #X2 #H
-elim (cpxs_inv_appl1 … H) -H *
-[ -IHV12b -HV12a -HV12b #V0 #T0 #_ #_ #H destruct /2 width=1 by toeq_pair, or_introl/
-| #q #W0 #T0 #HT0 #HU
-  elim (IHV12b … HV12b … HT0) -IHV12b -HT0 #HT0
-  [ -HV12a -HV12b -HU
-    elim (toeq_inv_pair1 … HT0) #V1 #T1 #H destruct
-  | @or_intror -V1b (**) (* explicit constructor *)
-    @(cpxs_trans … HU) -X2
-    elim (cpxs_inv_abbr1_dx … HT0) -HT0 *
-    [ -HV12a #V1 #T1 #_ #_ #H destruct
-    | -V1b #X #HT1 #H #H0 destruct
-      elim (lifts_inv_bind1 … H) -H #W1 #T1 #HW01 #HT01 #H destruct
-      @(cpxs_trans … (+ⓓV.ⓐV2a.ⓛ{q}W1.T1)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T -V2b -V2b
-      @(cpxs_strap2 … (ⓐV1a.ⓛ{q}W0.T0))
-      /4 width=7 by cpxs_beta_dx, cpx_zeta, lifts_bind, lifts_flat/
-    ]
-  ]
-| #q #V0a #Va #V0 #T0 #HV10a #HV0a #HT0 #HU
-  elim (IHV12b … HV12b … HT0) -HV12b -IHV12b -HT0 #HT0
-  [ -HV12a -HV10a -HV0a -HU
-    elim (toeq_inv_pair1 … HT0) #V1 #T1 #H destruct
-  | @or_intror -V1b -V1b (**) (* explicit constructor *)
-    @(cpxs_trans … HU) -X2
-    elim (cpxs_inv_abbr1_dx … HT0) -HT0 *
-    [ #V1 #T1 #HV1 #HT1 #H destruct
-      lapply (cpxs_lifts_bi … HV10a (Ⓣ) … (L.ⓓV) … HV12a … HV0a) -V1a -V0a /3 width=1 by drops_refl, drops_drop/ #HV2a
-      @(cpxs_trans … (ⓓ{p}V.ⓐV2a.T1)) /3 width=1 by cpxs_bind, cpxs_pair_sn, cpxs_flat_dx, cpxs_bind_dx/
-    | #X #HT1 #H #H0 destruct
-      elim (lifts_inv_bind1 … H) -H #V1 #T1 #HW01 #HT01 #H destruct
-      lapply (cpxs_lifts_bi … HV10a (Ⓣ) … (L.ⓓV0) … HV12a … HV0a) -V0a /3 width=1 by drops_refl, drops_drop/ #HV2a
-      @(cpxs_trans … (+ⓓV.ⓐV2a.ⓓ{q}V1.T1)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T -V2b -V2b
-      @(cpxs_strap2 … (ⓐV1a.ⓓ{q}V0.T0)) [ /4 width=7 by cpx_zeta, lifts_bind, lifts_flat/ ] -V -V1 -T1
-      @(cpxs_strap2 … (ⓓ{q}V0.ⓐV2a.T0)) /3 width=3 by cpxs_pair_sn, cpxs_bind_dx, cpx_theta/
-    ]
-  ]
-]
-qed-.
-
-(* Basic_1: was just: pr3_iso_appls_cast *)
-lemma cpxs_fwd_cast_vector (h) (G) (L):
-      ∀Vs,W,T,X2. ⦃G,L⦄ ⊢ ⒶVs.ⓝW.T ⬈*[h] X2 →
-      ∨∨ ⒶVs. ⓝW. T ⩳ X2
-       | ⦃G,L⦄ ⊢ ⒶVs.T ⬈*[h] X2
-       | ⦃G,L⦄ ⊢ ⒶVs.W ⬈*[h] X2.
-#h #G #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_cast/
-#V #Vs #IHVs #W #T #X2 #H
-elim (cpxs_inv_appl1 … H) -H *
-[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by toeq_pair, or3_intro0/
-| #q #W0 #T0 #HT0 #HU elim (IHVs … HT0) -IHVs -HT0 #HT0
-  [ elim (toeq_inv_applv_bind_simple … HT0) //
-  | @or3_intro1 -W (**) (* explicit constructor *)
-    @(cpxs_trans … HU) -X2
-    @(cpxs_strap1 … (ⓐV.ⓛ{q}W0.T0)) /2 width=1 by cpxs_flat_dx, cpx_beta/
-  | @or3_intro2 -T (**) (* explicit constructor *)
-    @(cpxs_trans … HU) -X2
-    @(cpxs_strap1 … (ⓐV.ⓛ{q}W0.T0)) /2 width=1 by cpxs_flat_dx, cpx_beta/
-  ]
-| #q #V0 #V1 #V2 #T0 #HV0 #HV01 #HT0 #HU
-  elim (IHVs … HT0) -IHVs -HT0 #HT0
-  [ elim (toeq_inv_applv_bind_simple … HT0) //
-  | @or3_intro1 -W (**) (* explicit constructor *)
-    @(cpxs_trans … HU) -X2
-    @(cpxs_strap1 … (ⓐV0.ⓓ{q}V2.T0)) /2 width=3 by cpxs_flat, cpx_theta/
-  | @or3_intro2 -T (**) (* explicit constructor *)
-    @(cpxs_trans … HU) -X2
-    @(cpxs_strap1 … (ⓐV0.ⓓ{q}V2.T0)) /2 width=3 by cpxs_flat, cpx_theta/
-  ]
-]
-qed-.
-
-(* Basic_1: was just: nf2_iso_appls_lref *)
-lemma cpxs_fwd_cnx_vector (h) (G) (L):
-      ∀T. 𝐒⦃T⦄ → ⦃G,L⦄ ⊢ ⬈[h] 𝐍⦃T⦄ →
-      ∀Vs,X2. ⦃G,L⦄ ⊢ ⒶVs.T ⬈*[h] X2 → ⒶVs.T ⩳ X2.
-#h #G #L #T #H1T #H2T #Vs elim Vs -Vs [ @(cpxs_fwd_cnx … H2T) ] (**) (* /2 width=3 by cpxs_fwd_cnx/ does not work *)
-#V #Vs #IHVs #X2 #H
-elim (cpxs_inv_appl1 … H) -H *
-[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by toeq_pair/
-| #p #W0 #T0 #HT0 #HU
-  lapply (IHVs … HT0) -IHVs -HT0 #HT0
-  elim (toeq_inv_applv_bind_simple … HT0) //
-| #p #V1 #V2 #V0 #T0 #HV1 #HV12 #HT0 #HU
-  lapply (IHVs … HT0) -IHVs -HT0 #HT0
-  elim (toeq_inv_applv_bind_simple … HT0) //
-]
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx_vector.ma
index 6d75480ff..949c28d9a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx_vector.ma
@@ -14,8 +14,8 @@
 
 (* STRONGLY NORMALIZING TERM VECTORS FOR UNBOUND PARALLEL RT-TRANSITION *****)
 
-include "basic_2/rt_computation/cpxs_toeq_vector.ma".
-include "basic_2/rt_computation/csx_simple_toeq.ma".
+include "basic_2/rt_computation/cpxs_teqo_vector.ma".
+include "basic_2/rt_computation/csx_simple_teqo.ma".
 include "basic_2/rt_computation/csx_cnx.ma".
 include "basic_2/rt_computation/csx_cpxs.ma".
 include "basic_2/rt_computation/csx_vector.ma".
@@ -30,7 +30,7 @@ lemma csx_applv_cnx (h) (G) (L):
 [ #_ normalize in ⊢ (????%); /2 width=1 by cnx_csx/
 | #V #Vs #IHV #H
   elim (csxv_inv_cons … H) -H #HV #HVs
-  @csx_appl_simple_toeq /2 width=1 by applv_simple/ -IHV -HV -HVs
+  @csx_appl_simple_teqo /2 width=1 by applv_simple/ -IHV -HV -HVs
   #X #H #H0
   lapply (cpxs_fwd_cnx_vector … H) -H // -H1T -H2T #H
   elim (H0) -H0 //
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma
index 53473452e..d88452162 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/rt_computation/cpxs_toeq_vector.ma".
-include "basic_2/rt_computation/csx_simple_toeq.ma".
+include "basic_2/rt_computation/cpxs_teqo_vector.ma".
+include "basic_2/rt_computation/csx_simple_teqo.ma".
 include "basic_2/rt_computation/csx_lsubr.ma".
 include "basic_2/rt_computation/csx_lpx.ma".
 include "basic_2/rt_computation/csx_vector.ma".
@@ -30,7 +30,7 @@ lemma csx_applv_beta (h) (G):
 #V0 #Vs #IHV #V #W #T #H1T
 lapply (csx_fwd_pair_sn … H1T) #HV0
 lapply (csx_fwd_flat_dx … H1T) #H2T
-@csx_appl_simple_toeq /2 width=1 by applv_simple, simple_flat/ -IHV -HV0 -H2T
+@csx_appl_simple_teqo /2 width=1 by applv_simple, simple_flat/ -IHV -HV0 -H2T
 #X #H #H0
 elim (cpxs_fwd_beta_vector … H) -H #H
 [ -H1T elim H0 -H0 //
@@ -47,7 +47,7 @@ lemma csx_applv_delta_drops (h) (G):
 | #V #Vs #IHV #H1T
   lapply (csx_fwd_pair_sn … H1T) #HV
   lapply (csx_fwd_flat_dx … H1T) #H2T
-  @csx_appl_simple_toeq /2 width=1 by applv_simple, simple_atom/ -IHV -HV  -H2T
+  @csx_appl_simple_teqo /2 width=1 by applv_simple, simple_atom/ -IHV -HV  -H2T
   #X #H #H0
   elim (cpxs_fwd_delta_drops_vector … HLK … HV12 … H) -HLK -HV12 -H #H
   [ -H1T elim H0 -H0 //
@@ -68,7 +68,7 @@ elim H -V1b -V2b /2 width=3 by csx_appl_theta/
 lapply (csx_appl_theta … H … HW12) -H -HW12 #H
 lapply (csx_fwd_pair_sn … H) #HW1
 lapply (csx_fwd_flat_dx … H) #H1
-@csx_appl_simple_toeq /2 width=3 by simple_flat/ -IHV12b -HW1 -H1 #X #H1 #H2
+@csx_appl_simple_teqo /2 width=3 by simple_flat/ -IHV12b -HW1 -H1 #X #H1 #H2
 elim (cpxs_fwd_theta_vector … (V2⨮V2b) … H1) -H1 /2 width=1 by liftsv_cons/ -HV12b -HV12
 [ -H #H elim H2 -H2 //
 | -H2 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/
@@ -84,7 +84,7 @@ lemma csx_applv_cast (h) (G):
 lapply (csx_fwd_pair_sn … H1U) #HV
 lapply (csx_fwd_flat_dx … H1U) #H2U
 lapply (csx_fwd_flat_dx … H1T) #H2T
-@csx_appl_simple_toeq /2 width=1 by applv_simple, simple_flat/ -IHV -HV -H2U -H2T
+@csx_appl_simple_teqo /2 width=1 by applv_simple, simple_flat/ -IHV -HV -H2U -H2T
 #X #H #H0
 elim (cpxs_fwd_cast_vector … H) -H #H
 [ -H1U -H1T elim H0 -H0 //
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple_teqo.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple_teqo.ma
new file mode 100644
index 000000000..c56f1f718
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple_teqo.ma
@@ -0,0 +1,49 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "static_2/syntax/teqo_simple.ma".
+include "static_2/syntax/teqo_teqo.ma".
+include "basic_2/rt_transition/cpx_simple.ma".
+include "basic_2/rt_computation/cpxs.ma".
+include "basic_2/rt_computation/csx_csx.ma".
+
+(* STRONGLY NORMALIZING TERMS FOR UNBOUND PARALLEL RT-TRANSITION ************)
+
+(* Properties with outer equivalence for terms ******************************)
+
+(* Basic_1: was just: sn3_appl_appl *)
+(* Basic_2A1: was: csx_appl_simple_tsts *)
+lemma csx_appl_simple_teqo (h) (G) (L):
+      ∀V. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃V⦄ → ∀T1. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ →
+      (∀T2. ⦃G,L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ⩳ T2 → ⊥) → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓐV.T2⦄) →
+      𝐒⦃T1⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓐV.T1⦄.
+#h #G #L #V #H @(csx_ind … H) -V
+#V #_ #IHV #T1 #H @(csx_ind … H) -T1
+#T1 #H1T1 #IHT1 #H2T1 #H3T1
+@csx_intro #X #HL #H
+elim (cpx_inv_appl1_simple … HL) -HL //
+#V0 #T0 #HLV0 #HLT10 #H0 destruct
+elim (tdneq_inv_pair … H) -H
+[ #H elim H -H //
+| -IHT1 #HV0
+  @(csx_cpx_trans … (ⓐV0.T1)) /2 width=1 by cpx_flat/ -HLT10
+  @IHV -IHV /4 width=3 by csx_cpx_trans, cpx_pair_sn/
+| -IHV -H1T1 #H1T10
+  @(csx_cpx_trans … (ⓐV.T0)) /2 width=1 by cpx_flat/ -HLV0
+  elim (teqo_dec T1 T0) #H2T10
+  [ @IHT1 -IHT1 /4 width=5 by cpxs_strap2, cpxs_strap1, teqo_canc_sn, simple_teqo_repl_dx/
+  | -IHT1 -H3T1 -H1T10 /3 width=1 by cpx_cpxs/
+  ]
+]
+qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple_toeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple_toeq.ma
deleted file mode 100644
index 8fb338684..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple_toeq.ma
+++ /dev/null
@@ -1,49 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "static_2/syntax/toeq_simple.ma".
-include "static_2/syntax/toeq_toeq.ma".
-include "basic_2/rt_transition/cpx_simple.ma".
-include "basic_2/rt_computation/cpxs.ma".
-include "basic_2/rt_computation/csx_csx.ma".
-
-(* STRONGLY NORMALIZING TERMS FOR UNBOUND PARALLEL RT-TRANSITION ************)
-
-(* Properties with outer equivalence for terms ******************************)
-
-(* Basic_1: was just: sn3_appl_appl *)
-(* Basic_2A1: was: csx_appl_simple_tsts *)
-lemma csx_appl_simple_toeq (h) (G) (L):
-      ∀V. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃V⦄ → ∀T1. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ →
-      (∀T2. ⦃G,L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ⩳ T2 → ⊥) → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓐV.T2⦄) →
-      𝐒⦃T1⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓐV.T1⦄.
-#h #G #L #V #H @(csx_ind … H) -V
-#V #_ #IHV #T1 #H @(csx_ind … H) -T1
-#T1 #H1T1 #IHT1 #H2T1 #H3T1
-@csx_intro #X #HL #H
-elim (cpx_inv_appl1_simple … HL) -HL //
-#V0 #T0 #HLV0 #HLT10 #H0 destruct
-elim (tdneq_inv_pair … H) -H
-[ #H elim H -H //
-| -IHT1 #HV0
-  @(csx_cpx_trans … (ⓐV0.T1)) /2 width=1 by cpx_flat/ -HLT10
-  @IHV -IHV /4 width=3 by csx_cpx_trans, cpx_pair_sn/
-| -IHV -H1T1 #H1T10
-  @(csx_cpx_trans … (ⓐV.T0)) /2 width=1 by cpx_flat/ -HLV0
-  elim (toeq_dec T1 T0) #H2T10
-  [ @IHT1 -IHT1 /4 width=5 by cpxs_strap2, cpxs_strap1, toeq_canc_sn, simple_toeq_repl_dx/
-  | -IHT1 -H3T1 -H1T10 /3 width=1 by cpx_cpxs/
-  ]
-]
-qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_req.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_req.ma
index 5f0c34f6c..3379c6e23 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_req.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_req.ma
@@ -20,7 +20,7 @@ include "basic_2/rt_transition/rpx_fsle.ma".
 (* Properties with syntactic equivalence for lenvs on referred entries ******)
 
 (* Basic_2A1: was: lleq_cpx_trans *)
-lemma req_cpx_trans: ∀h,G. req_transitive (cpx h G).
+lemma req_cpx_trans (h) (G): req_transitive (cpx h G).
 #h #G #L2 #T1 #T2 #H @(cpx_ind … H) -G -L2 -T1 -T2 /2 width=2 by cpx_ess/
 [ #I #G #K2 #V1 #V2 #W2 #_ #IH #HVW2 #L1 #H
   elim (req_inv_zero_pair_dx … H) -H #K1 #HK12 #H destruct
@@ -48,18 +48,7 @@ lemma req_cpx_trans: ∀h,G. req_transitive (cpx h G).
   elim (req_inv_bind … H) -H /3 width=3 by cpx_theta/
 ]
 qed-.
-(*
-(* Basic_2A1: was: cpx_lleq_conf *)
-lemma cpx_req_conf: ∀h,G,L2,T1,T2. ⦃G,L2⦄ ⊢ T1 ⬈[h] T2 →
-                    ∀L1. L2 ≘[T1] L1 → ⦃G,L1⦄ ⊢ T1 ⬈[h] T2.
-/3 width=3 by req_cpx_trans, req_sym/ qed-.
-*)
+
 (* Basic_2A1: was: cpx_lleq_conf_sn *)
-lemma cpx_req_conf_sn: ∀h,G. s_r_confluent1 … (cpx h G) req.
+lemma cpx_req_conf_sn (h) (G): s_r_confluent1 … (cpx h G) req.
 /2 width=5 by cpx_rex_conf/ qed-.
-(*
-(* Basic_2A1: was: cpx_lleq_conf_dx *)
-lemma cpx_req_conf_dx: ∀h,G,L2,T1,T2. ⦃G,L2⦄ ⊢ T1 ⬈[h] T2 →
-                       ∀L1. L1 ≘[T1] L2 → L1 ≘[T2] L2.
-/4 width=6 by cpx_req_conf_sn, req_sym/ 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 6e4575ba0..7773fd7b9 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
@@ -88,10 +88,10 @@ table {
              [ [ "compatibility for lenvs" ] "jsx" + "( ? ⊢ ? ⊒[?] ? )" "jsx_drops" + "jsx_lsubr" + "jsx_csx" + "jsx_rsx" + "jsx_jsx" * ]
              [ [ "strongly normalizing for lenvs on referred entries" ] "rsx" + "( ? ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "rsx_length" + "rsx_drops" + "rsx_fqup" + "rsx_cpxs" + "rsx_csx" + "rsx_rsx" * ]
              [ [ "strongly normalizing for term vectors" ] "csx_vector" + "( ⦃?,?⦄ ⊢ ⬈*[?] 𝐒⦃?⦄ )" "csx_cnx_vector" + "csx_csx_vector" * ]
-             [ [ "strongly normalizing for terms" ] "csx" + "( ⦃?,?⦄ ⊢ ⬈*[?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_toeq" + "csx_drops" + "csx_fqus" + "csx_lsubr" + "csx_rdeq" + "csx_fdeq" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lpx" + "csx_cnx" + "csx_fpbq" + "csx_cpxs" + "csx_lpxs" + "csx_csx" * ]
+             [ [ "strongly normalizing for terms" ] "csx" + "( ⦃?,?⦄ ⊢ ⬈*[?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_teqo" + "csx_drops" + "csx_fqus" + "csx_lsubr" + "csx_rdeq" + "csx_fdeq" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lpx" + "csx_cnx" + "csx_fpbq" + "csx_cpxs" + "csx_lpxs" + "csx_csx" * ]
              [ [ "for lenvs on all entries" ] "lpxs" + "( ⦃?,?⦄ ⊢ ⬈*[?] ? )" "lpxs_length" + "lpxs_drops" + "lpxs_rdeq" + "lpxs_fdeq" + "lpxs_aaa" + "lpxs_lpx" + "lpxs_cpxs" + "lpxs_lpxs" * ]
              [ [ "for binders" ] "cpxs_ext" + "( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" * ]
-             [ [ "for terms" ] "cpxs" + "( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_toeq" + "cpxs_toeq_vector" + "cpxs_drops" + "cpxs_fqus" + "cpxs_lsubr" + "cpxs_rdeq" + "cpxs_fdeq" + "cpxs_aaa" + "cpxs_lpx" + "cpxs_cnx" + "cpxs_cpxs" * ] 
+             [ [ "for terms" ] "cpxs" + "( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_teqo" + "cpxs_teqo_vector" + "cpxs_drops" + "cpxs_fqus" + "cpxs_lsubr" + "cpxs_rdeq" + "cpxs_fdeq" + "cpxs_aaa" + "cpxs_lpx" + "cpxs_cnx" + "cpxs_cpxs" * ] 
           }
         ]
      }
diff --git a/matita/matita/contribs/lambdadelta/refile.sh b/matita/matita/contribs/lambdadelta/refile.sh
new file mode 100644
index 000000000..ef74a9818
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/refile.sh
@@ -0,0 +1,8 @@
+#!/bin/sh
+for SRC in `find ground_2 static_2 basic_2 apps_2 -name "*.ma"`; do
+  if [ ! -e ${SRC//$1/$2} ];
+    then echo ${SRC//$1/$2}; git mv $SRC ${SRC//$1/$2};
+  fi
+done
+
+unset SRC
diff --git a/matita/matita/contribs/lambdadelta/static_2/etc/frees_drops.etc b/matita/matita/contribs/lambdadelta/static_2/etc/frees_drops.etc
new file mode 100644
index 000000000..0b5e52fa5
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/static_2/etc/frees_drops.etc
@@ -0,0 +1,17 @@
+lemma frees_sort_pushs:
+      ∀f,K,s. K ⊢ 𝐅+⦃⋆s⦄ ≘ f →
+      ∀i,L. ⇩*[i] L ≘ K → L ⊢ 𝐅+⦃⋆s⦄ ≘ ⫯*[i] f.
+#f #K #s #Hf #i elim i -i
+[ #L #H lapply (drops_fwd_isid … H ?) -H //
+| #i #IH #L #H elim (drops_inv_succ … H) -H /3 width=1 by frees_sort/
+]
+qed.
+
+lemma frees_gref_pushs:
+      ∀f,K,l. K ⊢ 𝐅+⦃§l⦄ ≘ f →
+      ∀i,L. ⇩*[i] L ≘ K → L ⊢ 𝐅+⦃§l⦄ ≘ ⫯*[i] f.
+#f #K #l #Hf #i elim i -i
+[ #L #H lapply (drops_fwd_isid … H ?) -H //
+| #i #IH #L #H elim (drops_inv_succ … H) -H /3 width=1 by frees_gref/
+]
+qed.
diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_teqo.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_teqo.ma
new file mode 100644
index 000000000..be9437843
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_teqo.ma
@@ -0,0 +1,76 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "static_2/syntax/teqo.ma".
+include "static_2/relocation/lifts_lifts.ma".
+
+(* GENERIC RELOCATION FOR TERMS *********************************************)
+
+(* Properties with sort-irrelevant outer equivalence for terms **************)
+
+lemma teqo_lifts_sn: liftable2_sn teqo.
+#T1 #T2 #H elim H -T1 -T2 [||| * ]
+[ #s1 #s2 #f #X #H 
+  >(lifts_inv_sort1 … H) -H
+  /2 width=3 by teqo_sort, ex2_intro/
+| #i #f #X #H
+  elim (lifts_inv_lref1 … H) -H #j #Hj #H destruct
+  /3 width=3 by teqo_lref, lifts_lref, ex2_intro/
+| #l #f #X #H
+  >(lifts_inv_gref1 … H) -H
+  /2 width=3 by teqo_gref, ex2_intro/
+| #p #I #V1 #V2 #T1 #T2 #f #X #H
+  elim (lifts_inv_bind1 … H) -H #W1 #U1 #_ #_ #H destruct -V1 -T1
+  elim (lifts_total V2 f) #W2 #HVW2
+  elim (lifts_total T2 (⫯f)) #U2 #HTU2
+  /3 width=3 by teqo_pair, lifts_bind, ex2_intro/
+| #I #V1 #V2 #T1 #T2 #f #X #H
+  elim (lifts_inv_flat1 … H) -H #W1 #U1 #_ #_ #H destruct -V1 -T1
+  elim (lifts_total V2 f) #W2 #HVW2
+  elim (lifts_total T2 f) #U2 #HTU2
+  /3 width=3 by teqo_pair, lifts_flat, ex2_intro/
+]
+qed-.
+
+lemma teqo_lifts_dx: liftable2_dx teqo.
+/3 width=3 by teqo_lifts_sn, liftable2_sn_dx, teqo_sym/ qed-.
+
+lemma teqo_lifts_bi: liftable2_bi teqo.
+/3 width=6 by teqo_lifts_sn, liftable2_sn_bi/ qed-.
+
+(* Inversion lemmas with sort-irrelevant outer equivalence for terms ********)
+
+lemma teqo_inv_lifts_bi: deliftable2_bi teqo.
+#U1 #U2 #H elim H -U1 -U2 [||| * ]
+[ #s1 #s2 #f #X1 #H1 #X2 #H2
+  >(lifts_inv_sort2 … H1) -H1 >(lifts_inv_sort2 … H2) -H2
+  /1 width=1 by teqo_sort/
+| #j #f #X1 #H1 #X2 #H2
+  elim (lifts_inv_lref2 … H1) -H1 #i1 #Hj1 #H destruct
+  elim (lifts_inv_lref2 … H2) -H2 #i2 #Hj2 #H destruct
+  <(at_inj … Hj2 … Hj1) -j -f -i1
+  /1 width=1 by teqo_lref/
+| #l #f #X1 #H1 #X2 #H2
+  >(lifts_inv_gref2 … H1) -H1 >(lifts_inv_gref2 … H2) -H2
+  /1 width=1 by teqo_gref/
+| #p #I #W1 #W2 #U1 #U2 #f #X1 #H1 #X2 #H2
+  elim (lifts_inv_bind2 … H1) -H1 #V1 #T1 #_ #_ #H destruct -W1 -U1
+  elim (lifts_inv_bind2 … H2) -H2 #V2 #T2 #_ #_ #H destruct -W2 -U2
+  /1 width=1 by teqo_pair/
+| #I #W1 #W2 #U1 #U2 #f #X1 #H1 #X2 #H2
+  elim (lifts_inv_flat2 … H1) -H1 #V1 #T1 #_ #_ #H destruct -W1 -U1
+  elim (lifts_inv_flat2 … H2) -H2 #V2 #T2 #_ #_ #H destruct -W2 -U2
+  /1 width=1 by teqo_pair/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_toeq.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_toeq.ma
deleted file mode 100644
index ffbddcbe4..000000000
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_toeq.ma
+++ /dev/null
@@ -1,76 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "static_2/syntax/toeq.ma".
-include "static_2/relocation/lifts_lifts.ma".
-
-(* GENERIC RELOCATION FOR TERMS *********************************************)
-
-(* Properties with sort-irrelevant outer equivalence for terms **************)
-
-lemma toeq_lifts_sn: liftable2_sn toeq.
-#T1 #T2 #H elim H -T1 -T2 [||| * ]
-[ #s1 #s2 #f #X #H 
-  >(lifts_inv_sort1 … H) -H
-  /2 width=3 by toeq_sort, ex2_intro/
-| #i #f #X #H
-  elim (lifts_inv_lref1 … H) -H #j #Hj #H destruct
-  /3 width=3 by toeq_lref, lifts_lref, ex2_intro/
-| #l #f #X #H
-  >(lifts_inv_gref1 … H) -H
-  /2 width=3 by toeq_gref, ex2_intro/
-| #p #I #V1 #V2 #T1 #T2 #f #X #H
-  elim (lifts_inv_bind1 … H) -H #W1 #U1 #_ #_ #H destruct -V1 -T1
-  elim (lifts_total V2 f) #W2 #HVW2
-  elim (lifts_total T2 (⫯f)) #U2 #HTU2
-  /3 width=3 by toeq_pair, lifts_bind, ex2_intro/
-| #I #V1 #V2 #T1 #T2 #f #X #H
-  elim (lifts_inv_flat1 … H) -H #W1 #U1 #_ #_ #H destruct -V1 -T1
-  elim (lifts_total V2 f) #W2 #HVW2
-  elim (lifts_total T2 f) #U2 #HTU2
-  /3 width=3 by toeq_pair, lifts_flat, ex2_intro/
-]
-qed-.
-
-lemma toeq_lifts_dx: liftable2_dx toeq.
-/3 width=3 by toeq_lifts_sn, liftable2_sn_dx, toeq_sym/ qed-.
-
-lemma toeq_lifts_bi: liftable2_bi toeq.
-/3 width=6 by toeq_lifts_sn, liftable2_sn_bi/ qed-.
-
-(* Inversion lemmas with sort-irrelevant outer equivalence for terms ********)
-
-lemma toeq_inv_lifts_bi: deliftable2_bi toeq.
-#U1 #U2 #H elim H -U1 -U2 [||| * ]
-[ #s1 #s2 #f #X1 #H1 #X2 #H2
-  >(lifts_inv_sort2 … H1) -H1 >(lifts_inv_sort2 … H2) -H2
-  /1 width=1 by toeq_sort/
-| #j #f #X1 #H1 #X2 #H2
-  elim (lifts_inv_lref2 … H1) -H1 #i1 #Hj1 #H destruct
-  elim (lifts_inv_lref2 … H2) -H2 #i2 #Hj2 #H destruct
-  <(at_inj … Hj2 … Hj1) -j -f -i1
-  /1 width=1 by toeq_lref/
-| #l #f #X1 #H1 #X2 #H2
-  >(lifts_inv_gref2 … H1) -H1 >(lifts_inv_gref2 … H2) -H2
-  /1 width=1 by toeq_gref/
-| #p #I #W1 #W2 #U1 #U2 #f #X1 #H1 #X2 #H2
-  elim (lifts_inv_bind2 … H1) -H1 #V1 #T1 #_ #_ #H destruct -W1 -U1
-  elim (lifts_inv_bind2 … H2) -H2 #V2 #T2 #_ #_ #H destruct -W2 -U2
-  /1 width=1 by toeq_pair/
-| #I #W1 #W2 #U1 #U2 #f #X1 #H1 #X2 #H2
-  elim (lifts_inv_flat2 … H1) -H1 #V1 #T1 #_ #_ #H destruct -W1 -U1
-  elim (lifts_inv_flat2 … H2) -H2 #V2 #T2 #_ #_ #H destruct -W2 -U2
-  /1 width=1 by toeq_pair/
-]
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/static_2/static/frees_drops.ma b/matita/matita/contribs/lambdadelta/static_2/static/frees_drops.ma
index 5cbeaea87..698427fee 100644
--- a/matita/matita/contribs/lambdadelta/static_2/static/frees_drops.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/frees_drops.ma
@@ -48,16 +48,7 @@ lemma frees_unit_drops:
   #J #L #HLK #H destruct /3 width=1 by frees_lref/
 ]
 qed.
-(*
-lemma frees_sort_pushs:
-      ∀f,K,s. K ⊢ 𝐅+⦃⋆s⦄ ≘ f →
-      ∀i,L. ⇩*[i] L ≘ K → L ⊢ 𝐅+⦃⋆s⦄ ≘ ⫯*[i] f.
-#f #K #s #Hf #i elim i -i
-[ #L #H lapply (drops_fwd_isid … H ?) -H //
-| #i #IH #L #H elim (drops_inv_succ … H) -H /3 width=1 by frees_sort/
-]
-qed.
-*)
+
 lemma frees_lref_pushs:
       ∀f,K,j. K ⊢ 𝐅+⦃#j⦄ ≘ f →
       ∀i,L. ⇩*[i] L ≘ K → L ⊢ 𝐅+⦃#(i+j)⦄ ≘ ⫯*[i] f.
@@ -67,16 +58,7 @@ lemma frees_lref_pushs:
   #I #Y #HYK #H destruct /3 width=1 by frees_lref/
 ]
 qed.
-(*
-lemma frees_gref_pushs:
-      ∀f,K,l. K ⊢ 𝐅+⦃§l⦄ ≘ f →
-      ∀i,L. ⇩*[i] L ≘ K → L ⊢ 𝐅+⦃§l⦄ ≘ ⫯*[i] f.
-#f #K #l #Hf #i elim i -i
-[ #L #H lapply (drops_fwd_isid … H ?) -H //
-| #i #IH #L #H elim (drops_inv_succ … H) -H /3 width=1 by frees_gref/
-]
-qed.
-*)
+
 (* Advanced inversion lemmas ************************************************)
 
 lemma frees_inv_lref_drops:
diff --git a/matita/matita/contribs/lambdadelta/static_2/static/rdeq.ma b/matita/matita/contribs/lambdadelta/static_2/static/rdeq.ma
index 2e155d1ee..99fe14ee6 100644
--- a/matita/matita/contribs/lambdadelta/static_2/static/rdeq.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/rdeq.ma
@@ -99,11 +99,11 @@ lemma rdeq_sort: ∀I1,I2,L1,L2,s.
 lemma rdeq_pair: ∀I,L1,L2,V1,V2.
                  L1 ≛[V1] L2 → V1 ≛ V2 → L1.ⓑ{I}V1 ≛[#0] L2.ⓑ{I}V2.
 /2 width=1 by rex_pair/ qed.
-(*
-lemma rdeq_unit: ∀f,I,L1,L2. 𝐈⦃f⦄ → L1 ⪤[cdeq_ext,cfull,f] L2 →
+
+lemma rdeq_unit: ∀f,I,L1,L2. 𝐈⦃f⦄ → L1 ≛[f] L2 →
                  L1.ⓤ{I} ≛[#0] L2.ⓤ{I}.
 /2 width=3 by rex_unit/ qed.
-*)
+
 lemma rdeq_lref: ∀I1,I2,L1,L2,i.
                  L1 ≛[#i] L2 → L1.ⓘ{I1} ≛[#↑i] L2.ⓘ{I2}.
 /2 width=1 by rex_lref/ qed.
@@ -125,17 +125,16 @@ lemma rdeq_inv_atom_sn: ∀Y2. ∀T:term. ⋆ ≛[T] Y2 → Y2 = ⋆.
 
 lemma rdeq_inv_atom_dx: ∀Y1. ∀T:term. Y1 ≛[T] ⋆ → Y1 = ⋆.
 /2 width=3 by rex_inv_atom_dx/ qed-.
-(*
-lemma rdeq_inv_zero: ∀Y1,Y2. Y1 ≛[#0] Y2 →
-                     ∨∨ ∧∧ Y1 = ⋆ & Y2 = ⋆
-                      | ∃∃I,L1,L2,V1,V2. L1 ≛[V1] L2 & V1 ≛ V2 &
-                                         Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2
-                      | ∃∃f,I,L1,L2. 𝐈⦃f⦄ & L1 ⪤[cdeq_ext h o,cfull,f] L2 &
-                                         Y1 = L1.ⓤ{I} & Y2 = L2.ⓤ{I}.
+
+lemma rdeq_inv_zero:
+      ∀Y1,Y2. Y1 ≛[#0] Y2 →
+      ∨∨ ∧∧ Y1 = ⋆ & Y2 = ⋆
+       | ∃∃I,L1,L2,V1,V2. L1 ≛[V1] L2 & V1 ≛ V2 & Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2
+       | ∃∃f,I,L1,L2. 𝐈⦃f⦄ & L1 ≛[f] L2 & Y1 = L1.ⓤ{I} & Y2 = L2.ⓤ{I}.
 #Y1 #Y2 #H elim (rex_inv_zero … H) -H *
 /3 width=9 by or3_intro0, or3_intro1, or3_intro2, ex4_5_intro, ex4_4_intro, conj/
 qed-.
-*)
+
 lemma rdeq_inv_lref: ∀Y1,Y2,i. Y1 ≛[#↑i] Y2 →
                      ∨∨ ∧∧ Y1 = ⋆ & Y2 = ⋆
                       | ∃∃I1,I2,L1,L2. L1 ≛[#i] L2 &
diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/teqo.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/teqo.ma
new file mode 100644
index 000000000..9ac0ed76a
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/teqo.ma
@@ -0,0 +1,159 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/topiso_2.ma".
+include "static_2/syntax/term.ma".
+
+(* SORT-IRRELEVANT OUTER EQUIVALENCE FOR TERMS ******************************)
+
+(* Basic_2A1: includes: tsts_atom tsts_pair *)
+inductive teqo: relation term ≝
+| teqo_sort: ∀s1,s2. teqo (⋆s1) (⋆s2)
+| teqo_lref: ∀i. teqo (#i) (#i)
+| teqo_gref: ∀l. teqo (§l) (§l)
+| teqo_pair: ∀I,V1,V2,T1,T2. teqo (②{I}V1.T1) (②{I}V2.T2)
+.
+
+interpretation
+  "sort-irrelevant outer equivalence (term)"
+  'TopIso T1 T2 = (teqo T1 T2).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact teqo_inv_sort1_aux: ∀X,Y. X ⩳ Y → ∀s1. X = ⋆s1 →
+                         ∃s2. Y = ⋆s2.
+#X #Y * -X -Y
+[ #s1 #s2 #s #H destruct /2 width=2 by ex_intro/
+| #i #s #H destruct
+| #l #s #H destruct
+| #I #V1 #V2 #T1 #T2 #s #H destruct
+]
+qed-.
+
+(* Basic_1: was just: iso_gen_sort *)
+lemma teqo_inv_sort1: ∀Y,s1. ⋆s1 ⩳ Y →
+                      ∃s2. Y = ⋆s2.
+/2 width=4 by teqo_inv_sort1_aux/ qed-.
+
+fact teqo_inv_lref1_aux: ∀X,Y. X ⩳ Y → ∀i. X = #i → Y = #i.
+#X #Y * -X -Y //
+[ #s1 #s2 #j #H destruct
+| #I #V1 #V2 #T1 #T2 #j #H destruct
+]
+qed-.
+
+(* Basic_1: was: iso_gen_lref *)
+lemma teqo_inv_lref1: ∀Y,i. #i ⩳ Y → Y = #i.
+/2 width=5 by teqo_inv_lref1_aux/ qed-.
+
+fact teqo_inv_gref1_aux: ∀X,Y. X ⩳ Y → ∀l. X = §l → Y = §l.
+#X #Y * -X -Y //
+[ #s1 #s2 #k #H destruct
+| #I #V1 #V2 #T1 #T2 #k #H destruct
+]
+qed-.
+
+lemma teqo_inv_gref1: ∀Y,l. §l ⩳ Y → Y = §l.
+/2 width=5 by teqo_inv_gref1_aux/ qed-.
+
+fact teqo_inv_pair1_aux: ∀T1,T2. T1 ⩳ T2 →
+                         ∀J,W1,U1. T1 = ②{J}W1.U1 →
+                         ∃∃W2,U2. T2 = ②{J}W2.U2.
+#T1 #T2 * -T1 -T2
+[ #s1 #s2 #J #W1 #U1 #H destruct
+| #i #J #W1 #U1 #H destruct
+| #l #J #W1 #U1 #H destruct
+| #I #V1 #V2 #T1 #T2 #J #W1 #U1 #H destruct /2 width=3 by ex1_2_intro/
+]
+qed-.
+
+(* Basic_1: was: iso_gen_head *)
+(* Basic_2A1: was: tsts_inv_pair1 *)
+lemma teqo_inv_pair1: ∀J,W1,U1,T2. ②{J}W1.U1 ⩳ T2 →
+                      ∃∃W2,U2. T2 = ②{J}W2. U2.
+/2 width=7 by teqo_inv_pair1_aux/ qed-.
+
+fact teqo_inv_pair2_aux: ∀T1,T2. T1 ⩳ T2 →
+                         ∀J,W2,U2. T2 = ②{J}W2.U2 →
+                         ∃∃W1,U1. T1 = ②{J}W1.U1.
+#T1 #T2 * -T1 -T2
+[ #s1 #s2 #J #W2 #U2 #H destruct
+| #i #J #W2 #U2 #H destruct
+| #l #J #W2 #U2 #H destruct
+| #I #V1 #V2 #T1 #T2 #J #W2 #U2 #H destruct /2 width=3 by ex1_2_intro/
+]
+qed-.
+
+(* Basic_2A1: was: tsts_inv_pair2 *)
+lemma teqo_inv_pair2: ∀J,T1,W2,U2. T1 ⩳ ②{J}W2.U2 →
+                      ∃∃W1,U1. T1 = ②{J}W1.U1.
+/2 width=7 by teqo_inv_pair2_aux/ qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma teqo_inv_pair: ∀I1,I2,V1,V2,T1,T2. ②{I1}V1.T1 ⩳ ②{I2}V2.T2 →
+                     I1 = I2.
+#I1 #I2 #V1 #V2 #T1 #T2 #H elim (teqo_inv_pair1 … H) -H
+#V0 #T0 #H destruct //
+qed-.
+
+(* Basic properties *********************************************************)
+
+(* Basic_1: was: iso_refl *)
+(* Basic_2A1: was: tsts_refl *)
+lemma teqo_refl: reflexive … teqo.
+* //
+* /2 width=1 by teqo_lref, teqo_gref/
+qed.
+
+(* Basic_2A1: was: tsts_sym *)
+lemma teqo_sym: symmetric … teqo.
+#T1 #T2 * -T1 -T2 /2 width=3 by teqo_sort/
+qed-.
+
+(* Basic_2A1: was: tsts_dec *)
+lemma teqo_dec: ∀T1,T2. Decidable (T1 ⩳ T2).
+* [ * #s1 | #I1 #V1 #T1 ] * [1,3,5,7: * #s2 |*: #I2 #V2 #T2 ]
+[ /3 width=1 by teqo_sort, or_introl/
+|2,3,13:
+  @or_intror #H
+  elim (teqo_inv_sort1 … H) -H #x #H destruct
+|4,6,14:
+  @or_intror #H
+  lapply (teqo_inv_lref1 … H) -H #H destruct
+|5:
+  elim (eq_nat_dec s1 s2) #Hs12 destruct /2 width=1 by or_introl/
+  @or_intror #H
+  lapply (teqo_inv_lref1 … H) -H #H destruct /2 width=1 by/
+|7,8,15:
+  @or_intror #H
+  lapply (teqo_inv_gref1 … H) -H #H destruct
+|9:
+  elim (eq_nat_dec s1 s2) #Hs12 destruct /2 width=1 by or_introl/
+  @or_intror #H
+  lapply (teqo_inv_gref1 … H) -H #H destruct /2 width=1 by/
+|10,11,12:
+  @or_intror #H
+  elim (teqo_inv_pair1 … H) -H #X1 #X2 #H destruct
+|16:
+  elim (eq_item2_dec I1 I2) #HI12 destruct
+  [ /3 width=1 by teqo_pair, or_introl/ ]
+  @or_intror #H
+  lapply (teqo_inv_pair … H) -H /2 width=1 by/
+]
+qed-.
+
+(* Basic_2A1: removed theorems 2:
+              tsts_inv_atom1 tsts_inv_atom2
+*)
diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/teqo_simple.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/teqo_simple.ma
new file mode 100644
index 000000000..8159a89f3
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/teqo_simple.ma
@@ -0,0 +1,31 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/term_simple.ma".
+include "static_2/syntax/teqo.ma".
+
+(* SORT-IRRELEVANT OUTER EQUIVALENCE FOR TERMS ******************************)
+
+(* Properies with simple (neutral) terms ************************************)
+
+(* Basic_2A1: was: simple_tsts_repl_dx *)
+lemma simple_teqo_repl_dx: ∀T1,T2. T1 ⩳ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄.
+#T1 #T2 * -T1 -T2 //
+#I #V1 #V2 #T1 #T2 #H
+elim (simple_inv_pair … H) -H #J #H destruct //
+qed-.
+
+(* Basic_2A1: was: simple_tsts_repl_sn *)
+lemma simple_teqo_repl_sn: ∀T1,T2. T1 ⩳ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄.
+/3 width=3 by simple_teqo_repl_dx, teqo_sym/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/teqo_simple_vector.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/teqo_simple_vector.ma
new file mode 100644
index 000000000..43ea6c691
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/teqo_simple_vector.ma
@@ -0,0 +1,31 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/term_vector.ma".
+include "static_2/syntax/teqo_simple.ma".
+
+(* SORT-IRRELEVANT OUTER EQUIVALENCE FOR TERMS ******************************)
+
+(* Advanced inversion lemmas with simple (neutral) terms ********************)
+
+(* Basic_1: was only: iso_flats_lref_bind_false iso_flats_flat_bind_false *)
+(* Basic_2A1: was: tsts_inv_bind_applv_simple *)
+lemma teqo_inv_applv_bind_simple (p) (I):
+      ∀Vs,V2,T1,T2. ⒶVs.T1 ⩳ ⓑ{p,I}V2.T2 → 𝐒⦃T1⦄ → ⊥.
+#p #I #Vs #V2 #T1 #T2 #H elim (teqo_inv_pair2 … H) -H
+#V0 #T0 elim Vs -Vs normalize
+[ #H destruct #H /2 width=5 by simple_inv_bind/
+| #V #Vs #_ #H destruct
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/teqo_tdeq.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/teqo_tdeq.ma
new file mode 100644
index 000000000..a0a93b9bd
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/teqo_tdeq.ma
@@ -0,0 +1,24 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "static_2/syntax/tdeq.ma".
+include "static_2/syntax/teqo.ma".
+
+(* SORT-IRRELEVANT OUTER EQUIVALENCE FOR TERMS ******************************)
+
+(* Properties with sort-irrelevant equivalence for terms ********************)
+
+lemma tdeq_teqo: ∀T1,T2. T1 ≛ T2 → T1 ⩳ T2.
+#T1 #T2 * -T1 -T2 /2 width=1 by teqo_sort, teqo_pair/
+qed.
diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/teqo_teqo.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/teqo_teqo.ma
new file mode 100644
index 000000000..c3d6d0c3a
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/teqo_teqo.ma
@@ -0,0 +1,40 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/teqo.ma".
+
+(* SORT-IRRELEVANT OUTER EQUIVALENCE FOR TERMS ******************************)
+
+(* Main properties **********************************************************)
+
+(* Basic_1: was: iso_trans *)
+(* Basic_2A1: was: tsts_trans *)
+theorem teqo_trans: Transitive … teqo.
+#T1 #T * -T1 -T
+[ #s1 #s #X #H
+  elim (teqo_inv_sort1 … H) -s /2 width=1 by teqo_sort/
+| #i1 #i #H <(teqo_inv_lref1 … H) -H //
+| #l1 #l #H <(teqo_inv_gref1 … H) -H //
+| #I #V1 #V #T1 #T #X #H
+  elim (teqo_inv_pair1 … H) -H #V2 #T2 #H destruct //
+]
+qed-.
+
+(* Basic_2A1: was: tsts_canc_sn *)
+theorem teqo_canc_sn: left_cancellable … teqo.
+/3 width=3 by teqo_trans, teqo_sym/ qed-.
+
+(* Basic_2A1: was: tsts_canc_dx *)
+theorem teqo_canc_dx: right_cancellable … teqo.
+/3 width=3 by teqo_trans, teqo_sym/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/toeq.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/toeq.ma
deleted file mode 100644
index 7206a1d62..000000000
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/toeq.ma
+++ /dev/null
@@ -1,159 +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/topiso_2.ma".
-include "static_2/syntax/term.ma".
-
-(* SORT-IRRELEVANT OUTER EQUIVALENCE FOR TERMS ******************************)
-
-(* Basic_2A1: includes: tsts_atom tsts_pair *)
-inductive toeq: relation term ≝
-| toeq_sort: ∀s1,s2. toeq (⋆s1) (⋆s2)
-| toeq_lref: ∀i. toeq (#i) (#i)
-| toeq_gref: ∀l. toeq (§l) (§l)
-| toeq_pair: ∀I,V1,V2,T1,T2. toeq (②{I}V1.T1) (②{I}V2.T2)
-.
-
-interpretation
-  "sort-irrelevant outer equivalence (term)"
-  'TopIso T1 T2 = (toeq T1 T2).
-
-(* Basic inversion lemmas ***************************************************)
-
-fact toeq_inv_sort1_aux: ∀X,Y. X ⩳ Y → ∀s1. X = ⋆s1 →
-                         ∃s2. Y = ⋆s2.
-#X #Y * -X -Y
-[ #s1 #s2 #s #H destruct /2 width=2 by ex_intro/
-| #i #s #H destruct
-| #l #s #H destruct
-| #I #V1 #V2 #T1 #T2 #s #H destruct
-]
-qed-.
-
-(* Basic_1: was just: iso_gen_sort *)
-lemma toeq_inv_sort1: ∀Y,s1. ⋆s1 ⩳ Y →
-                      ∃s2. Y = ⋆s2.
-/2 width=4 by toeq_inv_sort1_aux/ qed-.
-
-fact toeq_inv_lref1_aux: ∀X,Y. X ⩳ Y → ∀i. X = #i → Y = #i.
-#X #Y * -X -Y //
-[ #s1 #s2 #j #H destruct
-| #I #V1 #V2 #T1 #T2 #j #H destruct
-]
-qed-.
-
-(* Basic_1: was: iso_gen_lref *)
-lemma toeq_inv_lref1: ∀Y,i. #i ⩳ Y → Y = #i.
-/2 width=5 by toeq_inv_lref1_aux/ qed-.
-
-fact toeq_inv_gref1_aux: ∀X,Y. X ⩳ Y → ∀l. X = §l → Y = §l.
-#X #Y * -X -Y //
-[ #s1 #s2 #k #H destruct
-| #I #V1 #V2 #T1 #T2 #k #H destruct
-]
-qed-.
-
-lemma toeq_inv_gref1: ∀Y,l. §l ⩳ Y → Y = §l.
-/2 width=5 by toeq_inv_gref1_aux/ qed-.
-
-fact toeq_inv_pair1_aux: ∀T1,T2. T1 ⩳ T2 →
-                         ∀J,W1,U1. T1 = ②{J}W1.U1 →
-                         ∃∃W2,U2. T2 = ②{J}W2.U2.
-#T1 #T2 * -T1 -T2
-[ #s1 #s2 #J #W1 #U1 #H destruct
-| #i #J #W1 #U1 #H destruct
-| #l #J #W1 #U1 #H destruct
-| #I #V1 #V2 #T1 #T2 #J #W1 #U1 #H destruct /2 width=3 by ex1_2_intro/
-]
-qed-.
-
-(* Basic_1: was: iso_gen_head *)
-(* Basic_2A1: was: tsts_inv_pair1 *)
-lemma toeq_inv_pair1: ∀J,W1,U1,T2. ②{J}W1.U1 ⩳ T2 →
-                      ∃∃W2,U2. T2 = ②{J}W2. U2.
-/2 width=7 by toeq_inv_pair1_aux/ qed-.
-
-fact toeq_inv_pair2_aux: ∀T1,T2. T1 ⩳ T2 →
-                         ∀J,W2,U2. T2 = ②{J}W2.U2 →
-                         ∃∃W1,U1. T1 = ②{J}W1.U1.
-#T1 #T2 * -T1 -T2
-[ #s1 #s2 #J #W2 #U2 #H destruct
-| #i #J #W2 #U2 #H destruct
-| #l #J #W2 #U2 #H destruct
-| #I #V1 #V2 #T1 #T2 #J #W2 #U2 #H destruct /2 width=3 by ex1_2_intro/
-]
-qed-.
-
-(* Basic_2A1: was: tsts_inv_pair2 *)
-lemma toeq_inv_pair2: ∀J,T1,W2,U2. T1 ⩳ ②{J}W2.U2 →
-                      ∃∃W1,U1. T1 = ②{J}W1.U1.
-/2 width=7 by toeq_inv_pair2_aux/ qed-.
-
-(* Advanced inversion lemmas ************************************************)
-
-lemma toeq_inv_pair: ∀I1,I2,V1,V2,T1,T2. ②{I1}V1.T1 ⩳ ②{I2}V2.T2 →
-                     I1 = I2.
-#I1 #I2 #V1 #V2 #T1 #T2 #H elim (toeq_inv_pair1 … H) -H
-#V0 #T0 #H destruct //
-qed-.
-
-(* Basic properties *********************************************************)
-
-(* Basic_1: was: iso_refl *)
-(* Basic_2A1: was: tsts_refl *)
-lemma toeq_refl: reflexive … toeq.
-* //
-* /2 width=1 by toeq_lref, toeq_gref/
-qed.
-
-(* Basic_2A1: was: tsts_sym *)
-lemma toeq_sym: symmetric … toeq.
-#T1 #T2 * -T1 -T2 /2 width=3 by toeq_sort/
-qed-.
-
-(* Basic_2A1: was: tsts_dec *)
-lemma toeq_dec: ∀T1,T2. Decidable (T1 ⩳ T2).
-* [ * #s1 | #I1 #V1 #T1 ] * [1,3,5,7: * #s2 |*: #I2 #V2 #T2 ]
-[ /3 width=1 by toeq_sort, or_introl/
-|2,3,13:
-  @or_intror #H
-  elim (toeq_inv_sort1 … H) -H #x #H destruct
-|4,6,14:
-  @or_intror #H
-  lapply (toeq_inv_lref1 … H) -H #H destruct
-|5:
-  elim (eq_nat_dec s1 s2) #Hs12 destruct /2 width=1 by or_introl/
-  @or_intror #H
-  lapply (toeq_inv_lref1 … H) -H #H destruct /2 width=1 by/
-|7,8,15:
-  @or_intror #H
-  lapply (toeq_inv_gref1 … H) -H #H destruct
-|9:
-  elim (eq_nat_dec s1 s2) #Hs12 destruct /2 width=1 by or_introl/
-  @or_intror #H
-  lapply (toeq_inv_gref1 … H) -H #H destruct /2 width=1 by/
-|10,11,12:
-  @or_intror #H
-  elim (toeq_inv_pair1 … H) -H #X1 #X2 #H destruct
-|16:
-  elim (eq_item2_dec I1 I2) #HI12 destruct
-  [ /3 width=1 by toeq_pair, or_introl/ ]
-  @or_intror #H
-  lapply (toeq_inv_pair … H) -H /2 width=1 by/
-]
-qed-.
-
-(* Basic_2A1: removed theorems 2:
-              tsts_inv_atom1 tsts_inv_atom2
-*)
diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/toeq_simple.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/toeq_simple.ma
deleted file mode 100644
index 00d96949c..000000000
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/toeq_simple.ma
+++ /dev/null
@@ -1,31 +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/term_simple.ma".
-include "static_2/syntax/toeq.ma".
-
-(* SORT-IRRELEVANT OUTER EQUIVALENCE FOR TERMS ******************************)
-
-(* Properies with simple (neutral) terms ************************************)
-
-(* Basic_2A1: was: simple_tsts_repl_dx *)
-lemma simple_toeq_repl_dx: ∀T1,T2. T1 ⩳ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄.
-#T1 #T2 * -T1 -T2 //
-#I #V1 #V2 #T1 #T2 #H
-elim (simple_inv_pair … H) -H #J #H destruct //
-qed-.
-
-(* Basic_2A1: was: simple_tsts_repl_sn *)
-lemma simple_toeq_repl_sn: ∀T1,T2. T1 ⩳ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄.
-/3 width=3 by simple_toeq_repl_dx, toeq_sym/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/toeq_simple_vector.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/toeq_simple_vector.ma
deleted file mode 100644
index 92e28c878..000000000
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/toeq_simple_vector.ma
+++ /dev/null
@@ -1,31 +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/term_vector.ma".
-include "static_2/syntax/toeq_simple.ma".
-
-(* SORT-IRRELEVANT OUTER EQUIVALENCE FOR TERMS ******************************)
-
-(* Advanced inversion lemmas with simple (neutral) terms ********************)
-
-(* Basic_1: was only: iso_flats_lref_bind_false iso_flats_flat_bind_false *)
-(* Basic_2A1: was: tsts_inv_bind_applv_simple *)
-lemma toeq_inv_applv_bind_simple (p) (I):
-      ∀Vs,V2,T1,T2. ⒶVs.T1 ⩳ ⓑ{p,I}V2.T2 → 𝐒⦃T1⦄ → ⊥.
-#p #I #Vs #V2 #T1 #T2 #H elim (toeq_inv_pair2 … H) -H
-#V0 #T0 elim Vs -Vs normalize
-[ #H destruct #H /2 width=5 by simple_inv_bind/
-| #V #Vs #_ #H destruct
-]
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/toeq_tdeq.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/toeq_tdeq.ma
deleted file mode 100644
index 73be8f600..000000000
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/toeq_tdeq.ma
+++ /dev/null
@@ -1,24 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "static_2/syntax/tdeq.ma".
-include "static_2/syntax/toeq.ma".
-
-(* SORT-IRRELEVANT OUTER EQUIVALENCE FOR TERMS ******************************)
-
-(* Properties with sort-irrelevant equivalence for terms ********************)
-
-lemma tdeq_toeq: ∀T1,T2. T1 ≛ T2 → T1 ⩳ T2.
-#T1 #T2 * -T1 -T2 /2 width=1 by toeq_sort, toeq_pair/
-qed.
diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/toeq_toeq.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/toeq_toeq.ma
deleted file mode 100644
index 9b7af0a51..000000000
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/toeq_toeq.ma
+++ /dev/null
@@ -1,40 +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/toeq.ma".
-
-(* SORT-IRRELEVANT OUTER EQUIVALENCE FOR TERMS ******************************)
-
-(* Main properties **********************************************************)
-
-(* Basic_1: was: iso_trans *)
-(* Basic_2A1: was: tsts_trans *)
-theorem toeq_trans: Transitive … toeq.
-#T1 #T * -T1 -T
-[ #s1 #s #X #H
-  elim (toeq_inv_sort1 … H) -s /2 width=1 by toeq_sort/
-| #i1 #i #H <(toeq_inv_lref1 … H) -H //
-| #l1 #l #H <(toeq_inv_gref1 … H) -H //
-| #I #V1 #V #T1 #T #X #H
-  elim (toeq_inv_pair1 … H) -H #V2 #T2 #H destruct //
-]
-qed-.
-
-(* Basic_2A1: was: tsts_canc_sn *)
-theorem toeq_canc_sn: left_cancellable … toeq.
-/3 width=3 by toeq_trans, toeq_sym/ qed-.
-
-(* Basic_2A1: was: tsts_canc_dx *)
-theorem toeq_canc_dx: right_cancellable … toeq.
-/3 width=3 by toeq_trans, toeq_sym/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl b/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl
index 44690009a..627162218 100644
--- a/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl
@@ -86,7 +86,7 @@ table {
         [ { "generic and uniform relocation" * } {
              [ [ "for binders" ] "lifts_bind" + "( ⇧*[?] ? ≘ ? )" "lifts_weight_bind" + "lifts_lifts_bind" * ]
              [ [ "for term vectors" ] "lifts_vector" + "( ⇧*[?] ? ≘ ? )" "lifts_lifts_vector" * ]
-             [ [ "for terms" ] "lifts" + "( ⇧*[?] ? ≘ ? )" "lifts_simple" + "lifts_weight" + "lifts_tdeq" + "lifts_tweq" + "lifts_toeq" + "lifts_lifts" * ]
+             [ [ "for terms" ] "lifts" + "( ⇧*[?] ? ≘ ? )" "lifts_simple" + "lifts_weight" + "lifts_tdeq" + "lifts_tweq" + "lifts_teqo" + "lifts_lifts" * ]
           }
         ]
         [ { "syntactic equivalence" * } {
@@ -117,7 +117,7 @@ table {
           }
         ]
         [ { "sort-irrelevant outer equivalence" * } {
-             [ [ "for terms" ] "toeq" + "( ? ⩳ ? )" "toeq_simple" + "toeq_tdeq" + "toeq_toeq" + "toeq_simple_vector" * ]
+             [ [ "for terms" ] "teqo" + "( ? ⩳ ? )" "teqo_simple" + "teqo_tdeq" + "teqo_teqo" + "teqo_simple_vector" * ]
           }
         ]
         [ { "sort-irrelevant whd equivalence" * } {