From c0d38a82464481e3c8fd68e4b00d7b9b448df462 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
Date: Tue, 3 Sep 2019 19:36:47 +0200
Subject: [PATCH] milestone in basic_2

We parametrize applicability condition with a generic subset of numbers.
---
 .../lambdadelta/basic_2/dynamic/cnv_cpme.ma   |  4 +-
 .../lambdadelta/basic_2/dynamic/cnv_cpmuwe.ma |  5 +-
 .../basic_2/dynamic/cnv_cpmuwe_cpme.ma        | 35 +++++++++
 .../lambdadelta/basic_2/dynamic/cnv_eval.ma   |  3 +-
 .../basic_2/rt_computation/cnuw.ma            | 57 +-------------
 .../basic_2/rt_computation/cnuw_cnuw.ma       | 57 +++++++++++++-
 .../basic_2/rt_computation/cnuw_tdeq.ma       | 74 -------------------
 .../basic_2/rt_computation/cpme.ma            | 13 ++++
 .../basic_2/rt_computation/cpms.ma            | 30 ++++++++
 .../basic_2/rt_computation/cpmuwe_csx.ma      | 18 +++--
 .../basic_2/rt_computation/cpre_cpms.ma       |  2 +-
 .../basic_2/rt_computation/cpre_cpre.ma       |  2 +-
 .../basic_2/rt_computation/cpre_csx.ma        |  4 +-
 .../basic_2/rt_computation/cprs_tweq.ma       |  2 +-
 .../lambdadelta/basic_2/rt_transition/cpm.ma  | 25 +++++++
 .../lambdadelta/basic_2/web/basic_2.ldw.xml   |  7 +-
 .../lambdadelta/basic_2/web/basic_2_src.tbl   |  7 +-
 .../static_2/relocation/lifts_tweq.ma         |  2 +-
 .../static_2/syntax/term_weight.ma            |  4 +
 .../lambdadelta/static_2/syntax/tweq.ma       |  6 +-
 .../lambdadelta/static_2/syntax/tweq_tdeq.ma  | 32 ++++++++
 .../lambdadelta/static_2/web/static_2_src.tbl |  2 +-
 22 files changed, 229 insertions(+), 162 deletions(-)
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpmuwe_cpme.ma
 delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw_tdeq.ma
 create mode 100644 matita/matita/contribs/lambdadelta/static_2/syntax/tweq_tdeq.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpme.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpme.ma
index a9091b059..9e0da7d55 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpme.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpme.ma
@@ -18,7 +18,7 @@ include "basic_2/dynamic/cnv_preserve.ma".
 
 (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
 
-(* Properties with evaluation for t-bound rt-transition on terms ************)
+(* Properties with t-bound evaluation on terms ******************************)
 
 lemma cnv_cpme_trans (a) (h) (n) (G) (L):
       ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] →
@@ -33,7 +33,7 @@ lemma cnv_cpme_cpms_conf (a) (h) (n) (G) (L):
 #a #h #n #G #L #T0 #HT0 #T1 #HT01 #T2 * #HT02 #HT2
 elim (cnv_cpms_conf … HT0 … HT01 … HT02) -T0 <minus_n_n #T0 #HT10 #HT20
 lapply (cprs_inv_cnr_sn … HT20 HT2) -HT20 #H destruct
-/2 width=1 by conj/
+/2 width=1 by cpme_intro/
 qed-.
 
 (* Main properties with evaluation for t-bound rt-transition on terms *****)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpmuwe.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpmuwe.ma
index 011388942..9ba812a95 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpmuwe.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpmuwe.ma
@@ -18,7 +18,7 @@ include "basic_2/dynamic/cnv_preserve.ma".
 
 (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
 
-(* Properties with head evaluation for t-bound rt-transition on terms *******)
+(* Properties with t-unbound whd evaluation on terms ************************)
 
 lemma cnv_cpmuwe_trans (a) (h) (G) (L):
       ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] →
@@ -29,9 +29,6 @@ lemma cnv_R_cpmuwe_total (a) (h) (G) (L):
       ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] → ∃n. R_cpmuwe h G L T1 n.
 /4 width=2 by cnv_fwd_fsb, fsb_inv_csx, R_cpmuwe_total_csx/ qed-.
 
