From f677b4ef7fa20f1ab36c5ee59598865d5c1b719b Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
Date: Fri, 15 Nov 2019 16:22:29 +0100
Subject: [PATCH] update in static_2 and basic_2 for the article

+ commented theorems activated or parked
+ some renaming to match the article
---
 .../lambdadelta/basic_2/etc/cnuw_simple.etc   |  7 ++
 .../lambdadelta/basic_2/etc/cpx_req.etc       | 13 ++++
 .../lambdadelta/basic_2/etc/ntas_nta.etc      | 11 +++
 .../lambdadelta/basic_2/i_dynamic/ntas_nta.ma | 14 +---
 .../basic_2/rt_computation/cnuw_simple.ma     |  7 --
 .../{cpxs_toeq.ma => cpxs_teqo.ma}            | 10 +--
 ...pxs_toeq_vector.ma => cpxs_teqo_vector.ma} | 40 +++++-----
 .../basic_2/rt_computation/csx_cnx_vector.ma  |  6 +-
 .../basic_2/rt_computation/csx_csx_vector.ma  | 12 +--
 ...{csx_simple_toeq.ma => csx_simple_teqo.ma} | 10 +--
 .../basic_2/rt_transition/cpx_req.ma          | 17 +----
 .../lambdadelta/basic_2/web/basic_2_src.tbl   |  4 +-
 matita/matita/contribs/lambdadelta/refile.sh  |  8 ++
 .../lambdadelta/static_2/etc/frees_drops.etc  | 17 +++++
 .../{lifts_toeq.ma => lifts_teqo.ma}          | 34 ++++-----
 .../static_2/static/frees_drops.ma            | 22 +-----
 .../lambdadelta/static_2/static/rdeq.ma       | 21 +++---
 .../static_2/syntax/{toeq.ma => teqo.ma}      | 74 +++++++++----------
 .../syntax/{toeq_simple.ma => teqo_simple.ma} |  8 +-
 ...simple_vector.ma => teqo_simple_vector.ma} |  6 +-
 .../syntax/{toeq_tdeq.ma => teqo_tdeq.ma}     |  6 +-
 .../syntax/{toeq_toeq.ma => teqo_teqo.ma}     | 20 ++---
 .../lambdadelta/static_2/web/static_2_src.tbl |  4 +-
 23 files changed, 189 insertions(+), 182 deletions(-)
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/cnuw_simple.etc
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/cpx_req.etc
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/ntas_nta.etc
 rename matita/matita/contribs/lambdadelta/basic_2/rt_computation/{cpxs_toeq.ma => cpxs_teqo.ma} (94%)
 rename matita/matita/contribs/lambdadelta/basic_2/rt_computation/{cpxs_toeq_vector.ma => cpxs_teqo_vector.ma} (87%)
 rename matita/matita/contribs/lambdadelta/basic_2/rt_computation/{csx_simple_toeq.ma => csx_simple_teqo.ma} (89%)
 create mode 100644 matita/matita/contribs/lambdadelta/refile.sh
 create mode 100644 matita/matita/contribs/lambdadelta/static_2/etc/frees_drops.etc
 rename matita/matita/contribs/lambdadelta/static_2/relocation/{lifts_toeq.ma => lifts_teqo.ma} (79%)
 rename matita/matita/contribs/lambdadelta/static_2/syntax/{toeq.ma => teqo.ma} (66%)
 rename matita/matita/contribs/lambdadelta/static_2/syntax/{toeq_simple.ma => teqo_simple.ma} (86%)
 rename matita/matita/contribs/lambdadelta/static_2/syntax/{toeq_simple_vector.ma => teqo_simple_vector.ma} (91%)
 rename matita/matita/contribs/lambdadelta/static_2/syntax/{toeq_tdeq.ma => teqo_tdeq.ma} (89%)
 rename matita/matita/contribs/lambdadelta/static_2/syntax/{toeq_toeq.ma => teqo_teqo.ma} (74%)

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_toeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqo.ma
similarity index 94%
rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_toeq.ma
rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqo.ma
index 8b6725af0..1de400dad 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_toeq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqo.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "static_2/syntax/toeq_tdeq.ma".
+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".
@@ -46,7 +46,7 @@ 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/
+[ #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
@@ -62,7 +62,7 @@ lemma cpxs_fwd_theta (h) (p) (G) (L):
            ∨∨ ⓐ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/
+[ -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
@@ -93,10 +93,10 @@ lemma cpxs_fwd_cast (h) (G) (L):
       ∨∨ ⓝ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/
+#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_toeq/ qed-.
+/3 width=5 by cpxs_inv_cnx1, tdeq_teqo/ 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_teqo_vector.ma
similarity index 87%
rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_toeq_vector.ma
rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqo_vector.ma
index 20702a354..5b7135b01 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_toeq_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqo_vector.ma
@@ -12,9 +12,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "static_2/syntax/toeq_simple_vector.ma".
+include "static_2/syntax/teqo_simple_vector.ma".
 include "static_2/relocation/lifts_vector.ma".
-include "basic_2/rt_computation/cpxs_toeq.ma".
+include "basic_2/rt_computation/cpxs_teqo.ma".
 
 (* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
 
@@ -25,13 +25,13 @@ lemma cpxs_fwd_sort_vector (h) (G) (L):
 #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/
+[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1 by teqo_pair/
 | #p #W1 #T1 #HT1 #HU
   lapply (IHVs … HT1) -IHVs -HT1 #HT1
-  elim (toeq_inv_applv_bind_simple … HT1) //
+  elim (teqo_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) //
+  elim (teqo_inv_applv_bind_simple … HT1) //
 ]
 qed-.
 
@@ -45,17 +45,17 @@ lemma cpxs_fwd_delta_drops_vector (h) (I) (G) (L) (K):
 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/
+[ -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 (toeq_inv_applv_bind_simple … 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 (toeq_inv_applv_bind_simple … 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/
@@ -70,17 +70,17 @@ lemma cpxs_fwd_beta_vector (h) (p) (G) (L):
 #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/
+[ -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 (toeq_inv_applv_bind_simple … 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 (toeq_inv_applv_bind_simple … 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/
@@ -101,11 +101,11 @@ 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/
+[ -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 (toeq_inv_pair1 … HT0) #V1 #T1 #H destruct
+    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 *
@@ -120,7 +120,7 @@ elim (cpxs_inv_appl1 … H) -H *
 | #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
+    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 *
@@ -147,9 +147,9 @@ lemma cpxs_fwd_cast_vector (h) (G) (L):
 #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/
+[ -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 (toeq_inv_applv_bind_simple … 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/
@@ -159,7 +159,7 @@ elim (cpxs_inv_appl1 … H) -H *
   ]
 | #q #V0 #V1 #V2 #T0 #HV0 #HV01 #HT0 #HU
   elim (IHVs … HT0) -IHVs -HT0 #HT0
-  [ elim (toeq_inv_applv_bind_simple … 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/
@@ -177,12 +177,12 @@ lemma cpxs_fwd_cnx_vector (h) (G) (L):
 #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/
+[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by teqo_pair/
 | #p #W0 #T0 #HT0 #HU
   lapply (IHVs … HT0) -IHVs -HT0 #HT0
-  elim (toeq_inv_applv_bind_simple … HT0) //
+  elim (teqo_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) //
+  elim (teqo_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_toeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple_teqo.ma
similarity index 89%
rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple_toeq.ma
rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple_teqo.ma
index 8fb338684..c56f1f718 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple_toeq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple_teqo.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "static_2/syntax/toeq_simple.ma".
-include "static_2/syntax/toeq_toeq.ma".
+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".
@@ -24,7 +24,7 @@ include "basic_2/rt_computation/csx_csx.ma".
 
 (* Basic_1: was just: sn3_appl_appl *)
 (* Basic_2A1: was: csx_appl_simple_tsts *)
-lemma csx_appl_simple_toeq (h) (G) (L):
+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⦄.
@@ -41,8 +41,8 @@ elim (tdneq_inv_pair … H) -H
   @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/
+  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/
   ]
 ]
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_toeq.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_teqo.ma
similarity index 79%
rename from matita/matita/contribs/lambdadelta/static_2/relocation/lifts_toeq.ma
rename to matita/matita/contribs/lambdadelta/static_2/relocation/lifts_teqo.ma
index ffbddcbe4..be9437843 100644
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_toeq.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_teqo.ma
@@ -12,65 +12,65 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "static_2/syntax/toeq.ma".
+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 toeq_lifts_sn: liftable2_sn toeq.
+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 toeq_sort, ex2_intro/
+  /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 toeq_lref, lifts_lref, ex2_intro/
+  /3 width=3 by teqo_lref, lifts_lref, ex2_intro/
 | #l #f #X #H
   >(lifts_inv_gref1 … H) -H
-  /2 width=3 by toeq_gref, ex2_intro/
+  /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 toeq_pair, lifts_bind, ex2_intro/
+  /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 toeq_pair, lifts_flat, ex2_intro/
+  /3 width=3 by teqo_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 teqo_lifts_dx: liftable2_dx teqo.
+/3 width=3 by teqo_lifts_sn, liftable2_sn_dx, teqo_sym/ qed-.
 
-lemma toeq_lifts_bi: liftable2_bi toeq.
-/3 width=6 by toeq_lifts_sn, liftable2_sn_bi/ 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 toeq_inv_lifts_bi: deliftable2_bi toeq.
+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 toeq_sort/
+  /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 toeq_lref/
+  /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 toeq_gref/
+  /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 toeq_pair/
+  /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 toeq_pair/
+  /1 width=1 by teqo_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/toeq.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/teqo.ma
similarity index 66%
rename from matita/matita/contribs/lambdadelta/static_2/syntax/toeq.ma
rename to matita/matita/contribs/lambdadelta/static_2/syntax/teqo.ma
index 7206a1d62..9ac0ed76a 100644
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/toeq.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/teqo.ma
@@ -18,20 +18,20 @@ 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)
+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 = (toeq T1 T2).
+  'TopIso T1 T2 = (teqo T1 T2).
 
 (* Basic inversion lemmas ***************************************************)
 
-fact toeq_inv_sort1_aux: ∀X,Y. X ⩳ Y → ∀s1. X = ⋆s1 →
+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/
@@ -42,11 +42,11 @@ fact toeq_inv_sort1_aux: ∀X,Y. X ⩳ Y → ∀s1. X = ⋆s1 →
 qed-.
 
 (* Basic_1: was just: iso_gen_sort *)
-lemma toeq_inv_sort1: ∀Y,s1. ⋆s1 ⩳ Y →
+lemma teqo_inv_sort1: ∀Y,s1. ⋆s1 ⩳ Y →
                       ∃s2. Y = ⋆s2.
-/2 width=4 by toeq_inv_sort1_aux/ qed-.
+/2 width=4 by teqo_inv_sort1_aux/ qed-.
 
-fact toeq_inv_lref1_aux: ∀X,Y. X ⩳ Y → ∀i. X = #i → Y = #i.
+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
@@ -54,20 +54,20 @@ fact toeq_inv_lref1_aux: ∀X,Y. X ⩳ Y → ∀i. X = #i → Y = #i.
 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-.
+lemma teqo_inv_lref1: ∀Y,i. #i ⩳ Y → Y = #i.
+/2 width=5 by teqo_inv_lref1_aux/ qed-.
 
-fact toeq_inv_gref1_aux: ∀X,Y. X ⩳ Y → ∀l. X = §l → Y = §l.
+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 toeq_inv_gref1: ∀Y,l. §l ⩳ Y → Y = §l.
-/2 width=5 by toeq_inv_gref1_aux/ qed-.
+lemma teqo_inv_gref1: ∀Y,l. §l ⩳ Y → Y = §l.
+/2 width=5 by teqo_inv_gref1_aux/ qed-.
 
-fact toeq_inv_pair1_aux: ∀T1,T2. T1 ⩳ T2 →
+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
@@ -80,11 +80,11 @@ 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 →
+lemma teqo_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-.
+/2 width=7 by teqo_inv_pair1_aux/ qed-.
 
-fact toeq_inv_pair2_aux: ∀T1,T2. T1 ⩳ T2 →
+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
@@ -96,15 +96,15 @@ fact toeq_inv_pair2_aux: ∀T1,T2. T1 ⩳ T2 →
 qed-.
 
 (* Basic_2A1: was: tsts_inv_pair2 *)
-lemma toeq_inv_pair2: ∀J,T1,W2,U2. T1 ⩳ ②{J}W2.U2 →
+lemma teqo_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-.
+/2 width=7 by teqo_inv_pair2_aux/ qed-.
 
 (* Advanced inversion lemmas ************************************************)
 
-lemma toeq_inv_pair: ∀I1,I2,V1,V2,T1,T2. ②{I1}V1.T1 ⩳ ②{I2}V2.T2 →
+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 (toeq_inv_pair1 … H) -H
+#I1 #I2 #V1 #V2 #T1 #T2 #H elim (teqo_inv_pair1 … H) -H
 #V0 #T0 #H destruct //
 qed-.
 
@@ -112,45 +112,45 @@ qed-.
 
 (* Basic_1: was: iso_refl *)
 (* Basic_2A1: was: tsts_refl *)
-lemma toeq_refl: reflexive … toeq.
+lemma teqo_refl: reflexive … teqo.
 * //
-* /2 width=1 by toeq_lref, toeq_gref/
+* /2 width=1 by teqo_lref, teqo_gref/
 qed.
 
 (* Basic_2A1: was: tsts_sym *)
-lemma toeq_sym: symmetric … toeq.
-#T1 #T2 * -T1 -T2 /2 width=3 by toeq_sort/
+lemma teqo_sym: symmetric … teqo.
+#T1 #T2 * -T1 -T2 /2 width=3 by teqo_sort/
 qed-.
 
 (* Basic_2A1: was: tsts_dec *)
-lemma toeq_dec: ∀T1,T2. Decidable (T1 ⩳ T2).
+lemma teqo_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/
+[ /3 width=1 by teqo_sort, or_introl/
 |2,3,13:
   @or_intror #H
-  elim (toeq_inv_sort1 … H) -H #x #H destruct
+  elim (teqo_inv_sort1 … H) -H #x #H destruct
 |4,6,14:
   @or_intror #H
-  lapply (toeq_inv_lref1 … H) -H #H destruct
+  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 (toeq_inv_lref1 … H) -H #H destruct /2 width=1 by/
+  lapply (teqo_inv_lref1 … H) -H #H destruct /2 width=1 by/
 |7,8,15:
   @or_intror #H
-  lapply (toeq_inv_gref1 … H) -H #H destruct
+  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 (toeq_inv_gref1 … H) -H #H destruct /2 width=1 by/
+  lapply (teqo_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
+  elim (teqo_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/ ]
+  [ /3 width=1 by teqo_pair, or_introl/ ]
   @or_intror #H
-  lapply (toeq_inv_pair … H) -H /2 width=1 by/
+  lapply (teqo_inv_pair … H) -H /2 width=1 by/
 ]
 qed-.
 
diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/toeq_simple.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/teqo_simple.ma
similarity index 86%
rename from matita/matita/contribs/lambdadelta/static_2/syntax/toeq_simple.ma
rename to matita/matita/contribs/lambdadelta/static_2/syntax/teqo_simple.ma
index 00d96949c..8159a89f3 100644
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/toeq_simple.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/teqo_simple.ma
@@ -13,19 +13,19 @@
 (**************************************************************************)
 
 include "static_2/syntax/term_simple.ma".
-include "static_2/syntax/toeq.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_toeq_repl_dx: ∀T1,T2. T1 ⩳ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄.
+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_toeq_repl_sn: ∀T1,T2. T1 ⩳ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄.
-/3 width=3 by simple_toeq_repl_dx, toeq_sym/ qed-.
+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/toeq_simple_vector.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/teqo_simple_vector.ma
similarity index 91%
rename from matita/matita/contribs/lambdadelta/static_2/syntax/toeq_simple_vector.ma
rename to matita/matita/contribs/lambdadelta/static_2/syntax/teqo_simple_vector.ma
index 92e28c878..43ea6c691 100644
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/toeq_simple_vector.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/teqo_simple_vector.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "static_2/syntax/term_vector.ma".
-include "static_2/syntax/toeq_simple.ma".
+include "static_2/syntax/teqo_simple.ma".
 
 (* SORT-IRRELEVANT OUTER EQUIVALENCE FOR TERMS ******************************)
 
@@ -21,9 +21,9 @@ include "static_2/syntax/toeq_simple.ma".
 
 (* 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):
+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 (toeq_inv_pair2 … H) -H
+#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
diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/toeq_tdeq.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/teqo_tdeq.ma
similarity index 89%
rename from matita/matita/contribs/lambdadelta/static_2/syntax/toeq_tdeq.ma
rename to matita/matita/contribs/lambdadelta/static_2/syntax/teqo_tdeq.ma
index 73be8f600..a0a93b9bd 100644
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/toeq_tdeq.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/teqo_tdeq.ma
@@ -13,12 +13,12 @@
 (**************************************************************************)
 
 include "static_2/syntax/tdeq.ma".
-include "static_2/syntax/toeq.ma".
+include "static_2/syntax/teqo.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/
+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/toeq_toeq.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/teqo_teqo.ma
similarity index 74%
rename from matita/matita/contribs/lambdadelta/static_2/syntax/toeq_toeq.ma
rename to matita/matita/contribs/lambdadelta/static_2/syntax/teqo_teqo.ma
index 9b7af0a51..c3d6d0c3a 100644
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/toeq_toeq.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/teqo_teqo.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "static_2/syntax/toeq.ma".
+include "static_2/syntax/teqo.ma".
 
 (* SORT-IRRELEVANT OUTER EQUIVALENCE FOR TERMS ******************************)
 
@@ -20,21 +20,21 @@ include "static_2/syntax/toeq.ma".
 
 (* Basic_1: was: iso_trans *)
 (* Basic_2A1: was: tsts_trans *)
-theorem toeq_trans: Transitive … toeq.
+theorem teqo_trans: Transitive … teqo.
 #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 //
+  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 (toeq_inv_pair1 … H) -H #V2 #T2 #H destruct //
+  elim (teqo_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-.
+theorem teqo_canc_sn: left_cancellable … teqo.
+/3 width=3 by teqo_trans, teqo_sym/ qed-.
 
 (* Basic_2A1: was: tsts_canc_dx *)
-theorem toeq_canc_dx: right_cancellable … toeq.
-/3 width=3 by toeq_trans, toeq_sym/ qed-.
+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/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" * } {
-- 
2.39.2