From 380ceb6b6552fd9ebd48d710ab12931d5d97e465 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 28 Dec 2012 16:32:01 +0000
Subject: [PATCH] xoa: change in naming convenctions for existential quantifies
      to cope with ex2 in lib lib: some additions lambdadelta: partial commit
 in basic_2: just grammar, substitution, unfold, static

---
 matita/components/binaries/xoa/engine.ml      |   4 +-
 matita/matita/contribs/lambdadelta/Makefile   |   1 +
 .../lambdadelta/apps_2/functional/dsubst.ma   |   2 +-
 .../basic_2/computation/cprs_lfpr.ma          |   2 +-
 .../lambdadelta/basic_2/grammar/cl_weight.ma  |  11 +-
 .../lambdadelta/basic_2/grammar/lenv_px.ma    |   2 +-
 .../basic_2/grammar/lenv_weight.ma            |   6 -
 .../basic_2/grammar/term_weight.ma            |   8 +-
 .../basic_2/reducibility/cpr_cpr.ma           |   4 +-
 .../basic_2/reducibility/cpr_lift.ma          |   6 +-
 .../basic_2/reducibility/lfpr_cpr.ma          |   2 +-
 .../basic_2/reducibility/tpr_lift.ma          |   4 +-
 .../basic_2/reducibility/tpr_tpr.ma           |   8 +-
 .../basic_2/reducibility/tpr_tpss.ma          |   2 +-
 .../basic_2/substitution/ldrop_append.ma      |   6 +-
 .../basic_2/substitution/ldrop_sfr.ma         |  12 +-
 .../basic_2/substitution/lift_lift.ma         |   2 +-
 .../lambdadelta/basic_2/substitution/tps.ma   |   7 +-
 .../basic_2/substitution/tps_lift.ma          |   4 +-
 .../basic_2/substitution/tps_tps.ma           |   6 +-
 .../lambdadelta/basic_2/unfold/delift_alt.ma  |   6 +-
 .../lambdadelta/basic_2/unfold/delift_lift.ma |  33 +++--
 .../lambdadelta/basic_2/unfold/frsupp.ma      |  43 ++++---
 .../basic_2/unfold/ltpss_dx_ltpss_dx.ma       | 117 +++++++-----------
 .../basic_2/unfold/ltpss_sn_alt.ma            |   4 +-
 .../basic_2/unfold/ltpss_sn_ltpss_sn.ma       |  37 +++---
 .../lambdadelta/basic_2/unfold/tpss_tpss.ma   |   2 +-
 .../contribs/lambdadelta/ground_2/star.ma     |  29 +++--
 .../lambdadelta/ground_2/xoa.conf.xml         |   3 +-
 .../contribs/lambdadelta/ground_2/xoa.ma      |  20 +--
 .../lambdadelta/ground_2/xoa_notation.ma      |  10 --
 .../lambdadelta/ground_2/xoa_props.ma         |   4 -
 matita/matita/contribs/lambdadelta/root       |   2 +-
 matita/matita/lib/arithmetics/nat.ma          |   4 +
 matita/matita/lib/basics/star.ma              |   2 +-
 35 files changed, 180 insertions(+), 235 deletions(-)

diff --git a/matita/components/binaries/xoa/engine.ml b/matita/components/binaries/xoa/engine.ml
index d650f07b5..fa4bb7ff6 100644
--- a/matita/components/binaries/xoa/engine.ml
+++ b/matita/components/binaries/xoa/engine.ml
@@ -31,7 +31,9 @@ let void_iter f n =
 let mk_exists ooch noch c v =
    let description = "multiple existental quantifier" in
    let prec = "non associative with precedence 20\n" in
-   let name s = P.sprintf "%s%u_%u" s c v in
+   let name s = 
+      if v = 1 then P.sprintf "%s%u" s c else P.sprintf "%s%u_%u" s c v
+   in
    let o_name = name "ex" in
    let i_name = "'Ex" in
 
diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile
index 7e267a2f3..38f1c3076 100644
--- a/matita/matita/contribs/lambdadelta/Makefile
+++ b/matita/matita/contribs/lambdadelta/Makefile
@@ -16,6 +16,7 @@ ORIGS    = basic_2/basic_1.orig
 PACKAGES = ground_2 basic_2 apps_2
 
 all:
+	../../matitac.opt
 
 # xoa ########################################################################
 
diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/dsubst.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/dsubst.ma
index f5847371c..20e372bb6 100644
--- a/matita/matita/contribs/lambdadelta/apps_2/functional/dsubst.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/functional/dsubst.ma
@@ -41,7 +41,7 @@ theorem fdsubst_delift: ∀K,V,T,L,d.
 [ * #i #L #d #HLK normalize in ⊢ (? ? ? ? ? %); /2 width=3/
   elim (lt_or_eq_or_gt i d) #Hid
   [ -HLK >(tri_lt ?????? Hid) /3 width=3/
-  | destruct >tri_eq /4 width=4 by tpss_strap2, tps_subst, le_n, ex2_1_intro/ (**) (* too slow without trace *)   
+  | destruct >tri_eq /4 width=4 by tpss_strap2, tps_subst, le_n, ex2_intro/ (**) (* too slow without trace *)   
   | -HLK >(tri_gt ?????? Hid) /3 width=3/
   ]
 | * /3 width=1/ /4 width=1/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lfpr.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lfpr.ma
index a06643577..1ba4cadd8 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lfpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lfpr.ma
@@ -27,7 +27,7 @@ lemma ltpr_tpss_trans: ∀L1,L2. L1 ➡ L2 → ∀T1,T2,d,e. L2 ⊢ T1 ▶* [d,
 [ /2 width=3/
 | #T #T2 #_ #HT2 * #T0 #HT10 #HT0
   elim (ltpr_tps_trans … HT2 … HL12) -L2 #T3 #HT3 #HT32
-  @(ex2_1_intro … HT10) -T1 (**) (* explicit constructors *)
+  @(ex2_intro … HT10) -T1 (**) (* explicit constructors *)
   @(cprs_strap1 … T3 …) /2 width=1/ -HT32
   @(cprs_strap1 … HT0) -HT0 /3 width=3/
 ]
diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma
index d9569d4d5..fbe41b9d4 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma
@@ -23,13 +23,6 @@ interpretation "weight (closure)" 'Weight L T = (fw L T).
 
 (* Basic properties *********************************************************)
 
-(* Basic_1: was: flt_wf__q_ind *)
-
-(* Basic_1: was: flt_wf_ind *)
-axiom fw_ind: ∀R:relation2 lenv term.
-              (∀L2,T2. (∀L1,T1. #{L1,T1} < #{L2,T2} → R L1 T1) → R L2 T2) →
-              ∀L,T. R L T.
-
 (* Basic_1: was: flt_shift *)
 lemma fw_shift: ∀a,K,I,V,T. #{K. ⓑ{I} V, T} < #{K, ⓑ{a,I} V. T}.
 normalize //
@@ -63,6 +56,8 @@ lemma fw_tpair_sn_dx_shift: ∀I,I1,I2,L,V1,V2,T.
 normalize in ⊢ (?→?→?→?→?→?→?→?%%); /2 width=1/
 qed.
 
-(* Basic_1: removed theorems 6:
+(* Basic_1: removed theorems 7:
             flt_thead_sx flt_thead_dx flt_arith0 flt_arith1 flt_arith2 flt_trans
+            flt_wf_ind
 *)
+(* Basic_1: removed local theorems 1: q_ind *)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_px.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_px.ma
index 41710626a..11bd6822e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_px.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_px.ma
@@ -116,7 +116,7 @@ lemma lpx_trans: ∀R. Transitive ? R → Transitive … (lpx R).
 elim (lpx_inv_pair1 … H) -H #K2 #V2 #HK2 #HV2 #H destruct /3 width=3/
 qed.
 
-lemma lpx_conf: ∀R. Confluent ? R → Confluent … (lpx R).
+lemma lpx_conf: ∀R. confluent ? R → confluent … (lpx R).
 #R #HR #L0 #L1 #H elim H -L1
 [ #X #H >(lpx_inv_atom1 … H) -X /2 width=3/
 | #I #K0 #K1 #V0 #V1 #_ #HV01 #IHK01 #X #H
diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_weight.ma
index 59e2e6172..537d32e56 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_weight.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_weight.ma
@@ -29,11 +29,5 @@ interpretation "weight (local environment)" 'Weight L = (lw L).
 lemma lw_pair: ∀I,L,V. #{L} < #{(L.ⓑ{I}V)}.
 /3 width=1/ qed.
 
-(* Basic eliminators ********************************************************)
-
-axiom lw_ind: ∀R:predicate lenv.
-              (∀L2. (∀L1. #{L1} < #{L2} → R L1) → R L2) →
-              ∀L. R L.
-
 (* Basic_1: removed theorems 2: clt_cong clt_head clt_thead *)
 (* Basic_1: note: clt_thead should be renamed clt_ctail *)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/term_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/term_weight.ma
index d8f39a3a1..3f9fbef87 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/term_weight.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/term_weight.ma
@@ -30,14 +30,8 @@ lemma tw_pos: ∀T. 1 ≤ #{T}.
 #T elim T -T //
 qed.
 
-(* Basic eliminators ********************************************************)
-
-axiom tw_ind: ∀R:predicate term.
-              (∀T2. (∀T1. #{T1} < #{T2} → R T1) → R T2) →
-              ∀T. R T.
-
 (* 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
-            removed local theorems 1: q_ind
 *)
+(* Basic_1: removed local theorems 1: q_ind *)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_cpr.ma
index 8d2eb1f1d..f7738a247 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_cpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_cpr.ma
@@ -22,7 +22,7 @@ include "basic_2/reducibility/cpr.ma".
 lemma cpr_bind_sn: ∀a,I,L,V1,V2,T1,T2. L ⊢ V1 ➡ V2 → T1 ➡ T2 →
                    L ⊢ ⓑ{a,I} V1. T1 ➡ ⓑ{a,I} V2. T2.
 #a #I #L #V1 #V2 #T1 #T2 * #V #HV1 #HV2 #HT12
-@ex2_1_intro [2: @(tpr_delta … HV1 HT12) | skip ] /2 width=3/ (* /3 width=5/ is too slow *)
+@ex2_intro [2: @(tpr_delta … HV1 HT12) | skip ] /2 width=3/ (* /3 width=5/ is too slow *)
 qed.
 
 (* Basic_1: was only: pr2_gen_cbind *)
@@ -32,7 +32,7 @@ lemma cpr_bind_dx: ∀a,I,L,V1,V2,T1,T2. V1 ➡ V2 → L. ⓑ{I} V2 ⊢ T1 ➡ T
 elim (tpss_split_up … HT2 1 ? ?) -HT2 // #T0 <minus_n_O #HT0 normalize <minus_plus_m_m #HT02
 lapply (tpss_lsubs_trans … HT0 (⋆. ⓑ{I} V2) ?) -HT0 /2 width=1/ #HT0
 lapply (tpss_inv_SO2 … HT0) -HT0 #HT0
-@ex2_1_intro [2: @(tpr_delta … HV12 HT1 HT0) | skip | /2 width=1/ ] (**) (* /3 width=5/ is too slow *)
+@ex2_intro [2: @(tpr_delta … HV12 HT1 HT0) | skip | /2 width=1/ ] (**) (* /3 width=5/ is too slow *)
 qed.
 
 (* Basic_1: was only: pr2_head_1 *) 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_lift.ma
index b54510e8c..9ff04b705 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_lift.ma
@@ -25,7 +25,7 @@ lemma cpr_cdelta: ∀L,K,V1,W1,W2,i.
                   ⇧[0, i + 1] W1 ≡ W2 → L ⊢ #i ➡ W2.
 #L #K #V1 #W1 #W2 #i #HLK #HVW1 #HW12
 lapply (ldrop_fwd_ldrop2_length … HLK) #Hi
-@ex2_1_intro [2: // | skip | @tpss_subst /width=6/ ] (**) (* /3 width=6/ is too slow *)
+@ex2_intro [2: // | skip | @tpss_subst /width=6/ ] (**) (* /3 width=6/ is too slow *)
 qed.
 
 lemma cpr_abst: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀V,T1,T2.
@@ -33,7 +33,7 @@ lemma cpr_abst: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀V,T1,T2.
 #L #V1 #V2 * #V0 #HV10 #HV02 #V #T1 #T2 * #T0 #HT10 #HT02 #a
 lapply (tpss_inv_S2 … HT02 L V ?) -HT02 // #HT02
 lapply (tpss_lsubs_trans … HT02 (L.ⓛV2) ?) -HT02 /2 width=1/ #HT02
-@(ex2_1_intro … (ⓛ{a}V0.T0)) /2 width=1/ (* explicit constructors *)
+@(ex2_intro … (ⓛ{a}V0.T0)) /2 width=1/ (* explicit constructors *)
 qed.
 
 lemma cpr_beta: ∀a,L,V1,V2,W,T1,T2.
@@ -41,7 +41,7 @@ lemma cpr_beta: ∀a,L,V1,V2,W,T1,T2.
 #a #L #V1 #V2 #W #T1 #T2 * #V #HV1 #HV2 * #T #HT1 #HT2
 lapply (tpss_inv_S2 … HT2 L W ?) -HT2 // #HT2
 lapply (tpss_lsubs_trans … HT2 (L.ⓓV2) ?) -HT2 /2 width=1/ #HT2
-@(ex2_1_intro … (ⓓ{a}V.T)) /2 width=1/ (**) (* explicit constructor, /3/ is too slow *)
+@(ex2_intro … (ⓓ{a}V.T)) /2 width=1/ (**) (* explicit constructor, /3/ is too slow *)
 qed.
 
 lemma cpr_beta_dx: ∀a,L,V1,V2,W,T1,T2.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_cpr.ma
index 2a40f58bd..4ce12bcc6 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_cpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_cpr.ma
@@ -25,5 +25,5 @@ lemma lfpr_pair_cpr: ∀L1,L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀V1,V2. L2 ⊢ V1 ➡
 #L1 #L2 * #L #HL1 #HL2 #V1 #V2 *
 <(ltpss_sn_fwd_length … HL2) #V #HV1 #HV2 #I
 lapply (ltpss_sn_tpss_trans_eq … HV2 … HL2) -HV2 #V2
-@(ex2_1_intro … (L.ⓑ{I}V)) /2 width=1/ (**) (* explicit constructor *)
+@(ex2_intro … (L.ⓑ{I}V)) /2 width=1/ (**) (* explicit constructor *)
 qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_lift.ma
index b4d76066a..438cefbca 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_lift.ma
@@ -77,7 +77,7 @@ lemma tpr_inv_lift1: t_deliftable_sn tpr.
   elim (IHV12 … HWV1) -V1 #W2 #HWV2 #HW12
   elim (IHT1 … HUT1) -T1 #U #HUT #HU1
   elim (tps_inv_lift1_le … HT2 … HUT ?) -T // [3: /2 width=5/ |2: skip ] #U2 #HU2 #HUT2
-  @ex2_1_intro  [2: /2 width=2/ |1: skip |3: /2 width=3/ ] (**) (* /3 width=5/ is slow *)
+  @ex2_intro  [2: /2 width=2/ |1: skip |3: /2 width=3/ ] (**) (* /3 width=5/ is slow *)
 | #a #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #X #d #e #HX
   elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct
   elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct
@@ -85,7 +85,7 @@ lemma tpr_inv_lift1: t_deliftable_sn tpr.
   elim (IHW12 … HW01) -W1 #W3 #HW32 #HW03
   elim (IHT12 … HT01) -T1 #T3 #HT32 #HT03
   elim (lift_trans_le … HV32 … HV2 ?) -V2 // #V2 #HV32 #HV2
-  @ex2_1_intro [2: /3 width=2/ |1: skip |3: /2 width=3/ ] (**) (* /4 width=5/ is slow *)
+  @ex2_intro [2: /3 width=2/ |1: skip |3: /2 width=3/ ] (**) (* /4 width=5/ is slow *)
 | #V #T1 #T #T2 #_ #HT2 #IHT1 #X #d #e #HX
   elim (lift_inv_bind2 … HX) -HX #V3 #T3 #_ #HT31 #H destruct
   elim (IHT1 … HT31) -T1 #T1 #HT1 #HT31
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpr.ma
index 1522d00c0..a4bda6daf 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpr.ma
@@ -72,7 +72,7 @@ elim (tpr_inv_abbr1 … H) -H *
   elim (IH … HW02 … HWW2) -HW02 -HWW2 /2 width=1/ #W #HW02 #HWW2
   elim (IH … HU02 … HUU02) -HU02 -HUU02 -IH /2 width=1/ #U #HU2 #HUUU2
   elim (tpr_tps_bind … HWW2 HUUU2 … HUU2) -UU2 #UUU #HUUU2 #HUUU1
-  @ex2_1_intro
+  @ex2_intro
   [2: @tpr_theta [6: @HVV |7: @HWW2 |8: @HUUU2 |1,2,3,4: skip | // ]
   |1:skip
   |3: @tpr_delta [3: @tpr_flat |1: skip ] /2 width=5/
@@ -81,7 +81,7 @@ elim (tpr_inv_abbr1 … H) -H *
 | -HV2 -HW02 -HVV2 #U1 #HU01 #HTU1
   elim (IH … HU01 … HU02) -HU01 -HU02 -IH // -U0 #U #HU1 #HU2
   elim (tpr_inv_lift1 … HU1 … HTU1) -U1 #UU #HUU #HT1UU #H destruct
-  @(ex2_1_intro … (ⓐVV.UU)) /2 width=1/ /3 width=5/ (**) (* /4 width=9/ is too slow *)
+  @(ex2_intro … (ⓐVV.UU)) /2 width=1/ /3 width=5/ (**) (* /4 width=9/ is too slow *)
 ]
 qed.
 
@@ -127,7 +127,7 @@ elim (IH … HT01 … HT02) -HT01 -HT02 -IH // #T #HT1 #HT2
 elim (tpr_tps_bind … HV1 HT1 … HTT1) -T1 #U1 #TTU1 #HTU1
 elim (tpr_tps_bind … HV2 HT2 … HTT2) -T2 #U2 #TTU2 #HTU2
 elim (tps_conf_eq … HTU1 … HTU2) -T #U #HU1 #HU2
-@ex2_1_intro [2,3: @tpr_delta |1: skip ] /width=10/ (**) (* /3 width=10/ is too slow *)
+@ex2_intro [2,3: @tpr_delta |1: skip ] /width=10/ (**) (* /3 width=10/ is too slow *)
 qed.
 
 fact tpr_conf_delta_zeta:
@@ -163,7 +163,7 @@ elim (IH … HT01 … HT02) -HT01 -HT02 -IH /2 width=1/ #T #HT1 #HT2
 elim (lift_total V 0 1) #VV #HVV
 lapply (tpr_lift … HV1 … HVV1 … HVV) -V1 #HVV1
 lapply (tpr_lift … HV2 … HVV2 … HVV) -V2 -HVV #HVV2
-@ex2_1_intro [2,3: @tpr_bind |1:skip ] /2 width=5/ (**) (* /4 width=5/ is too slow *)
+@ex2_intro [2,3: @tpr_bind |1:skip ] /2 width=5/ (**) (* /4 width=5/ is too slow *)
 qed.
 
 fact tpr_conf_zeta_zeta:
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpss.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpss.ma
index e1ead4e44..aadc0c80e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpss.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpss.ma
@@ -55,7 +55,7 @@ lemma tpr_tps_ltpr: ∀T1,T2. T1 ➡ T2 →
   elim (IHT12 … HTT1 (L2. ⓓWW2) ?) -T1 /2 width=1/ -HL12 #TT2 #HTT12 #HTT2
   elim (lift_total VV2 0 1) #VV #H2VV
   lapply (tpss_lift_ge … HVV2 (L2. ⓓWW2) … HV2 … H2VV) -V2 /2 width=1/ #HVV
-  @ex2_1_intro [2: @tpr_theta |1: skip |3: @tpss_bind [2: @tpss_flat ] ] /width=11/ (**) (* /4 width=11/ is too slow *)
+  @ex2_intro [2: @tpr_theta |1: skip |3: @tpss_bind [2: @tpss_flat ] ] /width=11/ (**) (* /4 width=11/ is too slow *)
 | #V #T1 #T #T2 #_ #HT2 #IHT1 #L1 #d #e #X #H #L2 #HL12
   elim (tps_inv_bind1 … H) -H #W #U1 #_ #HTU1 #H destruct -V
   elim (IHT1 … HTU1 (L2.ⓓW) ?) -T1 /2 width=1/ -HL12 #U #HU1 #HTU
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_append.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_append.ma
index 359d39c80..38244e6be 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_append.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_append.ma
@@ -54,9 +54,11 @@ lemma ldrop_O1_inv_append1_le: ∀K,L1,L2,e. ⇩[0, e] L1 @@ L2 ≡ K → e ≤
   [ #H1 #_ #K2 #H2
     lapply (ldrop_inv_refl … H1) -H1 #H1
     lapply (ldrop_inv_refl … H2) -H2 #H2 destruct //
-  | #e #_ #H1 #H1e #K2 #H2
+  | #e #_ #H1 #H #K2 #H2
+    lapply (le_plus_to_le_r … H) -H
     lapply (ldrop_inv_ldrop1 … H1 ?) -H1 //
-    lapply (ldrop_inv_ldrop1 … H2 ?) -H2 // /3 width=4/
+    lapply (ldrop_inv_ldrop1 … H2 ?) -H2 //
+    <minus_plus_m_m /2 width=4/
   ]
 ]
 qed-. 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_sfr.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_sfr.ma
index 78a15d70d..4f4060ff1 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_sfr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_sfr.ma
@@ -52,13 +52,15 @@ lemma sfr_ldrop: ∀L,d,e.
 #L elim L -L //
 #L #I #V #IHL #d @(nat_ind_plus … d) -d
 [ #e @(nat_ind_plus … e) -e //
-  #e #_ #HH
-  >(HH I L V 0 ? ? ?) // /5 width=6/
-| /5 width=6/
+  #e #_ #H0
+  >(H0 I L V 0 ? ? ?) //
+  /5 width=6 by sfr_abbr, ldrop_ldrop, lt_minus_to_plus_r/ (**) (* auto now too slow without trace *)
+| #d #_ #e #H0 
+  /5 width=6 by sfr_skip, ldrop_ldrop, le_S_S, lt_minus_to_plus_r/ (**) (* auto now too slow without trace *)
 ]
 qed.
 
-lemma sfr_ldrop_trans_le: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → ∀dd,ee. ≽ [dd, ee] L1 → 
+lemma sfr_ldrop_trans_le: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → ∀dd,ee. ≽ [dd, ee] L1 →
                           dd + ee ≤ d → ≽ [dd, ee] L2.
 #L1 #L2 #d #e #HL12 #dd #ee #HL1 #Hddee
 @sfr_ldrop #I #K2 #V2 #i #Hddi #Hiddee #HLK2
@@ -80,7 +82,7 @@ lapply (ldrop_trans_ge … HL12 … HLK2 ?) -L2 // -Hdi  #HL1K2
 @(sfr_inv_ldrop … HL1K2 … HL1) -L1 >commutative_plus // -Hddie /2 width=1/
 qed.
 
-lemma sfr_ldrop_trans_ge: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → ∀dd,ee. ≽ [dd, ee] L1 → 
+lemma sfr_ldrop_trans_ge: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → ∀dd,ee. ≽ [dd, ee] L1 →
                           d + e ≤ dd → ≽ [dd - e, ee] L2.
 #L1 #L2 #d #e #HL12 #dd #ee #HL1 #Hddee
 @sfr_ldrop #I #K2 #V2 #i #Hddi #Hiddee #HLK2
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_lift.ma
index 3e18bff32..81f2b49a9 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_lift.ma
@@ -84,7 +84,7 @@ theorem lift_div_be: ∀d1,e1,T1,T. ⇧[d1, e1] T1 ≡ T →
   | >(lift_inv_lref2_ge … H ?) -H //
     lapply (le_plus_to_minus … Hie1d1e2) #Hd1e21i
     elim (le_inv_plus_l … Hie1d1e2) -Hie1d1e2 #Hd1e12 #He2ie1
-    @ex2_1_intro [2: /2 width=1/ | skip ] -Hd1e12
+    @ex2_intro [2: /2 width=1/ | skip ] -Hd1e12
     @lift_lref_ge_minus_eq [ >plus_minus_commutative // | /2 width=1/ ]
   ]
 | #p #d1 #e1 #e #e2 #T2 #H >(lift_inv_gref2 … H) -H /2 width=3/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma
index ab11536bd..6872e4b2b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma
@@ -106,9 +106,8 @@ lemma tps_split_up: ∀L,T1,T2,d,e. L ⊢ T1 ▶ [d, e] T2 → ∀i. d ≤ i →
   elim (lt_or_ge i j)
   [ -Hide -Hjde
     >(plus_minus_m_m j d) in ⊢ (% → ?); // -Hdj /3 width=4/
-  | -Hdi -Hdj #Hid
-    generalize in match Hide; -Hide (**) (* rewriting in the premises, rewrites in the goal too *)
-    >(plus_minus_m_m … Hjde) in ⊢ (% → ?); -Hjde /4 width=4/
+  | -Hdi -Hdj #Hij
+    lapply (plus_minus_m_m … Hjde) -Hjde /3 width=8/
   ]
 | #L #a #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #i #Hdi #Hide
   elim (IHV12 i ? ?) -IHV12 // #V #HV1 #HV2
@@ -129,7 +128,7 @@ lemma tps_split_down: ∀L,T1,T2,d,e. L ⊢ T1 ▶ [d, e] T2 →
 [ /2 width=3/
 | #L #K #V #W #i #d #e #Hdi #Hide #HLK #HVW #j #Hdj #Hjde
   elim (lt_or_ge i j)
-  [ -Hide -Hjde >(plus_minus_m_m j d) in ⊢ (% → ?); // -Hdj /4 width=4/
+  [ -Hide -Hjde >(plus_minus_m_m j d) in ⊢ (% → ?); // -Hdj /3 width=8/
   | -Hdi -Hdj
     >(plus_minus_m_m (d+e) j) in Hide; // -Hjde /3 width=4/
   ]
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/tps_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/tps_lift.ma
index 5ffc94922..808f6e3ba 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/tps_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/tps_lift.ma
@@ -181,7 +181,7 @@ lemma tps_inv_lift1_be: ∀L,U1,U2,dt,et. L ⊢ U1 ▶ [dt, et] U2 →
     lapply (ldrop_conf_ge … HLK … HLKV ?) -L // #HKV
     elim (lift_split … HVW d (i - e + 1) ? ? ?) -HVW [4: // |3: /2 width=1/ |2: /3 width=1/ ] -Hid -Hdie
     #V1 #HV1 >plus_minus // <minus_minus // /2 width=1/ <minus_n_n <plus_n_O #H
-    @ex2_1_intro [3: @H | skip | @tps_subst [3,5,6: // |1,2: skip | >commutative_plus >plus_minus // /2 width=1/ ] ] (**) (* explicit constructor, uses monotonic_lt_minus_l *)
+    @ex2_intro [3: @H | skip | @tps_subst [3,5,6: // |1,2: skip | >commutative_plus >plus_minus // /2 width=1/ ] ] (**) (* explicit constructor, uses monotonic_lt_minus_l *)
   ]
 | #L #a #I #V1 #V2 #U1 #U2 #dt #et #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H #Hdtd #Hdedet
   elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
@@ -214,7 +214,7 @@ lemma tps_inv_lift1_ge: ∀L,U1,U2,dt,et. L ⊢ U1 ▶ [dt, et] U2 →
   lapply (ldrop_conf_ge … HLK … HLKV ?) -L // #HKV
   elim (lift_split … HVW d (i - e + 1) ? ? ?) -HVW [4: // |3: /2 width=1/ |2: /3 width=1/ ] -Hdei -Hdie 
   #V0 #HV10 >plus_minus // <minus_minus // /2 width=1/ <minus_n_n <plus_n_O #H
-  @ex2_1_intro [3: @H | skip | @tps_subst [5,6: // |1,2: skip | /2 width=1/ | >plus_minus // /2 width=1/ ] ] (**) (* explicit constructor, uses monotonic_lt_minus_l *)
+  @ex2_intro [3: @H | skip | @tps_subst [5,6: // |1,2: skip | /2 width=1/ | >plus_minus // /2 width=1/ ] ] (**) (* explicit constructor, uses monotonic_lt_minus_l *)
 | #L #a #I #V1 #V2 #U1 #U2 #dt #et #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H #Hdetd
   elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
   elim (le_inv_plus_l … Hdetd) #_ #Hedt
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/tps_tps.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/tps_tps.ma
index 3882750bd..a99b352ab 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/tps_tps.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/tps_tps.ma
@@ -26,7 +26,7 @@ theorem tps_conf_eq: ∀L,T0,T1,d1,e1. L ⊢ T0 ▶ [d1, e1] T1 →
 [ /2 width=3/
 | #L #K1 #V1 #T1 #i0 #d1 #e1 #Hd1 #Hde1 #HLK1 #HVT1 #T2 #d2 #e2 #H
   elim (tps_inv_lref1 … H) -H
-  [ #HX destruct /4 width=4/
+  [ #HX destruct /3 width=6/
   | -Hd1 -Hde1 * #K2 #V2 #_ #_ #HLK2 #HVT2
     lapply (ldrop_mono … HLK1 … HLK2) -HLK1 -HLK2 #H destruct
     >(lift_mono … HVT1 … HVT2) -HVT1 -HVT2 /2 width=3/
@@ -54,7 +54,7 @@ theorem tps_conf_neq: ∀L1,T0,T1,d1,e1. L1 ⊢ T0 ▶ [d1, e1] T1 →
 [ /2 width=3/
 | #L1 #K1 #V1 #T1 #i0 #d1 #e1 #Hd1 #Hde1 #HLK1 #HVT1 #L2 #T2 #d2 #e2 #H1 #H2
   elim (tps_inv_lref1 … H1) -H1
-  [ #H destruct /4 width=4/
+  [ #H destruct /3 width=6/
   | -HLK1 -HVT1 * #K2 #V2 #Hd2 #Hde2 #_ #_ elim H2 -H2 #Hded
     [ -Hd1 -Hde2
       lapply (transitive_le … Hded Hd2) -Hded -Hd2 #H
@@ -116,7 +116,7 @@ theorem tps_trans_down: ∀L,T1,T0,d1,e1. L ⊢ T1 ▶ [d1, e1] T0 →
 | #L #K #V #W #i1 #d1 #e1 #Hdi1 #Hide1 #HLK #HVW #T2 #d2 #e2 #HWT2 #Hde2d1
   lapply (transitive_le … Hde2d1 Hdi1) -Hde2d1 #Hde2i1
   lapply (tps_weak … HWT2 0 (i1 + 1) ? ?) -HWT2 normalize /2 width=1/ -Hde2i1 #HWT2
-  <(tps_inv_lift1_eq … HWT2 … HVW) -HWT2 /4 width=4/
+  <(tps_inv_lift1_eq … HWT2 … HVW) -HWT2 /3 width=8/
 | #L #a #I #V1 #V0 #T1 #T0 #d1 #e1 #_ #_ #IHV10 #IHT10 #X #d2 #e2 #HX #de2d1
   elim (tps_inv_bind1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct
   lapply (tps_lsubs_trans … HT02 (L. ⓑ{I} V0) ?) -HT02 /2 width=1/ #HT02
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_alt.ma
index 9a3eb1b7c..6828b50b7 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_alt.ma
@@ -49,8 +49,8 @@ lemma delifta_lsubs_trans: ∀L1,T1,T2,d,e. L1 ⊢ ▼▼*[d, e] T1 ≡ T2 →
 qed.
 
 lemma delift_delifta: ∀L,T1,T2,d,e. L ⊢ ▼*[d, e] T1 ≡ T2 → L ⊢ ▼▼*[d, e] T1 ≡ T2.
-#L #T1 @(fw_ind … L T1) -L -T1 #L #T1 elim T1 -T1
-[ * #i #IH #T2 #d #e #H
+#L #T1 @(f2_ind … fw … L T1) -L -T1 #n #IH #L *
+[ * #i #Hn #T2 #d #e #H destruct
   [ >(delift_inv_sort1 … H) -H //
   | elim (delift_inv_lref1 … H) -H * /2 width=1/
     #K #V1 #V2 #Hdi #Hide #HLK #HV12 #HVT2
@@ -58,7 +58,7 @@ lemma delift_delifta: ∀L,T1,T2,d,e. L ⊢ ▼*[d, e] T1 ≡ T2 → L ⊢ ▼
     lapply (IH … HV12) // -H /2 width=6/
   | >(delift_inv_gref1 … H) -H //
   ]
-| * [ #a ] #I #V1 #T1 #_ #_ #IH #X #d #e #H
+| * [ #a ] #I #V1 #T1 #Hn #X #d #e #H
   [ elim (delift_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
     lapply (delift_lsubs_trans … HT12 (L.ⓑ{I}V1) ?) -HT12 /2 width=1/ #HT12
     lapply (IH … HV12) -HV12 // #HV12
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_lift.ma
index 01ee6108e..259150909 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_lift.ma
@@ -27,13 +27,14 @@ lemma delift_lref_be: ∀L,K,V1,V2,U2,i,d,e. d ≤ i → i < d + e →
 elim (lift_total V 0 (i+1)) #U #HVU
 lapply (lift_trans_be … HV2 … HVU ? ?) -HV2 // >minus_plus <plus_minus_m_m /2 width=1/ #HV2U 
 lapply (lift_conf_be … HVU2 … HV2U ?) //
->commutative_plus in ⊢ (??%??→?); <minus_plus_m_m /3 width=6/ 
+>commutative_plus in ⊢ (??%??→?); <minus_plus_m_m /3 width=6/
 qed.
 
-fact sfr_delift_aux: ∀L,T,T1,d,e. d + e ≤ |L| → ≽ [d, e] L → T = T1 →
-                     ∃T2. L ⊢ ▼*[d, e] T1 ≡ T2.
-#L #T @(fw_ind … L T) -L -T #L #T #IH * * /2 width=2/
-[ #i #d #e #Hde #HL #H destruct
+lemma sfr_delift: ∀L,T1,d,e. d + e ≤ |L| → ≽ [d, e] L →
+                  ∃T2. L ⊢ ▼*[d, e] T1 ≡ T2.
+#L #T1 @(f2_ind … fw … L T1) -L -T1
+#n #IH #L * * /2 width=2/
+[ #i #H #d #e #Hde #HL destruct
   elim (lt_or_ge i d) #Hdi [ /3 width=2/ ]
   elim (lt_or_ge i (d+e)) #Hide [2: /3 width=2/ ]
   lapply (lt_to_le_to_lt … Hide Hde) #Hi
@@ -44,22 +45,18 @@ fact sfr_delift_aux: ∀L,T,T1,d,e. d + e ≤ |L| → ≽ [d, e] L → T = T1 
   lapply (ldrop_fwd_O1_length … HLK0) #H
   lapply (sfr_ldrop_trans_be_up … HLK0 … HL ? ?) -HLK0 -HL
   [1,2: /2 width=1/ | <minus_n_O <minus_plus ] #HK
-  elim (IH … HKL … HK ?) -IH -HKL -HK
-  [3: // |2: skip |4: >H -H /2 width=1/ ] -Hde -H #V2 #V12 (**) (* H erased two times *)
+  elim (IH … HKL … HK) -IH -HKL -HK
+  [2: >H -H /2 width=1/ ] -Hde -H #V2 #V12 (**) (* H erased two times *)
   elim (lift_total V2 0 d) /3 width=7/
-| #a #I #V1 #T1 #d #e #Hde #HL #H destruct
-  elim (IH … V1 … Hde HL ?) [2,4: // |3: skip ] #V2 #HV12
-  elim (IH (L.ⓑ{I}V1) T1 ? ? (d+1) e ? ? ?) -IH [3,6: // |2: skip |4,5: /2 width=1/ ] -Hde -HL #T2 #HT12
+| #a #I #V1 #T1 #H #d #e #Hde #HL destruct
+  elim (IH … V1 … Hde HL) // #V2 #HV12
+  elim (IH (L.ⓑ{I}V1) T1 … (d+1) e ??) -IH // [2,3: /2 width=1/ ] -Hde -HL #T2 #HT12
   lapply (delift_lsubs_trans … HT12 (L.ⓑ{I}V2) ?) -HT12 /2 width=1/ /3 width=4/
-| #I #V1 #T1 #d #e #Hde #HL #H destruct
-  elim (IH … V1 … Hde HL ?) [2,4: // |3: skip ] #V2 #HV12
-  elim (IH … T1 … Hde HL ?) -IH -Hde -HL [3,4: // |2: skip ] /3 width=2/
+| #I #V1 #T1 #H #d #e #Hde #HL destruct
+  elim (IH … V1 … Hde HL) // #V2 #HV12
+  elim (IH … T1 … Hde HL) -IH -Hde -HL // /3 width=2/
 ]
-qed.
-
-lemma sfr_delift: ∀L,T1,d,e. d + e ≤ |L| → ≽ [d, e] L →
-                  ∃T2. L ⊢ ▼*[d, e] T1 ≡ T2.
-/2 width=2/ qed-.
+qed-.
 
 (* Advanced inversion lemmas ************************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/frsupp.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/frsupp.ma
index 9cfee7cfd..1fee98341 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/frsupp.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/frsupp.ma
@@ -39,6 +39,16 @@ lemma frsupp_ind_dx: ∀L2,T2. ∀R:relation2 lenv term.
 @(bi_TC_ind_dx … IH1 IH2 ? ? H)
 qed-.
 
+(* Baic inversion lemmas ****************************************************)
+
+lemma frsupp_inv_dx: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ ∨
+                     ∃∃L,T. ⦃L1, T1⦄ ⧁+ ⦃L, T⦄ & ⦃L, T⦄ ⧁ ⦃L2, T2⦄.
+/2 width=1 by bi_TC_decomp_r/ qed-.
+
+lemma frsupp_inv_sn: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ ∨
+                     ∃∃L,T. ⦃L1, T1⦄ ⧁ ⦃L, T⦄ & ⦃L, T⦄ ⧁+ ⦃L2, T2⦄.
+/2 width=1 by bi_TC_decomp_l/ qed-.
+
 (* Basic properties *********************************************************)
 
 lemma frsup_frsupp: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄.
@@ -79,29 +89,18 @@ qed-.
 
 (* Advanced forward lemmas **************************************************)
 
-fact lift_frsupp_trans_aux: ∀L2,U0. (
-                               ∀L,K,U1,U2. ⦃L, U1⦄ ⧁+ ⦃L @@ K, U2⦄ →
-                               ∀T1,d,e. ⇧[d, e] T1 ≡ U1 →
-                               #{L, U1} < #{L2, U0} → 
-                               ∃T2. ⇧[d + |K|, e] T2 ≡ U2
-                            ) →
-                            ∀L1,K,U1,U2. ⦃L1, U1⦄ ⧁+ ⦃L2 @@ K, U2⦄ →
-                            ∀T1,d,e. ⇧[d, e] T1 ≡ U1 →
-                            L2 = L1 → U0 = U1 →
-                            ∃T2. ⇧[d + |K|, e] T2 ≡ U2.
-#L2 #U0 #IH #L1 #X #U1 #U2 #H @(frsupp_ind_dx … H) -L1 -U1 /2 width=5 by lift_frsup_trans/
-#L1 #L #U1 #U #HL1 #HL2 #_ #T1 #d #e #HTU1 #H1 #H2 destruct
-elim (frsup_fwd_append … HL1) #K1 #H destruct
-elim (frsupp_fwd_append … HL2) #K >append_assoc #H
-elim (append_inj_dx … H ?) -H // #_ #H destruct
-<append_assoc in HL2; #HL2
-elim (lift_frsup_trans … HTU1 … HL1) -T1 #T #HTU
-lapply (frsup_fwd_fw … HL1) -HL1 #HL1
-elim (IH … HL2 … HTU ?) -IH -HL2 -T // -L1 -U1 -U /2 width=2/
-qed-.
-
 lemma lift_frsupp_trans: ∀L,U1,K,U2. ⦃L, U1⦄ ⧁+ ⦃L @@ K, U2⦄ →
                          ∀T1,d,e. ⇧[d, e] T1 ≡ U1 →
                          ∃T2. ⇧[d + |K|, e] T2 ≡ U2.
-#L #U1 @(fw_ind … L U1) -L -U1 /3 width=10 by lift_frsupp_trans_aux/
+#L #U1 @(f2_ind … fw … L U1) -L -U1 #n #IH
+#L #U1 #Hn #K #U2 #H #T1 #d #e #HTU1 destruct
+elim (frsupp_inv_sn … H) -H /2 width=5 by lift_frsup_trans/ *
+#L0 #U0 #HL0 #HL
+elim (frsup_fwd_append … HL0) #K0 #H destruct
+elim (frsupp_fwd_append … HL) #L0 >append_assoc #H
+elim (append_inj_dx … H ?) -H // #_ #H destruct
+<append_assoc in HL; #HL
+elim (lift_frsup_trans … HTU1 … HL0) -T1 #T #HTU
+lapply (frsup_fwd_fw … HL0) -HL0 #HL0
+elim (IH … HL … HTU) -IH -HL -T // -L -U1 -U0 /2 width=2/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_ltpss_dx.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_ltpss_dx.ma
index 5ea9f6bd6..67867f8c8 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_ltpss_dx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_ltpss_dx.ma
@@ -13,7 +13,6 @@
 (**************************************************************************)
 
 include "basic_2/unfold/tpss_tpss.ma".
-include "basic_2/unfold/tpss_alt.ma".
 include "basic_2/unfold/ltpss_dx_tpss.ma".
 
 (* DX PARTIAL UNFOLD ON LOCAL ENVIRONMENTS **********************************)
@@ -43,93 +42,65 @@ lemma ltpss_dx_tpss_trans_down: ∀L0,L1,T2,U2,d1,e1,d2,e2. d2 + e2 ≤ d1 →
 ]
 qed.
 
-fact ltpss_dx_tpss_trans_eq_aux: ∀Y1,X2,L1,T2,U2,d,e.
-                                 L1 ⊢ T2 ▶* [d, e] U2 → ∀L0. L0 ▶* [d, e] L1 →
-                                 Y1 = L1 → X2 = T2 → L0 ⊢ T2 ▶* [d, e] U2.
-#Y1 #X2 @(fw_ind … Y1 X2) -Y1 -X2 #Y1 #X2 #IH
-#L1 #T2 #U2 #d #e #H @(tpss_ind_alt … H) -L1 -T2 -U2 -d -e
-[ //
-| #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #HV12 #HVW2 #_ #L0 #HL01 #H1 #H2 destruct
+lemma ltpss_dx_tpss_trans_eq: ∀L1,T2,U2,d,e. L1 ⊢ T2 ▶* [d, e] U2 →
+                              ∀L0. L0 ▶* [d, e] L1 → L0 ⊢ T2 ▶* [d, e] U2.
+#L1 #T2 @(f2_ind … fw … L1 T2) -L1 -T2 #n #IH #L1 *
+[ #I #Hn #W2 #d #e #H #L0 #HL01 destruct
+  elim (tpss_inv_atom1 … H) -H // *
+  #K1 #V1 #V2 #i #Hdi #Hide #HLK1 #HV12 #HVW2 #H destruct
   lapply (ldrop_fwd_lw … HLK1) #H1 normalize in H1;
   elim (ltpss_dx_ldrop_trans_be … HL01 … HLK1 ? ?) -HL01 -HLK1 // /2 width=2/ #X #H #HLK0
   elim (ltpss_dx_inv_tpss22 … H ?) -H /2 width=1/ #K0 #V0 #HK01 #HV01 #H destruct
   lapply (tpss_fwd_tw … HV01) #H2
   lapply (transitive_le (#{K1} + #{V0}) … H1) -H1 /2 width=1/ -H2 #H
   lapply (tpss_trans_eq … HV01 HV12) -V1 #HV02
-  lapply (IH … HV02 … HK01 ? ?) -IH -HV02 -HK01
-  [1,3: // |2,4: skip | normalize /2 width=1/ | /2 width=6/ ]
-| #L #a #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #_ #_ #L0 #HL0 #H1 #H2 destruct
-  lapply (tpss_lsubs_trans … HT12 (L. ⓑ{I} V1) ?) -HT12 /2 width=1/ #HT12
-  lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3: // |2,4: skip |5: /2 width=2/ ] #HV12
-  lapply (IH … HT12 (L0. ⓑ{I} V1) ? ? ?) -IH -HT12 [1,3,5: /2 width=2/ |2,4: skip | normalize // ] -HL0 #HT12
-  lapply (tpss_lsubs_trans … HT12 (L0. ⓑ{I} V2) ?) -HT12 /2 width=1/
-| #L #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #_ #_ #L0 #HL0 #H1 #H2 destruct
-  lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3: // |2,4: skip |5: /2 width=3/ ]
-  lapply (IH … HT12 … HL0 ? ?) -IH -HT12 [1,3,5: normalize // |2,4: skip ] -HL0 /2 width=1/
+  lapply (IH … HV02 … HK01) -IH -HV02 -HK01
+  [ normalize /2 width=1/ | /2 width=6/ ]
+| * [ #a ] #I #V2 #T2 #Hn #X #d #e #H #L0 #HL0 destruct
+  [ elim (tpss_inv_bind1 … H) -H #W2 #U2 #HVW2 #HTU2 #H destruct
+    lapply (tpss_lsubs_trans … HTU2 (L1. ⓑ{I} V2) ?) -HTU2 /2 width=1/ #HTU2
+    lapply (IH … HVW2 … HL0) -HVW2 [ /2 width=2/ ] #HVW2
+    lapply (IH … HTU2 (L0. ⓑ{I} V2) ?) -IH -HTU2 // /2 width=2/ -HL0 #HTU2
+    lapply (tpss_lsubs_trans … HTU2 (L0. ⓑ{I} W2) ?) -HTU2 /2 width=1/
+  | elim (tpss_inv_flat1 … H) -H #W2 #U2 #HVW2 #HTU2 #H destruct
+    lapply (IH … HVW2 … HL0) -HVW2 //
+    lapply (IH … HTU2 … HL0) -IH -HTU2 // -HL0 /2 width=1/
 ]
 qed.
 
-lemma ltpss_dx_tpss_trans_eq: ∀L1,T2,U2,d,e. L1 ⊢ T2 ▶* [d, e] U2 →
-                              ∀L0. L0 ▶* [d, e] L1 → L0 ⊢ T2 ▶* [d, e] U2.
-/2 width=5/ qed.
-
 lemma ltpss_dx_tps_trans_eq: ∀L0,L1,T2,U2,d,e. L0 ▶* [d, e] L1 →
                              L1 ⊢ T2 ▶ [d, e] U2 → L0 ⊢ T2 ▶* [d, e] U2.
 /3 width=3/ qed.
 
 (* Main properties **********************************************************)
 
-fact ltpss_dx_conf_aux: ∀K,K1,L1,d1,e1. K1 ▶* [d1, e1] L1 →
-                        ∀K2,L2,d2,e2. K2 ▶* [d2, e2] L2 → K1 = K → K2 = K →
-                        ∃∃L. L1 ▶* [d2, e2] L & L2 ▶* [d1, e1] L.
-#K @(lw_ind … K) -K #K #IH #K1 #L1 #d1 #e1 * -K1 -L1 -d1 -e1
-[ -IH /2 width=3/
-| -IH #K1 #I1 #V1 #K2 #L2 #d2 #e2 * -K2 -L2 -d2 -e2
-  [ /2 width=3/
-  | #K2 #I2 #V2 #H1 #H2 destruct /2 width=3/
-  | #K2 #L2 #I2 #W2 #V2 #e2 #HKL2 #HWV2 #H1 #H2 destruct /3 width=3/
-  | #K2 #L2 #I2 #W2 #V2 #d2 #e2 #HKL2 #HWV2 #H1 #H2 destruct /3 width=3/
-  ]
-| #K1 #L1 #I1 #W1 #V1 #e1 #HKL1 #HWV1 #K2 #L2 #d2 #e2 * -K2 -L2 -d2 -e2
-  [ -IH #d2 #e2 #H1 #H2 destruct
-  | -IH #K2 #I2 #V2 #H1 #H2 destruct /3 width=5/
-  | #K2 #L2 #I2 #W2 #V2 #e2 #HKL2 #HWV2 #H1 #H2 destruct
-    elim (IH … HKL1 … HKL2 ? ?) -IH [2,4: // |3: skip |5: /2 width=1/ ] -K1 #L #HL1 #HL2
-    elim (ltpss_dx_tpss_conf … HWV1 … HL1) #U1 #HWU1 #HVU1
-    elim (ltpss_dx_tpss_conf … HWV2 … HL2) #U2 #HWU2 #HVU2
-    elim (tpss_conf_eq … HWU1 … HWU2) -W1 #W #HU1W #HU2W
-    lapply (tpss_trans_eq … HVU1 HU1W) -U1
-    lapply (tpss_trans_eq … HVU2 HU2W) -U2 /3 width=5/
-  | #K2 #L2 #I2 #W2 #V2 #d2 #e2 #HKL2 #HWV2 #H1 #H2 destruct
-    elim (IH … HKL1 … HKL2 ? ?) -IH [2,4: // |3: skip |5: /2 width=1/ ] -K1 #L #HL1 #HL2
-    elim (ltpss_dx_tpss_conf … HWV1 … HL1) #U1 #HWU1 #HVU1
-    elim (ltpss_dx_tpss_conf … HWV2 … HL2) #U2 #HWU2 #HVU2
-    elim (tpss_conf_eq … HWU1 … HWU2) -W1 #W #HU1W #HU2W
-    lapply (tpss_trans_eq … HVU1 HU1W) -U1
-    lapply (tpss_trans_eq … HVU2 HU2W) -U2 /3 width=5/
-  ]
-| #K1 #L1 #I1 #W1 #V1 #d1 #e1 #HKL1 #HWV1 #K2 #L2 #d2 #e2 * -K2 -L2 -d2 -e2
-  [ -IH #d2 #e2 #H1 #H2 destruct
-  | -IH #K2 #I2 #V2 #H1 #H2 destruct /3 width=5/
-  | #K2 #L2 #I2 #W2 #V2 #e2 #HKL2 #HWV2 #H1 #H2 destruct
-    elim (IH … HKL1 … HKL2 ? ?) -IH [2,4: // |3: skip |5: /2 width=1/ ] -K1 #L #HL1 #HL2
-    elim (ltpss_dx_tpss_conf … HWV1 … HL1) #U1 #HWU1 #HVU1
-    elim (ltpss_dx_tpss_conf … HWV2 … HL2) #U2 #HWU2 #HVU2
-    elim (tpss_conf_eq … HWU1 … HWU2) -W1 #W #HU1W #HU2W
-    lapply (tpss_trans_eq … HVU1 HU1W) -U1
-    lapply (tpss_trans_eq … HVU2 HU2W) -U2 /3 width=5/
-  | #K2 #L2 #I2 #W2 #V2 #d2 #e2 #HKL2 #HWV2 #H1 #H2 destruct
-    elim (IH … HKL1 … HKL2 ? ?) -IH [2,4: // |3: skip |5: /2 width=1/ ] -K1 #L #HL1 #HL2
-    elim (ltpss_dx_tpss_conf … HWV1 … HL1) #U1 #HWU1 #HVU1
-    elim (ltpss_dx_tpss_conf … HWV2 … HL2) #U2 #HWU2 #HVU2
-    elim (tpss_conf_eq … HWU1 … HWU2) -W1 #W #HU1W #HU2W
-    lapply (tpss_trans_eq … HVU1 HU1W) -U1
-    lapply (tpss_trans_eq … HVU2 HU2W) -U2 /3 width=5/
-  ]
-]
-qed.
-
 theorem ltpss_dx_conf: ∀L0,L1,d1,e1. L0 ▶* [d1, e1] L1 →
                        ∀L2,d2,e2. L0 ▶* [d2, e2] L2 →
                        ∃∃L. L1 ▶* [d2, e2] L & L2 ▶* [d1, e1] L.
-/2 width=7/ qed.
+#L0 @(f_ind … lw … L0) -L0 #n #IH *
+[ #_ #L1 #d1 #e1 #H1 #L2 #d2 #e2 #H2 -n
+  >(ltpss_dx_inv_atom1 … H1) -L1
+  >(ltpss_dx_inv_atom1 … H2) -L2 /2 width=3/
+| #K0 #I0 #V0 #Hn #L1 #d1 #e1 #H1 #L2 #d2 #e2 #H2 destruct
+  elim (eq_or_gt d1) #Hd1 [ elim (eq_or_gt e1) #He1 ] destruct
+  [ lapply (ltpss_dx_inv_refl_O2 … H1) -H1 #H1
+  | elim (ltpss_dx_inv_tpss21 … H1 … He1) -H1 #K1 #V1 #HK01 #HV01 #H1
+  | elim (ltpss_dx_inv_tpss11 … H1 … Hd1) -H1 #K1 #V1 #HK01 #HV01 #H1
+  ] destruct
+  elim (eq_or_gt d2) #Hd2 [1,3,5: elim (eq_or_gt e2) #He2 ] destruct
+  [1,3,5: lapply (ltpss_dx_inv_refl_O2 … H2) -H2 #H2
+  |2,4,6: elim (ltpss_dx_inv_tpss21 … H2 … He2) -H2 #K2 #V2 #HK02 #HV02 #H2
+  |7,8,9: elim (ltpss_dx_inv_tpss11 … H2 … Hd2) -H2 #K2 #V2 #HK02 #HV02 #H2
+  ] destruct
+  [1: -IH /2 width=3/
+  |2,3,4,7: -IH /3 width=5/
+  |5,6,8,9:
+    elim (IH … HK01 … HK02) // -K0 #K #HK1 #HK2
+    elim (ltpss_dx_tpss_conf … HV01 … HK1) -HV01 #W1 #HW1 #HVW1
+    elim (ltpss_dx_tpss_conf … HV02 … HK2) -HV02 #W2 #HW2 #HVW2
+    elim (tpss_conf_eq … HW1 … HW2) -V0 #V #HW1 #HW2
+    lapply (tpss_trans_eq … HVW1 HW1) -W1
+    lapply (tpss_trans_eq … HVW2 HW2) -W2 /3 width=5/
+  ]
+]
+qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_alt.ma
index 7a453d270..8b414d203 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_alt.ma
@@ -106,7 +106,7 @@ lemma ltpss_sn_strip: ∀L0,L1,d1,e1. L0 ⊢ ▶* [d1, e1] L1 →
 #L0 #L1 #d1 #e1 #H #L2 #d2 #e2 #HL02
 lapply (ltpss_sn_ltpssa … H) -H #HL01
 elim (ltpssa_strip … HL01 … HL02) -L0
-/3 width=3 by ltpssa_ltpss_sn, ex2_1_intro/
+/3 width=3 by ltpssa_ltpss_sn, ex2_intro/
 qed.
 
 (* Note: this should go in ltpss_sn_ltpss_sn.ma *)
@@ -152,5 +152,5 @@ theorem ltpss_sn_conf: ∀L0,L1,d1,e1. L0 ⊢ ▶* [d1, e1] L1 →
 lapply (ltpss_sn_ltpssa … H1) -H1 #HL01
 lapply (ltpss_sn_ltpssa … H2) -H2 #HL02
 elim (ltpssa_conf … HL01 … HL02) -L0
-/3 width=3 by ltpssa_ltpss_sn, ex2_1_intro/
+/3 width=3 by ltpssa_ltpss_sn, ex2_intro/
 qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_ltpss_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_ltpss_sn.ma
index 10a190143..dfcd35c73 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_ltpss_sn.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_ltpss_sn.ma
@@ -13,40 +13,35 @@
 (**************************************************************************)
 
 include "basic_2/unfold/tpss_tpss.ma".
-include "basic_2/unfold/tpss_alt.ma".
 include "basic_2/unfold/ltpss_sn_tpss.ma".
 
 (* PARTIAL UNFOLD ON LOCAL ENVIRONMENTS *************************************)
 
 (* Advanced properties ******************************************************)
 
-fact ltpss_sn_tpss_trans_eq_aux: ∀Y1,X2,L1,T2,U2,d,e.
-                                 L1 ⊢ T2 ▶* [d, e] U2 → ∀L0. L0 ⊢ ▶* [d, e] L1 →
-                                 Y1 = L1 → X2 = T2 → L0 ⊢ T2 ▶* [d, e] U2.
-#Y1 #X2 @(fw_ind … Y1 X2) -Y1 -X2 #Y1 #X2 #IH
-#L1 #T2 #U2 #d #e #H @(tpss_ind_alt … H) -L1 -T2 -U2 -d -e
-[ //
-| #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #HV12 #HVW2 #_ #L0 #HL01 #H1 #H2 destruct
+lemma ltpss_sn_tpss_trans_eq: ∀L1,T2,U2,d,e. L1 ⊢ T2 ▶* [d, e] U2 →
+                              ∀L0. L0 ⊢ ▶* [d, e] L1 → L0 ⊢ T2 ▶* [d, e] U2.
+#L1 #T2 @(f2_ind … fw … L1 T2) -L1 -T2 #n #IH #L1 *
+[ #I #Hn #W2 #d #e #H #L0 #HL01 destruct
+  elim (tpss_inv_atom1 … H) -H // *
+  #K1 #V1 #V2 #i #Hdi #Hide #HLK1 #HV12 #HVW2 #H destruct
   lapply (ldrop_fwd_lw … HLK1) #H1 normalize in H1;
   elim (ltpss_sn_ldrop_trans_be … HL01 … HLK1 ? ?) -HL01 -HLK1 // /2 width=2/ #X #H #HLK0
   elim (ltpss_sn_inv_tpss22 … H ?) -H /2 width=1/ #K0 #V0 #HK01 #HV01 #H destruct
-  lapply (IH … HV12 … HK01 ? ?) -IH -HV12 -HK01 [1,3: // |2,4: skip | normalize /2 width=1/ ] #HV12 
+  lapply (IH … HV12 … HK01) -IH -HV12 -HK01 [ normalize /2 width=1/ ] #HV12
   lapply (tpss_trans_eq … HV01 HV12) -V1 /2 width=6/
-| #L #a #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #_ #_ #L0 #HL0 #H1 #H2 destruct
-  lapply (tpss_lsubs_trans … HT12 (L. ⓑ{I} V1) ?) -HT12 /2 width=1/ #HT12
-  lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3: // |2,4: skip |5: /2 width=2/ ] #HV12
-  lapply (IH … HT12 (L0. ⓑ{I} V1) ? ? ?) -IH -HT12 [1,3,5: /2 width=2/ |2,4: skip | normalize // ] -HL0 #HT12
-  lapply (tpss_lsubs_trans … HT12 (L0. ⓑ{I} V2) ?) -HT12 /2 width=1/
-| #L #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #_ #_ #L0 #HL0 #H1 #H2 destruct
-  lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3: // |2,4: skip |5: /2 width=3/ ]
-  lapply (IH … HT12 … HL0 ? ?) -IH -HT12 [1,3,5: normalize // |2,4: skip ] -HL0 /2 width=1/
+| * [ #a ] #I #V2 #T2 #Hn #X #d #e #H #L0 #HL0 destruct
+  [ elim (tpss_inv_bind1 … H) -H #W2 #U2 #HVW2 #HTU2 #H destruct
+    lapply (tpss_lsubs_trans … HTU2 (L1. ⓑ{I} V2) ?) -HTU2 /2 width=1/ #HTU2
+    lapply (IH … HVW2 … HL0) -HVW2 [ /2 width=2/ ] #HVW2
+    lapply (IH … HTU2 (L0. ⓑ{I} V2) ?) -IH -HTU2 // /2 width=2/ -HL0 #HTU2
+    lapply (tpss_lsubs_trans … HTU2 (L0. ⓑ{I} W2) ?) -HTU2 /2 width=1/
+  | elim (tpss_inv_flat1 … H) -H #W2 #U2 #HVW2 #HTU2 #H destruct
+    lapply (IH … HVW2 … HL0) -HVW2 //
+    lapply (IH … HTU2 … HL0) -IH -HTU2 // -HL0 /2 width=1/
 ]
 qed.
 
-lemma ltpss_sn_tpss_trans_eq: ∀L1,T2,U2,d,e. L1 ⊢ T2 ▶* [d, e] U2 →
-                              ∀L0. L0 ⊢ ▶* [d, e] L1 → L0 ⊢ T2 ▶* [d, e] U2.
-/2 width=5/ qed.
-
 lemma ltpss_sn_tps_trans_eq: ∀L0,L1,T2,U2,d,e. L0 ⊢ ▶* [d, e] L1 →
                              L1 ⊢ T2 ▶ [d, e] U2 → L0 ⊢ T2 ▶* [d, e] U2.
 /3 width=3/ qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_tpss.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_tpss.ma
index 3f41b0083..d124bb32c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_tpss.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_tpss.ma
@@ -56,7 +56,7 @@ lemma tpss_split_up: ∀L,T1,T2,d,e. L ⊢ T1 ▶* [d, e] T2 →
 | #T #T2 #_ #HT12 * #T3 #HT13 #HT3
   elim (tps_split_up … HT12 … Hdi Hide) -HT12 -Hide #T0 #HT0 #HT02
   elim (tpss_strap1_down … HT3 … HT0 ?) -T [2: >commutative_plus /2 width=1/ ]
-  /3 width=7 by ex2_1_intro, step/ (**) (* just /3 width=7/ is too slow *)
+  /3 width=7 by ex2_intro, step/ (**) (* just /3 width=7/ is too slow *)
 ]
 qed.
 
diff --git a/matita/matita/contribs/lambdadelta/ground_2/star.ma b/matita/matita/contribs/lambdadelta/ground_2/star.ma
index 1e46a48c6..431ef80a8 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/star.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/star.ma
@@ -20,10 +20,6 @@ include "ground_2/notation.ma".
 
 definition Decidable: Prop → Prop ≝ λR. R ∨ (R → ⊥).
 
-definition Confluent: ∀A. ∀R: relation A. Prop ≝ λA,R.
-                      ∀a0,a1. R a0 a1 → ∀a2. R a0 a2 →
-                      ∃∃a. R a1 a & R a2 a.
-
 definition Transitive: ∀A. ∀R: relation A. Prop ≝ λA,R.
                        ∀a1,a0. R a1 a0 → ∀a2. R a0 a2 → R a1 a2.
 
@@ -47,7 +43,7 @@ lemma TC_strip1: ∀A,R1,R2. confluent2 A R1 R2 →
   elim (HR12 … Ha01 … Ha02) -HR12 -a0 /3 width=3/
 | #a #a1 #_ #Ha1 #IHa0 #a2 #Ha02
   elim (IHa0 … Ha02) -a0 #a0 #Ha0 #Ha20
-  elim (HR12 … Ha1 … Ha0) -HR12 -a /4 width=3/
+  elim (HR12 … Ha1 … Ha0) -HR12 -a /4 width=5/
 ]
 qed.
 
@@ -70,7 +66,7 @@ lemma TC_confluent2: ∀A,R1,R2.
   elim (TC_strip2 … HR12 … Ha02 … Ha01) -HR12 -a0 /3 width=3/
 | #a #a1 #_ #Ha1 #IHa0 #a2 #Ha02
   elim (IHa0 … Ha02) -a0 #a0 #Ha0 #Ha20
-  elim (TC_strip2 … HR12 … Ha0 … Ha1) -HR12 -a /4 width=3/
+  elim (TC_strip2 … HR12 … Ha0 … Ha1) -HR12 -a /4 width=5/
 ]
 qed.
 
@@ -82,7 +78,7 @@ lemma TC_strap1: ∀A,R1,R2. transitive2 A R1 R2 →
   elim (HR12 … Ha10 … Ha02) -HR12 -a0 /3 width=3/
 | #a #a0 #_ #Ha0 #IHa #a2 #Ha02
   elim (HR12 … Ha0 … Ha02) -HR12 -a0 #a0 #Ha0 #Ha02
-  elim (IHa … Ha0) -a /4 width=3/
+  elim (IHa … Ha0) -a /4 width=5/
 ]
 qed.
 
@@ -105,7 +101,7 @@ lemma TC_transitive2: ∀A,R1,R2.
   elim (TC_strap2 … HR12 … Ha02 … Ha10) -HR12 -a0 /3 width=3/
 | #a #a0 #_ #Ha0 #IHa #a2 #Ha02
   elim (TC_strap2 … HR12 … Ha02 … Ha0) -HR12 -a0 #a0 #Ha0 #Ha02
-  elim (IHa … Ha0) -a /4 width=3/
+  elim (IHa … Ha0) -a /4 width=5/
 ]
 qed.
 
@@ -156,3 +152,20 @@ lemma bi_TC_confluent: ∀A,B,R. bi_confluent A B R →
   elim (bi_TC_strip … HR … H13 … H10) -a1 -b1 /3 width=7/
 ]
 qed.
+
+lemma bi_TC_decomp_r: ∀A,B. ∀R:bi_relation A B.
+                      ∀a1,a2,b1,b2. bi_TC … R a1 b1 a2 b2 →
+                      R a1 b1 a2 b2 ∨
+                      ∃∃a,b. bi_TC … R a1 b1 a b & R a b a2 b2.
+#A #B #R #a1 #a2 #b1 #b2 * -a2 -b2 /2 width=1/ /3 width=4/
+qed-.
+
+lemma bi_TC_decomp_l: ∀A,B. ∀R:bi_relation A B.
+                      ∀a1,a2,b1,b2. bi_TC … R a1 b1 a2 b2 →
+                      R a1 b1 a2 b2 ∨
+                      ∃∃a,b. R a1 b1 a b & bi_TC … R a b a2 b2.
+#A #B #R #a1 #a2 #b1 #b2 #H @(bi_TC_ind_dx ?????????? H) -a1 -b1
+[ /2 width=1/
+| #a1 #a #b1 #b #Hab1 #Hab2 #_ /3 width=4/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml b/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml
index c6a00c160..ddc63af0e 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml
+++ b/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml
@@ -10,13 +10,12 @@
 -->
   </section>
   <section name="xoa">
-    <key name="output_dir">contribs/lambda_delta/ground_2/</key>
+    <key name="output_dir">contribs/lambdadelta/ground_2/</key>
     <key name="objects">xoa</key>
     <key name="notations">xoa_notation</key>
     <key name="include">basics/pts.ma</key>
     <key name="ex">1 2</key>
     <key name="ex">1 3</key>
-    <key name="ex">2 1</key>
     <key name="ex">2 2</key>
     <key name="ex">2 3</key>
     <key name="ex">3 1</key>
diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa.ma b/matita/matita/contribs/lambdadelta/ground_2/xoa.ma
index ac4c8f9f7..06bbcb29c 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/xoa.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/xoa.ma
@@ -32,14 +32,6 @@ inductive ex1_3 (A0,A1,A2:Type[0]) (P0:A0→A1→A2→Prop) : Prop ≝
 
 interpretation "multiple existental quantifier (1, 3)" 'Ex P0 = (ex1_3 ? ? ? P0).
 
-(* multiple existental quantifier (2, 1) *)
-
-inductive ex2_1 (A0:Type[0]) (P0,P1:A0→Prop) : Prop ≝
-   | ex2_1_intro: ∀x0. P0 x0 → P1 x0 → ex2_1 ? ? ?
-.
-
-interpretation "multiple existental quantifier (2, 1)" 'Ex P0 P1 = (ex2_1 ? P0 P1).
-
 (* multiple existental quantifier (2, 2) *)
 
 inductive ex2_2 (A0,A1:Type[0]) (P0,P1:A0→A1→Prop) : Prop ≝
@@ -58,11 +50,11 @@ interpretation "multiple existental quantifier (2, 3)" 'Ex P0 P1 = (ex2_3 ? ? ?
 
 (* multiple existental quantifier (3, 1) *)
 
-inductive ex3_1 (A0:Type[0]) (P0,P1,P2:A0→Prop) : Prop ≝
-   | ex3_1_intro: ∀x0. P0 x0 → P1 x0 → P2 x0 → ex3_1 ? ? ? ?
+inductive ex3 (A0:Type[0]) (P0,P1,P2:A0→Prop) : Prop ≝
+   | ex3_intro: ∀x0. P0 x0 → P1 x0 → P2 x0 → ex3 ? ? ? ?
 .
 
-interpretation "multiple existental quantifier (3, 1)" 'Ex P0 P1 P2 = (ex3_1 ? P0 P1 P2).
+interpretation "multiple existental quantifier (3, 1)" 'Ex P0 P1 P2 = (ex3 ? P0 P1 P2).
 
 (* multiple existental quantifier (3, 2) *)
 
@@ -90,11 +82,11 @@ interpretation "multiple existental quantifier (3, 4)" 'Ex P0 P1 P2 = (ex3_4 ? ?
 
 (* multiple existental quantifier (4, 1) *)
 
-inductive ex4_1 (A0:Type[0]) (P0,P1,P2,P3:A0→Prop) : Prop ≝
-   | ex4_1_intro: ∀x0. P0 x0 → P1 x0 → P2 x0 → P3 x0 → ex4_1 ? ? ? ? ?
+inductive ex4 (A0:Type[0]) (P0,P1,P2,P3:A0→Prop) : Prop ≝
+   | ex4_intro: ∀x0. P0 x0 → P1 x0 → P2 x0 → P3 x0 → ex4 ? ? ? ? ?
 .
 
-interpretation "multiple existental quantifier (4, 1)" 'Ex P0 P1 P2 P3 = (ex4_1 ? P0 P1 P2 P3).
+interpretation "multiple existental quantifier (4, 1)" 'Ex P0 P1 P2 P3 = (ex4 ? P0 P1 P2 P3).
 
 (* multiple existental quantifier (4, 2) *)
 
diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa_notation.ma b/matita/matita/contribs/lambdadelta/ground_2/xoa_notation.ma
index 6f614f2e5..890f52739 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/xoa_notation.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/xoa_notation.ma
@@ -34,16 +34,6 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0)"
  non associative with precedence 20
  for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) }.
 
-(* multiple existental quantifier (2, 1) *)
-
-notation > "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1)"
- non associative with precedence 20
- for @{ 'Ex (λ${ident x0}.$P0) (λ${ident x0}.$P1) }.
-
-notation < "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1)"
- non associative with precedence 20
- for @{ 'Ex (λ${ident x0}:$T0.$P0) (λ${ident x0}:$T0.$P1) }.
-
 (* multiple existental quantifier (2, 2) *)
 
 notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1)"
diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa_props.ma b/matita/matita/contribs/lambdadelta/ground_2/xoa_props.ma
index 71216d1c4..06bfbc739 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/xoa_props.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/xoa_props.ma
@@ -19,7 +19,3 @@ include "ground_2/xoa.ma".
 interpretation "logical false" 'false = False.
 
 interpretation "logical true" 'true = True.
-
-lemma ex2_1_comm: ∀A0. ∀P0,P1:A0→Prop. (∃∃x0. P0 x0 & P1 x0) → ∃∃x0. P1 x0 & P0 x0.
-#A0 #P0 #P1 * /2 width=3/
-qed.
diff --git a/matita/matita/contribs/lambdadelta/root b/matita/matita/contribs/lambdadelta/root
index c41bf7380..4fb517279 100644
--- a/matita/matita/contribs/lambdadelta/root
+++ b/matita/matita/contribs/lambdadelta/root
@@ -1 +1 @@
-baseuri=cic:/matita/lambda_delta/
+baseuri=cic:/matita/lambdadelta/
diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma
index e80380217..c707c3207 100644
--- a/matita/matita/lib/arithmetics/nat.ma
+++ b/matita/matita/lib/arithmetics/nat.ma
@@ -439,6 +439,10 @@ theorem decidable_lt: ∀n,m. decidable (n < m).
 theorem le_to_or_lt_eq: ∀n,m:nat. n ≤ m → n < m ∨ n = m.
 #n #m #lenm (elim lenm) /3/ qed.
 
+theorem eq_or_gt: ∀n. 0 = n ∨ 0 < n.
+#n elim (le_to_or_lt_eq 0 n ?) // /2 width=1/
+qed-.
+
 theorem increasing_to_le2: ∀f:nat → nat. increasing f → 
   ∀m:nat. f 0 ≤ m → ∃i. f i ≤ m ∧ m < f (S i).
 #f #incr #m #lem (elim lem)
diff --git a/matita/matita/lib/basics/star.ma b/matita/matita/lib/basics/star.ma
index 5ac7d91fb..36aee8fe4 100644
--- a/matita/matita/lib/basics/star.ma
+++ b/matita/matita/lib/basics/star.ma
@@ -273,7 +273,7 @@ lemma bi_TC_strap: ∀A,B. ∀R:bi_relation A B. ∀a1,a,a2,b1,b,b2.
                    R a1 b1 a b → bi_TC … R a b a2 b2 → bi_TC … R a1 b1 a2 b2.
 #A #B #R #a1 #a #a2 #b1 #b #b2 #HR #H elim H -a2 -b2 /2 width=4/ /3 width=4/
 qed.
-
+                       
 lemma bi_TC_reflexive: ∀A,B,R. bi_reflexive A B R →
                        bi_reflexive A B (bi_TC … R).
 /2 width=1/ qed.
-- 
2.39.2