-axiom cnv_R_cpmuwe_dec (a) (h) (G) (L):
-      ∀T. ⦃G,L⦄ ⊢ T ![a,h] → ∀n. Decidable (R_cpmuwe h G L T n).
-
 (* Main inversions with head evaluation for t-bound rt-transition on terms **)
 
 theorem cnv_cpmuwe_mono (a) (h) (G) (L):
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpmuwe_cpme.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpmuwe_cpme.ma
new file mode 100644
index 000000000..992588e0b
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpmuwe_cpme.ma
@@ -0,0 +1,35 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/rt_computation/cpme_aaa.ma".
+include "basic_2/rt_computation/cnuw_cnuw.ma".
+include "basic_2/rt_computation/cpmuwe.ma".
+include "basic_2/dynamic/cnv_cpme.ma".
+
+(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
+
+(* Advanced Properties with t-unbound whd evaluation on terms ***************)
+
+lemma cnv_R_cpmuwe_dec (a) (h) (G) (L):
+      ∀T. ⦃G,L⦄ ⊢ T ![a,h] → ∀n. Decidable (R_cpmuwe h G L T n).
+#a #h #G #L #T1 #HT1 #n
+elim (cnv_fwd_aaa … HT1) #A #HA
+elim (cpme_total_aaa h n … HA) -HA #T2 #HT12
+elim (cnuw_dec h G L T2) #HnT1
+[ /5 width=3 by cpme_fwd_cpms, cpmuwe_intro, ex_intro, or_introl/
+| @or_intror * #T3 * #HT13 #HT3
+  lapply (cnv_cpme_cpms_conf … HT1 … HT13 … HT12) -a -T1 #HT32
+  /4 width=9 by cpme_fwd_cpms, cnuw_cpms_trans/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_eval.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_eval.ma
index 9d86f579d..363774648 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_eval.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_eval.ma
@@ -14,7 +14,8 @@
 
 include "basic_2/rt_computation/cpmuwe_cpmuwe.ma".
 include "basic_2/rt_equivalence/cpes_cpes.ma".
-include "basic_2/dynamic/cnv_cpmuwe.ma".
+include "basic_2/dynamic/cnv_cpmuwe.ma". (**) (* should be included by the next *)
+include "basic_2/dynamic/cnv_cpmuwe_cpme.ma".
 include "basic_2/dynamic/cnv_cpes.ma".
 include "basic_2/dynamic/cnv_preserve_cpes.ma".
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw.ma
index 72a8e9ac3..45b655229 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw.ma
@@ -25,61 +25,6 @@ interpretation
   "normality for t-unbound weak head context-sensitive parallel rt-transition (term)"
   'PRedITNormal h G L T = (cnuw h G L T).
 
-lemma cpm_inv_lref1_ctop (n) (h) (G):
-      ∀X2,i. ⦃G,⋆⦄ ⊢ #i ➡[n,h] X2 → ∧∧ X2 = #i & n = 0.
-#n #h #G #X2 * [| #i ] #H
-[ elim (cpm_inv_zero1 … H) -H *
-  [ #H1 #H2 destruct /2 width=1 by conj/
-  | #Y #X1 #X2 #_ #_ #H destruct
-  | #m #Y #X1 #X2 #_ #_ #H destruct
-  ]
-| elim (cpm_inv_lref1 … H) -H *
-  [ #H1 #H2 destruct /2 width=1 by conj/
-  | #Z #Y #X0 #_ #_ #H destruct
-  ]
-]
-qed.
-
-lemma cpm_inv_zero1_unit (n) (h) (I) (K) (G):
-      ∀X2. ⦃G,K.ⓤ{I}⦄ ⊢ #0 ➡[n,h] X2 → ∧∧ X2 = #0 & n = 0.
-#n #h #I #G #K #X2 #H
-elim (cpm_inv_zero1 … H) -H *
-[ #H1 #H2 destruct /2 width=1 by conj/
-| #Y #X1 #X2 #_ #_ #H destruct
-| #m #Y #X1 #X2 #_ #_ #H destruct
-]
-qed.
-
-lemma cpms_inv_lref1_ctop (n) (h) (G):
-      ∀X2,i. ⦃G,⋆⦄ ⊢ #i ➡*[n,h] X2 → ∧∧ X2 = #i & n = 0.
-#n #h #G #X2 #i #H @(cpms_ind_dx … H) -X2
-[ /2 width=1 by conj/
-| #n1 #n2 #X #X2 #_ * #HX #Hn1 #HX2 destruct
-  elim (cpm_inv_lref1_ctop … HX2) -HX2 #H1 #H2 destruct
-  /2 width=1 by conj/
-]
-qed-.
-
-lemma cpms_inv_zero1_unit (n) (h) (I) (K) (G):
-      ∀X2. ⦃G,K.ⓤ{I}⦄ ⊢ #0 ➡*[n,h] X2 → ∧∧ X2 = #0 & n = 0.
-#n #h #I #G #K #X2 #H @(cpms_ind_dx … H) -X2
-[ /2 width=1 by conj/
-| #n1 #n2 #X #X2 #_ * #HX #Hn1 #HX2 destruct
-  elim (cpm_inv_zero1_unit … HX2) -HX2 #H1 #H2 destruct
-  /2 width=1 by conj/
-]
-qed-.
-
-lemma cpms_inv_gref1 (n) (h) (G) (L):
-      ∀X2,l. ⦃G,L⦄ ⊢ §l ➡*[n,h] X2 → ∧∧ X2 = §l & n = 0.
-#n #h #G #L #X2 #l #H @(cpms_ind_dx … H) -X2
-[ /2 width=1 by conj/
-| #n1 #n2 #X #X2 #_ * #HX #Hn1 #HX2 destruct
-  elim (cpm_inv_gref1 … HX2) -HX2 #H1 #H2 destruct
-  /2 width=1 by conj/
-]
-qed-.
-
 (* Basic properties *********************************************************)
 
 lemma cnuw_sort (h) (G) (L): ∀s. ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] ⋆s.
@@ -118,7 +63,7 @@ lemma cnuw_inv_cast (h) (G) (L):
       ∀V,T. ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] ⓝV.T → ⊥.
 #h #G #L #V #T #H
 lapply (H 0 T ?) [ /3 width=1 by cpm_cpms, cpm_eps/ ] -H #H
-/2 width=3 by tweq_inv_cast_sn_XY_Y/
+/2 width=3 by tweq_inv_cast_xy_y/
 qed-.
 
 (* Basic forward lemmas *****************************************************)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw_cnuw.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw_cnuw.ma
index 0249a95e0..6cde759d9 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw_cnuw.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw_cnuw.ma
@@ -12,7 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/rt_computation/cnuw.ma".
+include "basic_2/rt_computation/cnuw_simple.ma".
+include "basic_2/rt_computation/cnuw_drops.ma".
 include "basic_2/rt_computation/cprs_tweq.ma".
 include "basic_2/rt_computation/lprs_cpms.ma".
 
@@ -49,3 +50,57 @@ lemma cnuw_cpms_trans (h) (n) (G) (L):
 #h #n1 #G #L #T1 #HT1 #T2 #HT12 #n2 #T3 #HT23
 /4 width=5 by cpms_trans, tweq_canc_sn/
 qed-.
+
+lemma cnuw_dec_ex (h) (G) (L):
+      ∀T1. ∨∨ ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] T1
+            | ∃∃n,T2. ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 & (T1 ≅ T2 → ⊥).
+#h #G #L #T1 elim T1 -T1 *
+[ #s /3 width=5 by cnuw_sort, or_introl/
+| #i elim (drops_F_uni L i)
+  [ /3 width=7 by cnuw_atom_drops, or_introl/
+  | * * [ #I | * #V ] #K #HLK
+    [ /3 width=8 by cnuw_unit_drops, or_introl/
+    | elim (lifts_total V 𝐔❴↑i❵) #W #HVW
+      @or_intror @(ex2_2_intro … W) [1,2: /2 width=7 by cpms_delta_drops/ ] #H
+      lapply (tweq_inv_lref_sn … H) -H #H destruct
+      /2 width=5 by lifts_inv_lref2_uni_lt/
+    | elim (lifts_total V 𝐔❴↑i❵) #W #HVW
+      @or_intror @(ex2_2_intro … W) [1,2: /2 width=7 by cpms_ell_drops/ ] #H
+      lapply (tweq_inv_lref_sn … H) -H #H destruct
+      /2 width=5 by lifts_inv_lref2_uni_lt/
+    ]
+  ]
+| #l /3 width=5 by cnuw_gref, or_introl/
+| #p * [ cases p ] #V1 #T1 #_ #_
+  [ elim (cprs_abbr_pos_twneq h G L V1 T1) #T2 #HT12 #HnT12
+    /4 width=4 by ex2_2_intro, or_intror/
+  | /3 width=5 by cnuw_abbr_neg, or_introl/
+  | /3 width=5 by cnuw_abst, or_introl/
+  ]
+| * #V1 #T1 #_ #IH
+  [ elim (simple_dec_ex T1) [ #HT1 | * #p * #W1 #U1 #H destruct ]
+    [ elim IH -IH
+      [ /3 width=6 by cnuw_appl_simple, or_introl/
+      | * #n #T2 #HT12 #HnT12 -HT1
+        @or_intror @(ex2_2_intro … n (ⓐV1.T2)) [ /2 width=1 by cpms_appl_dx/ ] #H
+        lapply (tweq_inv_appl_bi … H) -H /2 width=1 by/
+      ]
+    | elim (lifts_total V1 𝐔❴1❵) #X1 #HVX1
+      @or_intror @(ex2_2_intro … (ⓓ{p}W1.ⓐX1.U1)) [1,2: /2 width=3 by cpms_theta/ ] #H
+      elim (tweq_inv_appl_sn … H) -H #X1 #X2 #_ #H destruct
+    | @or_intror @(ex2_2_intro … (ⓓ{p}ⓝW1.V1.U1)) [1,2: /2 width=2 by cpms_beta/ ] #H
+      elim (tweq_inv_appl_sn … H) -H #X1 #X2 #_ #H destruct
+    ]
+  | @or_intror @(ex2_2_intro … T1) [1,2: /2 width=2 by cpms_eps/ ] #H
+    /2 width=4 by tweq_inv_cast_xy_y/
+  ]
+]
+qed-.
+
+lemma cnuw_dec (h) (G) (L): ∀T. Decidable (⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] T).
+#h #G #L #T1
+elim (cnuw_dec_ex h G L T1)
+[ /2 width=1 by or_introl/
+| * #n #T2 #HT12 #nT12 /4 width=2 by or_intror/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw_tdeq.ma
deleted file mode 100644
index 40ac5ddbf..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw_tdeq.ma
+++ /dev/null
@@ -1,74 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/rt_transition/cpr_tdeq.ma".
-include "basic_2/rt_computation/cnuw_simple.ma".
-include "basic_2/rt_computation/cnuw_drops.ma".
-include "basic_2/rt_computation/cnuw_cnuw.ma".
-
-(* NORMAL TERMS FOR T-UNUNBOUND WHD RT-TRANSITION ***************************)
-
-(* Properties with context-free sort-irrelevant equivalence for terms *******)
-
-lemma cnuw_dec_tdeq (h) (G) (L):
-      ∀T1. ∨∨ ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] T1
-            | ∃∃n,T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 & (T1 ≛ T2 → ⊥).
-#h #G #L #T1 elim T1 -T1 *
-[ #s /3 width=5 by cnuw_sort, or_introl/
-| #i elim (drops_F_uni L i)
-  [ /3 width=7 by cnuw_atom_drops, or_introl/
-  | * * [ #I | * #V ] #K #HLK
-    [ /3 width=8 by cnuw_unit_drops, or_introl/
-    | elim (lifts_total V 𝐔❴↑i❵) #W #HVW
-      @or_intror @(ex2_2_intro … W) [1,2: /2 width=7 by cpm_delta_drops/ ] #H
-      lapply (tdeq_inv_lref1 … H) -H #H destruct
-      /2 width=5 by lifts_inv_lref2_uni_lt/
-    | elim (lifts_total V 𝐔❴↑i❵) #W #HVW
-      @or_intror @(ex2_2_intro … W) [1,2: /2 width=7 by cpm_ell_drops/ ] #H
-      lapply (tdeq_inv_lref1 … H) -H #H destruct
-      /2 width=5 by lifts_inv_lref2_uni_lt/
-    ]
-  ]
-| #l /3 width=5 by cnuw_gref, or_introl/
-| #p * [ cases p ] #V1 #T1 #_ #_
-  [ elim (cpr_subst h G (L.ⓓV1) T1 0 L V1) [| /2 width=1 by drops_refl/ ] #T2 #X2 #HT12 #HXT2
-    elim (tdeq_dec T1 T2) [ -HT12 #HT12 | #HnT12 ]
-    [ elim (tdeq_inv_lifts_dx … HT12 … HXT2) -T2 #X1 #HXT1 #_ -X2
-      @or_intror @(ex2_2_intro … X1) [1,2: /2 width=4 by cpm_zeta/ ] #H
-      /2 width=7 by tdeq_lifts_inv_pair_sn/
-    | @or_intror @(ex2_2_intro … (+ⓓV1.T2)) [1,2: /2 width=2 by cpm_bind/ ] #H
-      elim (tdeq_inv_pair … H) -H /2 width=1 by/
-    ]
-  | /3 width=5 by cnuw_abbr_neg, or_introl/
-  | /3 width=5 by cnuw_abst, or_introl/
-  ]
-| * #V1 #T1 #_ #IH
-  [ elim (simple_dec_ex T1) [ #HT1 | * #p * #W1 #U1 #H destruct ]
-    [ elim IH -IH
-      [ /3 width=6 by cnuw_appl_simple, or_introl/
-      | * #n #T2 #HT12 #HnT12
-        @or_intror @(ex2_2_intro … n (ⓐV1.T2)) [ /2 width=1 by cpm_appl/ ] #H
-        elim (tdeq_inv_pair … H) -H #_ #_ /2 width=1 by/
-      ]
-    | elim (lifts_total V1 𝐔❴1❵) #X1 #HVX1
-      @or_intror @(ex2_2_intro … (ⓓ{p}W1.ⓐX1.U1)) [1,2: /2 width=3 by cpm_theta/ ] #H
-      elim (tdeq_inv_pair … H) -H #H destruct
-    | @or_intror @(ex2_2_intro … (ⓓ{p}ⓝW1.V1.U1)) [1,2: /2 width=2 by cpm_beta/ ] #H
-      elim (tdeq_inv_pair … H) -H #H destruct
-    ]
-  | @or_intror @(ex2_2_intro … T1) [1,2: /2 width=2 by cpm_eps/ ] #H
-    /2 width=4 by tdeq_inv_pair_xy_y/
-  ]
-]
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpme.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpme.ma
index 931c8168b..dcee3eb9f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpme.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpme.ma
@@ -24,3 +24,16 @@ definition cpme (h) (n) (G) (L): relation2 term term ≝
 
 interpretation "evaluation for t-bound context-sensitive parallel rt-transition (term)"
    'PRedEval h n G L T1 T2 = (cpme h n G L T1 T2).
+
+(* Basic properties *********************************************************)
+
+lemma cpme_intro (h) (n) (G) (L):
+      ∀T1,T2. ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 → ⦃G,L⦄ ⊢ ➡[h] 𝐍⦃T2⦄ → ⦃G,L⦄⊢T1➡*[h,n]𝐍⦃T2⦄.
+/2 width=1 by conj/ qed.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma cpme_fwd_cpms (h) (n) (G) (L):
+      ∀T1,T2. ⦃G,L⦄⊢T1➡*[h,n]𝐍⦃T2⦄ → ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2.
+#h #n #G #L #T1 #T2 * //
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms.ma
index d1817d6ff..2f7d1f449 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms.ma
@@ -156,6 +156,36 @@ lemma cpms_inv_sort1 (n) (h) (G) (L): ∀X2,s. ⦃G,L⦄ ⊢ ⋆s ➡*[n,h] X2 
 elim (cpm_inv_sort1 … HX2) -HX2 #H #_ destruct //
 qed-.
 
+lemma cpms_inv_lref1_ctop (n) (h) (G):
+      ∀X2,i. ⦃G,⋆⦄ ⊢ #i ➡*[n,h] X2 → ∧∧ X2 = #i & n = 0.
+#n #h #G #X2 #i #H @(cpms_ind_dx … H) -X2
+[ /2 width=1 by conj/
+| #n1 #n2 #X #X2 #_ * #HX #Hn1 #HX2 destruct
+  elim (cpm_inv_lref1_ctop … HX2) -HX2 #H1 #H2 destruct
+  /2 width=1 by conj/
+]
+qed-.
+
+lemma cpms_inv_zero1_unit (n) (h) (I) (K) (G):
+      ∀X2. ⦃G,K.ⓤ{I}⦄ ⊢ #0 ➡*[n,h] X2 → ∧∧ X2 = #0 & n = 0.
+#n #h #I #G #K #X2 #H @(cpms_ind_dx … H) -X2
+[ /2 width=1 by conj/
+| #n1 #n2 #X #X2 #_ * #HX #Hn1 #HX2 destruct
+  elim (cpm_inv_zero1_unit … HX2) -HX2 #H1 #H2 destruct
+  /2 width=1 by conj/
+]
+qed-.
+
+lemma cpms_inv_gref1 (n) (h) (G) (L):
+      ∀X2,l. ⦃G,L⦄ ⊢ §l ➡*[n,h] X2 → ∧∧ X2 = §l & n = 0.
+#n #h #G #L #X2 #l #H @(cpms_ind_dx … H) -X2
+[ /2 width=1 by conj/
+| #n1 #n2 #X #X2 #_ * #HX #Hn1 #HX2 destruct
+  elim (cpm_inv_gref1 … HX2) -HX2 #H1 #H2 destruct
+  /2 width=1 by conj/
+]
+qed-.
+
 lemma cpms_inv_cast1 (h) (n) (G) (L):
       ∀W1,T1,X2. ⦃G,L⦄ ⊢ ⓝW1.T1 ➡*[n,h] X2 →
       ∨∨ ∃∃W2,T2. ⦃G,L⦄ ⊢ W1 ➡*[n,h] W2 & ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 & X2 = ⓝW2.T2
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmuwe_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmuwe_csx.ma
index 911dddd5b..1939101a3 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmuwe_csx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmuwe_csx.ma
@@ -12,9 +12,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/rt_transition/cpm_cpx.ma".
-include "basic_2/rt_computation/csx.ma".
-include "basic_2/rt_computation/cnuw_tdeq.ma".
+include "static_2/syntax/tweq_tdeq.ma".
+include "basic_2/rt_computation/csx_cpxs.ma".
+include "basic_2/rt_computation/cpms_cpxs.ma".
+include "basic_2/rt_computation/cnuw_cnuw.ma".
 include "basic_2/rt_computation/cpmuwe.ma".
 
 (* T-UNBOUND WHD EVALUATION FOR T-BOUND RT-TRANSITION ON TERMS **************)
@@ -24,12 +25,15 @@ include "basic_2/rt_computation/cpmuwe.ma".
 lemma cpmuwe_total_csx (h) (G) (L):
       ∀T1. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ∃∃T2,n. ⦃G,L⦄ ⊢ T1 ➡*𝐍𝐖*[h,n] T2.
 #h #G #L #T1 #H
-@(csx_ind … H) -T1 #T1 #_ #IHT1
-elim (cnuw_dec_tdeq h G L T1)
+@(csx_ind_cpxs … H) -T1 #T1 #_ #IHT1
+elim (cnuw_dec_ex h G L T1)
 [ -IHT1 #HT1 /3 width=4 by cpmuwe_intro, ex1_2_intro/
 | * #n1 #T0 #HT10 #HnT10
-  elim (IHT1 … HnT10) -IHT1 -HnT10 [| /2 width=2 by cpm_fwd_cpx/ ]
-  #T2 #n2 * #HT02 #HT2 /4 width=5 by cpms_step_sn, cpmuwe_intro, ex1_2_intro/
+  elim (IHT1 … T0) -IHT1
+  [ #T2 #n2 * #HT02 #HT2 /4 width=5 by cpms_trans, cpmuwe_intro, ex1_2_intro/
+  | /3 width=1 by tdeq_tweq/
+  | /2 width=2 by cpms_fwd_cpxs/
+  ]
 ]
 qed-.
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpre_cpms.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpre_cpms.ma
index a6fc27e18..2dd997c45 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpre_cpms.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpre_cpms.ma
@@ -23,5 +23,5 @@ lemma cpms_cpre_trans (h) (n) (G) (L):
       ∀T1,T0. ⦃G,L⦄ ⊢T1 ➡*[n,h] T0 →
       ∀T2. ⦃G,L⦄ ⊢ T0 ➡*[h] 𝐍⦃T2⦄ → ⦃G,L⦄ ⊢ T1 ➡*[h,n] 𝐍⦃T2⦄.
 #h #n #G #L #T1 #T0 #HT10 #T2 * #HT02 #HT2
-/3 width=3 by cpms_cprs_trans, conj/
+/3 width=3 by cpms_cprs_trans, cpme_intro/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpre_cpre.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpre_cpre.ma
index 5ddc528f4..a855b327f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpre_cpre.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpre_cpre.ma
@@ -25,7 +25,7 @@ lemma cpre_cprs_conf (h) (G) (L) (T):
 #h #G #L #T0 #T1 #HT01 #T2 * #HT02 #HT2
 elim (cprs_conf … HT01 … HT02) -T0 #T0 #HT10 #HT20
 lapply (cprs_inv_cnr_sn … HT20 HT2) -HT20 #H destruct
-/2 width=1 by conj/
+/2 width=1 by cpme_intro/
 qed-.
 
 (* Main properties *********************************************************)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpre_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpre_csx.ma
index 3d1a34c8b..555ff0cb7 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpre_csx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpre_csx.ma
@@ -26,8 +26,8 @@ lemma cpre_total_csx (h) (G) (L):
       ∀T1. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ∃T2. ⦃G,L⦄ ⊢ T1 ➡*[h] 𝐍⦃T2⦄.
 #h #G #L #T1 #H
 @(csx_ind … H) -T1 #T1 #_ #IHT1
-elim (cnr_dec_tdeq h G L T1) [ /3 width=3 by ex_intro, conj/ ] *
+elim (cnr_dec_tdeq h G L T1) [ /3 width=3 by ex_intro, cpme_intro/ ] *
 #T0 #HT10 #HnT10
 elim (IHT1 … HnT10) -IHT1 -HnT10 [| /2 width=2 by cpm_fwd_cpx/ ]
-#T2 * /4 width=3 by cprs_step_sn, ex_intro, conj/
+#T2 * /4 width=3 by cprs_step_sn, ex_intro, cpme_intro/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_tweq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_tweq.ma
index a7c2b4074..7c8102af2 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_tweq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_tweq.ma
@@ -28,7 +28,7 @@ elim (cpr_subst h G (L.ⓓV) U1 … 0) [|*: /2 width=4 by drops_refl/ ] #U2 #T2
 elim (tweq_dec U1 U2) [ #HpU12 | -HTU2 #HnU12 ]
 [ @(ex2_intro … T2) (**) (* full auto not tried *)
   [ /3 width=6 by cpms_zeta, cpms_step_sn, cpm_bind/
-  | /4 width=6 by tweq_inv_abbr_pos_sn_X_lifts_Y_Y, tweq_canc_sn, tweq_abbr_pos/
+  | /4 width=6 by tweq_inv_abbr_pos_x_lifts_y_y, tweq_canc_sn, tweq_abbr_pos/
   ]
 | /4 width=3 by cpm_cpms, cpm_bind, tweq_inv_abbr_pos_bi, ex2_intro/
 ]
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma
index db5bdfe78..c069b4ca0 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma
@@ -175,6 +175,16 @@ lemma cpm_inv_zero1: ∀n,h,G,L,T2. ⦃G,L⦄ ⊢ #0 ➡[n,h] T2 →
 ]
 qed-.
 
+lemma cpm_inv_zero1_unit (n) (h) (I) (K) (G):
+      ∀X2. ⦃G,K.ⓤ{I}⦄ ⊢ #0 ➡[n,h] X2 → ∧∧ X2 = #0 & n = 0.
+#n #h #I #G #K #X2 #H
+elim (cpm_inv_zero1 … H) -H *
+[ #H1 #H2 destruct /2 width=1 by conj/
+| #Y #X1 #X2 #_ #_ #H destruct
+| #m #Y #X1 #X2 #_ #_ #H destruct
+]
+qed.
+
 lemma cpm_inv_lref1: ∀n,h,G,L,T2,i. ⦃G,L⦄ ⊢ #↑i ➡[n,h] T2 →
                      ∨∨ T2 = #(↑i) ∧ n = 0
                       | ∃∃I,K,T. ⦃G,K⦄ ⊢ #i ➡[n,h] T & ⬆*[1] T ≘ T2 & L = K.ⓘ{I}.
@@ -185,6 +195,21 @@ lemma cpm_inv_lref1: ∀n,h,G,L,T2,i. ⦃G,L⦄ ⊢ #↑i ➡[n,h] T2 →
 ]
 qed-.
 
+lemma cpm_inv_lref1_ctop (n) (h) (G):
+      ∀X2,i. ⦃G,⋆⦄ ⊢ #i ➡[n,h] X2 → ∧∧ X2 = #i & n = 0.
+#n #h #G #X2 * [| #i ] #H
+[ elim (cpm_inv_zero1 … H) -H *
+  [ #H1 #H2 destruct /2 width=1 by conj/
+  | #Y #X1 #X2 #_ #_ #H destruct
+  | #m #Y #X1 #X2 #_ #_ #H destruct
+  ]
+| elim (cpm_inv_lref1 … H) -H *
+  [ #H1 #H2 destruct /2 width=1 by conj/
+  | #Z #Y #X0 #_ #_ #H destruct
+  ]
+]
+qed.
+
 lemma cpm_inv_gref1: ∀n,h,G,L,T2,l. ⦃G,L⦄ ⊢ §l ➡[n,h] T2 → T2 = §l ∧ n = 0.
 #n #h #G #L #T2 #l * #c #Hc #H elim (cpg_inv_gref1 … H) -H
 #H1 #H2 destruct /3 width=1 by isrt_inv_00, conj/ 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml
index be3c16d73..1be3304c9 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml
@@ -27,8 +27,13 @@
    <table name="basic_2_sum"/>
 
    <subsection name="B">Stage "B"</subsection>
+   <news class="beta" date="2019 September 3.">
+         Applicability condition is now parametrized
+         with a generic subset of numbers.
+   </news>
    <news class="beta" date="2019 June 2.">
-         Parametrized applicability condition
+         Applicability condition parametrized
+         with an initial interval of numbers
          allows λδ-2B to generalize both λδ-2A and λδ-1B.
    </news>
    <news class="beta" date="2019 April 16.">
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 daa511a89..fdfa71e69 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
@@ -25,7 +25,7 @@ table {
         ]
         [ { "context-sensitive native validity" * } {
              [ [ "restricted refinement for lenvs" ] "lsubv ( ? ⊢ ? ⫃![?,?] ? )" "lsubv_drops" + "lsubv_lsubr" + "lsubv_lsuba" + "lsubv_cpms" + "lsubv_cpcs" + "lsubv_cnv" + "lsubv_lsubv" * ]
-             [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" + "( ⦃?,?⦄ ⊢ ? ![?] )" + "( ⦃?,?⦄ ⊢ ? !*[?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpm_tdeq" + "cnv_cpm_tdeq_trans" + "cnv_cpm_tdeq_conf" + "cnv_cpms_tdeq" + "cnv_cpms_conf" + "cnv_cpms_tdeq_conf" + "cnv_cpme" + "cnv_cpmuwe" + "cnv_eval" + "cnv_cpce" + "cnv_cpes" + "cnv_cpcs" + "cnv_preserve_sub" + "cnv_preserve" + "cnv_preserve_cpes" + "cnv_preserve_cpcs" * ]
+             [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" + "( ⦃?,?⦄ ⊢ ? ![?] )" + "( ⦃?,?⦄ ⊢ ? !*[?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpm_tdeq" + "cnv_cpm_tdeq_trans" + "cnv_cpm_tdeq_conf" + "cnv_cpms_tdeq" + "cnv_cpms_conf" + "cnv_cpms_tdeq_conf" + "cnv_cpme" + "cnv_cpmuwe" + "cnv_cpmuwe_cpme" + "cnv_eval" + "cnv_cpce" + "cnv_cpes" + "cnv_cpcs" + "cnv_preserve_sub" + "cnv_preserve" + "cnv_preserve_cpes" + "cnv_preserve_cpcs" * ]
           }
         ]
      }
@@ -67,9 +67,8 @@ table {
         ]
         [ { "t-bound context-sensitive parallel rt-computation" * } {
              [ [ "t-unbound whd evaluation for terms" ] "cpmuwe ( ⦃?,?⦄ ⊢ ? ⬌*𝐍𝐖*[?,?] ? )" "cpmuwe_csx" + "cpmuwe_cpmuwe" * ]
-             [ [ "t-unbound whd normal form for terms" ] "cnuw ( ⦃?,?⦄ ⊢ ⬌𝐍𝐖*[?] ? )" "cnuw_tdeq" + "cnuw_drops" + "cnuw_simple" + "cnuw_cnuw" * ]
-
-             [ [ "evaluation for terms" ] "cpme ( ⦃?,?⦄ ⊢ ? ➡*[?,?] 𝐍⦃?⦄ )" "cpme_aaa" * ]
+             [ [ "t-unbound whd normal form for terms" ] "cnuw ( ⦃?,?⦄ ⊢ ⬌𝐍𝐖*[?] ? )" "cnuw_drops" + "cnuw_simple" + "cnuw_cnuw" * ]
+             [ [ "t-bpund evaluation for terms" ] "cpme ( ⦃?,?⦄ ⊢ ? ➡*[?,?] 𝐍⦃?⦄ )" "cpme_aaa" * ]
              [ [ "for terms" ] "cpms" + "( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpms_drops" + "cpms_lsubr" + "cpms_rdeq" + "cpms_aaa" + "cpms_lpr" + "cpms_cpxs" + "cpms_fpbs" + "cpms_fpbg" + "cpms_cpms" * ]
           }
         ]
diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_tweq.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_tweq.ma
index 3802cb1d4..addd91c72 100644
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_tweq.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_tweq.ma
@@ -96,7 +96,7 @@ lemma tweq_inv_lifts_bi: deliftable2_bi tweq.
 ]
 qed-.
 
-lemma tweq_inv_abbr_pos_sn_X_lifts_Y_Y (T) (f:rtmap):
+lemma tweq_inv_abbr_pos_x_lifts_y_y (T) (f:rtmap):
       ∀V,U. +ⓓV.U ≅ T → ⬆*[f]T ≘ U → ⊥.
 @(f_ind … tw) #n #IH #T #Hn #f #V #U #H1 #H2 destruct
 elim (tweq_inv_abbr_pos_sn … H1) -H1 #X1 #X2 #HX2 #H destruct -V
diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/term_weight.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/term_weight.ma
index c8d4c974d..6948a54a8 100644
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/term_weight.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/term_weight.ma
@@ -31,6 +31,10 @@ lemma tw_pos: ∀T. 1 ≤ ♯{T}.
 #T elim T -T //
 qed.
 
+lemma tw_le_pair_dx (I): ∀V,T. ♯{T} < ♯{②{I}V.T}.
+#I #V #T /2 width=1 by le_S_S/
+qed.
+
 (* Basic_1: removed theorems 11:
             wadd_le wadd_lt wadd_O weight_le weight_eq weight_add_O
             weight_add_S tlt_trans tlt_head_sx tlt_head_dx tlt_wf_ind
diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/tweq.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/tweq.ma
index fd31eb05e..91234b9ce 100644
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/tweq.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/tweq.ma
@@ -15,10 +15,6 @@
 include "static_2/notation/relations/approxeq_2.ma".
 include "static_2/syntax/term_weight.ma".
 
-lemma tw_le_pair_dx (I): ∀V,T. ♯{T} < ♯{②{I}V.T}.
-#I #V #T /2 width=1 by le_S_S/
-qed.
-
 (* SORT-IRRELEVANT WHD EQUIVALENCE ON TERMS *********************************)
 
 inductive tweq: relation term ≝
@@ -211,7 +207,7 @@ elim (tweq_inv_cast_sn … H) -H #W2 #U2 #HVW #HTU #H destruct
 /2 width=1 by conj/
 qed-.
 
-lemma tweq_inv_cast_sn_XY_Y: ∀T,V. ⓝV.T ≅ T → ⊥.
+lemma tweq_inv_cast_xy_y: ∀T,V. ⓝV.T ≅ T → ⊥.
 @(f_ind … tw) #n #IH #T #Hn #V #H destruct
 elim (tweq_inv_cast_sn … H) -H #X1 #X2 #_ #HX2 #H destruct -V
 /2 width=4 by/
diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/tweq_tdeq.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/tweq_tdeq.ma
new file mode 100644
index 000000000..fb8d7e704
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/tweq_tdeq.ma
@@ -0,0 +1,32 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/tweq.ma".
+
+(* SORT-IRRELEVANT WHD EQUIVALENCE ON TERMS *********************************)
+
+(* Properties with sort-irrelevant equivalence for terms ********************)
+
+lemma tdeq_tweq: ∀T1,T2. T1 ≛ T2 → T1 ≅ T2.
+#T1 #T2 #H elim H -T1 -T2 [||| * [ #p ] * #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT ]
+[ /1 width=1 by tweq_sort/
+| /1 width=1 by tweq_lref/
+| /1 width=1 by tweq_gref/
+| cases p -p /2 width=1 by tweq_abbr_pos, tweq_abbr_neg/  
+| /1 width=1 by tweq_abst/
+| /2 width=1 by tweq_appl/
+| /2 width=1 by tweq_cast/
+]
+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 5fb750e3f..257341c6a 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
@@ -120,7 +120,7 @@ table {
           }
         ]
         [ { "sort-irrelevant whd equivalence" * } {
-             [ [ "for terms" ] "tweq" + "( ? ≅ ? )" "tweq_simple" + "tweq_tueq" * ]
+             [ [ "for terms" ] "tweq" + "( ? ≅ ? )" "tweq_simple" + "tweq_tdeq" + "tweq_tueq" * ]
           }
         ]
         [ { "sort-irrelevant equivalence" * } {
-- 
2.39.2