From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 6 Dec 2011 17:51:52 +0000 (+0000)
Subject: - support for atomic arities and candidates of reducibility started
X-Git-Tag: make_still_working~2048
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=9aa9a54946719d3fdb4cadb7c7d33fd13956c083;p=helm.git

- support for atomic arities and candidates of reducibility started
- integrations to standard library reduced
- some refactoring
---

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_cr.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_cr.ma
new file mode 100644
index 000000000..449dd7b69
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_cr.ma
@@ -0,0 +1,29 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/grammar/aarity.ma".
+include "Basic_2/grammar/lenv.ma".
+
+(* ABSTRACT CANDIDATES OF REDUCIBILITY **************************************)
+
+(* the abstract candidate of reducibility associated to an atomic arity *)
+let rec acr (R:lenv→predicate term) (A:aarity) (L:lenv) on A: predicate term ≝
+λT. match A with
+[ AAtom     ⇒ R L T
+| APair B A ⇒ ∀V. acr R B L V → acr R A L (𝕔{Appl} V. T)
+].
+
+interpretation
+   "candidate of reducibility (abstract)"
+   'InEInt R L T A = (acr R A L T).
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_weight.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_weight.ma
index c5e93ce16..22818a980 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_weight.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_weight.ma
@@ -38,7 +38,7 @@ qed.
 lemma tw_shift: ∀L,T. #[L, T] ≤ #[L @ T].
 #L elim L //
 #K #I #V #IHL #T
-@transitive_le [3: @IHL |2: /2 width=1/ | skip ]
+@transitive_le [3: @IHL |2: /2 width=2/ | skip ]
 qed.
 
 (* Basic_1: removed theorems 6:
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/sh.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/sh.ma
deleted file mode 100644
index 1708b7970..000000000
--- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/sh.ma
+++ /dev/null
@@ -1,23 +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 "Ground_2/list.ma".
-
-(* SORT HIERARCHY ***********************************************************)
-
-(* sort hierarchy specifications *)
-record sh: Type[0] ≝ {
-   next: nat → nat;        (* next sort in the hierarchy *)
-   next_lt: ∀k. k < next k (* strict monotonicity condition *)
-}.
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma
index f3f307cd6..42e7b8633 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma
@@ -43,7 +43,7 @@ lemma discr_tpair_xy_x: ∀I,T,V. 𝕔{I} V. T = V → False.
 [ #J #H destruct
 | #J #W #U #IHW #_ #H destruct
   -H >e0 in e1; normalize (**) (* destruct: one quality is not simplified, the destucted equality is not erased *)
-  /2 width=1/ 
+  /2 width=1/
 ]
 qed-.
 
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma
index dcbbbffed..0ec1b1466 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma
@@ -32,10 +32,18 @@ notation "hvbox( § term 90 p )"
  non associative with precedence 90
  for @{ 'GRef $p }.
 
+notation "hvbox( 𝕒 )"
+ non associative with precedence 90
+ for @{ 'SItem }.
+
 notation "hvbox( 𝕒 { I } )"
  non associative with precedence 90
  for @{ 'SItem $I }.
 
+notation "hvbox( 𝕔 term 90 T1 . break term 90 T )"
+ non associative with precedence 90
+ for @{ 'SItem $T1 $T }.
+
 notation "hvbox( 𝕔 { I } break term 90 T1 . break term 90 T )"
  non associative with precedence 90
  for @{ 'SItem $I $T1 $T }.
@@ -108,6 +116,12 @@ notation "hvbox( L ⊢ break term 90 T1 break [ d , break e ] ≡ break T2 )"
    non associative with precedence 45
    for @{ 'TSubst $L $T1 $d $e $T2 }.
 
+(* Static Typing ************************************************************)
+
+notation "hvbox( L ⊢ break term 90 T ÷ break A )"
+   non associative with precedence 45
+   for @{ 'AtomicArity $L $T $A }.
+
 (* Reducibility *************************************************************)
 
 notation "hvbox( ℝ [ T ] )"
@@ -191,3 +205,19 @@ notation "hvbox( ⇓ T  )"
 notation "hvbox( L ⊢ ⇓ T )"
    non associative with precedence 45
    for @{ 'SN $L $T }.
+
+notation "hvbox( { L, break T } ϵ break 〚 A 〛 )"
+   non associative with precedence 45
+   for @{ 'InEInt $L $T $A }.
+
+notation "hvbox( R ⊢ break { L, break T } ϵ break 〚 A 〛 )"
+   non associative with precedence 45
+   for @{ 'InEInt $R $L $T $A }.
+
+notation "hvbox( T1 ⊑ break T2 )"
+   non associative with precedence 45
+   for @{ 'CrSubEq $T1 $T2 }.
+
+notation "hvbox( T1 break [ R ] ⊑ break T2 )"
+   non associative with precedence 45
+   for @{ 'CrSubEq $T1 $R $T2 }.
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/apr_cr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/apr_cr.ma
deleted file mode 100644
index b46de8470..000000000
--- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/apr_cr.ma
+++ /dev/null
@@ -1,43 +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/grammar/term_simple.ma".
-
-(* CANDIDATES OF REDUCIBILITY ***********************************************)
-
-(* abstract conditions for candidates *)
-
-definition CR1: predicate term → predicate term → Prop ≝
-                λRD,RC. ∀T. RC T → RD T.
-
-definition CR2: relation term → predicate term → Prop ≝
-                λRR,RC. ∀T1,T2. RC T1 → 𝕊[T1] → RR T1 T2 → RC T2.
-
-definition CR3: relation term → predicate term → Prop ≝
-                λRR,RC. ∀T1. (∀T2. RR T1 T2 → RC T2) → 𝕊[T1] → RC T1.
-
-(* a candidate *)
-record cr (RR:relation term) (RD:predicate term): Type[0] ≝ {
-   in_cr: predicate term;
-   cr1: CR1 RD in_cr;
-   cr2: CR2 RR in_cr;
-   cr3: CR3 RR in_cr
-}.
-
-interpretation
-   "context-free parallel reduction (term)"
-   'InSubset T R = (in_cr ? ? R T).
-
-definition in_fun_cr: ∀RR,RD. ∀D,C:(cr RR RD). predicate term ≝
-                      λRR,RD,D,C,T. ∀V. V ϵ D → 𝕔{Appl}V.T ϵ C.
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_lift.ma
index 0775cefd2..f33692b42 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_lift.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_lift.ma
@@ -58,7 +58,7 @@ lemma cpr_lift: ∀L,K,d,e. ↓[d, e] L ≡ K →
 elim (lift_total T d e) #U #HTU 
 lapply (tpr_lift … HT1 … HTU1 … HTU) -T1 #HU1
 elim (lt_or_ge (|K|) d) #HKd
-[ lapply (tpss_lift_le … HT2 … HLK HTU … HTU2) -T2 -T -HLK [ /2 width=1/ | /3 width=4/ ]
+[ lapply (tpss_lift_le … HT2 … HLK HTU … HTU2) -T2 -T -HLK [ /2 width=2/ | /3 width=4/ ]
 | lapply (tpss_lift_be … HT2 … HLK HTU … HTU2) -T2 -T -HLK // /3 width=4/
 ]
 qed.
@@ -70,9 +70,9 @@ lemma cpr_inv_lift: ∀L,K,d,e. ↓[d, e] L ≡ K →
 #L #K #d #e #HLK #T1 #U1 #HTU1 #U2 * #U #HU1 #HU2
 elim (tpr_inv_lift … HU1 … HTU1) -U1 #T #HTU #T1
 elim (lt_or_ge (|L|) d) #HLd
-[ elim (tpss_inv_lift1_le … HU2 … HLK … HTU ?) -U -HLK [ /5 width=4/ | /2 width=1/ ]
+[ elim (tpss_inv_lift1_le … HU2 … HLK … HTU ?) -U -HLK [ /5 width=4/ | /2 width=2/ ]
 | elim (lt_or_ge (|L|) (d + e)) #HLde
-  [ elim (tpss_inv_lift1_be_up … HU2 … HLK … HTU ? ?) -U -HLK // [ /5 width=4/ | /2 width=1/ ] 
+  [ elim (tpss_inv_lift1_be_up … HU2 … HLK … HTU ? ?) -U -HLK // [ /5 width=4/ | /2 width=2/ ] 
   | elim (tpss_inv_lift1_be … HU2 … HLK … HTU ? ?) -U -HLK // /5 width=4/
   ]
 ]
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpr.ma
index 332575c21..40feeff2f 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpr.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpr.ma
@@ -45,8 +45,8 @@ fact tpr_conf_flat_beta:
    ∃∃X. 𝕔{Appl} V1. T1 ⇒ X & 𝕔{Abbr} V2. T2 ⇒ X.
 #V0 #V1 #T1 #V2 #W0 #U0 #T2 #IH #HV01 #HV02 #HT02 #H
 elim (tpr_inv_abst1 … H) -H #W1 #U1 #HW01 #HU01 #H destruct
-elim (IH … HV01 … HV02) -HV01 -HV02 // #V #HV1 #HV2
-elim (IH … HT02 … HU01) -HT02 -HU01 -IH // /3 width=5/
+elim (IH … HV01 … HV02) -HV01 -HV02 /2 width=1/ #V #HV1 #HV2
+elim (IH … HT02 … HU01) -HT02 -HU01 -IH /2 width=1/ /3 width=5/
 qed.
 
 (* basic-1: was:
@@ -63,14 +63,14 @@ fact tpr_conf_flat_theta:
    W0 ⇒ W2 → U0 ⇒ U2 →  𝕔{Abbr} W0. U0 ⇒ T1 →
    ∃∃X. 𝕔{Appl} V1. T1 ⇒ X & 𝕔{Abbr} W2. 𝕔{Appl} V. U2 ⇒ X.
 #V0 #V1 #T1 #V2 #V #W0 #W2 #U0 #U2 #IH #HV01 #HV02 #HV2 #HW02 #HU02 #H
-elim (IH … HV01 … HV02) -HV01 -HV02 // #VV #HVV1 #HVV2
+elim (IH … HV01 … HV02) -HV01 -HV02 /2 width=1/ #VV #HVV1 #HVV2
 elim (lift_total VV 0 1) #VVV #HVV
 lapply (tpr_lift … HVV2 … HV2 … HVV) #HVVV
 elim (tpr_inv_abbr1 … H) -H *
 (* case 1: delta *)
 [ -HV2 -HVV2 #WW2 #UU2 #UU #HWW2 #HUU02 #HUU2 #H destruct
-  elim (IH … HW02 … HWW2) -HW02 -HWW2 // #W #HW02 #HWW2
-  elim (IH … HU02 … HUU02) -HU02 -HUU02 -IH // #U #HU2 #HUUU2
+  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
   [2: @tpr_theta [6: @HVV |7: @HWW2 |8: @HUUU2 |1,2,3,4: skip | // ]
@@ -81,7 +81,7 @@ elim (tpr_inv_abbr1 … H) -H *
 | -HW02 -HVV -HVVV #UU1 #HUU10 #HUUT1
   elim (tpr_inv_lift … HU02 … HUU10) -HU02 #UU #HUU2 #HUU1
   lapply (tw_lift … HUU10) -HUU10 #HUU10
-  elim (IH … HUUT1 … HUU1) -HUUT1 -HUU1 -IH // -HUU10 #U #HU2 #HUUU2
+  elim (IH … HUUT1 … HUU1) -HUUT1 -HUU1 -IH /2 width=1/ -HUU10 #U #HU2 #HUUU2
   @ex2_1_intro
   [2: @tpr_flat
   |1: skip 
@@ -111,8 +111,8 @@ fact tpr_conf_beta_beta:
    V0 ⇒ V1 → V0 ⇒ V2 → T0 ⇒ T1 → T0 ⇒ T2 →
    ∃∃X. 𝕔{Abbr} V1. T1 ⇒X & 𝕔{Abbr} V2. T2 ⇒ X.
 #W0 #V0 #V1 #T0 #T1 #V2 #T2 #IH #HV01 #HV02 #HT01 #HT02
-elim (IH … HV01 … HV02) -HV01 -HV02 //
-elim (IH … HT01 … HT02) -HT01 -HT02 -IH // /3 width=5/
+elim (IH … HV01 … HV02) -HV01 -HV02 /2 width=1/
+elim (IH … HT01 … HT02) -HT01 -HT02 -IH /2 width=1/ /3 width=5/
 qed.
 
 (* Basic_1: was: pr0_cong_delta pr0_delta_delta *)
@@ -162,9 +162,9 @@ fact tpr_conf_theta_theta:
    ↑[O, 1] V1 ≡ VV1 → ↑[O, 1] V2 ≡ VV2 →
    ∃∃X. 𝕔{Abbr} W1. 𝕔{Appl} VV1. T1 ⇒ X & 𝕔{Abbr} W2. 𝕔{Appl} VV2. T2 ⇒ X.
 #VV1 #V0 #V1 #W0 #W1 #T0 #T1 #V2 #VV2 #W2 #T2 #IH #HV01 #HV02 #HW01 #HW02 #HT01 #HT02 #HVV1 #HVV2
-elim (IH … HV01 … HV02) -HV01 -HV02 // #V #HV1 #HV2
-elim (IH … HW01 … HW02) -HW01 -HW02 // #W #HW1 #HW2
-elim (IH … HT01 … HT02) -HT01 -HT02 -IH // #T #HT1 #HT2
+elim (IH … HV01 … HV02) -HV01 -HV02 /2 width=1/ #V #HV1 #HV2
+elim (IH … HW01 … HW02) -HW01 -HW02 /2 width=1/ #W #HW1 #HW2
+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
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/static/sh.ma b/matita/matita/contribs/lambda_delta/Basic_2/static/sh.ma
new file mode 100644
index 000000000..1708b7970
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/Basic_2/static/sh.ma
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "Ground_2/list.ma".
+
+(* SORT HIERARCHY ***********************************************************)
+
+(* sort hierarchy specifications *)
+record sh: Type[0] ≝ {
+   next: nat → nat;        (* next sort in the hierarchy *)
+   next_lt: ∀k. k < next k (* strict monotonicity condition *)
+}.
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma
index db31dfaab..2b8f3f953 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma
@@ -152,17 +152,17 @@ lemma ldrop_lsubs_ldrop1_abbr: ∀L1,L2,d,e. L1 [d, e] ≼ L2 →
   [ -IHL12 -Hie destruct
     <minus_n_O <minus_plus_m_m // /2 width=3/
   | -HL12
-    elim (IHL12 … HLK1 ? ?) -IHL12 -HLK1 // /2 width=1/ -Hie >arith_g1 // /3 width=3/
+    elim (IHL12 … HLK1 ? ?) -IHL12 -HLK1 // /2 width=1/ -Hie >minus_minus_comm >arith_b1 // /4 width=3/
   ]
 | #L1 #L2 #I #V1 #V2 #e #_ #IHL12 #K1 #W #i #H #_ #Hie
   elim (ldrop_inv_O1 … H) -H * #Hi #HLK1
   [ -IHL12 -Hie -Hi destruct
-  | elim (IHL12 … HLK1 ? ?) -IHL12 -HLK1 // /2 width=1/ -Hie >arith_g1 // /3 width=3/
+  | elim (IHL12 … HLK1 ? ?) -IHL12 -HLK1 // /2 width=1/ -Hie >minus_minus_comm >arith_b1 // /3 width=3/
   ]
 | #L1 #L2 #I1 #I2 #V1 #V2 #d #e #_ #IHL12 #K1 #V #i #H #Hdi >plus_plus_comm_23 #Hide
-  lapply (plus_S_le_to_pos … Hdi) #Hi
+  elim (le_inv_plus_l … Hdi) #Hdim #Hi
   lapply (ldrop_inv_ldrop1 … H ?) -H // #HLK1
-  elim (IHL12 … HLK1 ? ?) -IHL12 -HLK1 /2 width=1/ -Hdi -Hide >arith_g1 // /3 width=3/
+  elim (IHL12 … HLK1 ? ?) -IHL12 -HLK1 // /2 width=1/ -Hdi -Hide >minus_minus_comm >arith_b1 // /3 width=3/
 ]
 qed.
 
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop_ldrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop_ldrop.ma
index f4b20bcb5..3aef19c0e 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop_ldrop.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop_ldrop.ma
@@ -46,7 +46,7 @@ theorem ldrop_conf_ge: ∀d1,e1,L,L1. ↓[d1, e1] L ≡ L1 →
 | //
 | #L #K #I #V #e #_ #IHLK #e2 #L2 #H #He2
   lapply (ldrop_inv_ldrop1 … H ?) -H /2 width=2/ #HL2
-  <minus_plus_comm /3 width=1/
+  <minus_plus >minus_minus_comm /3 width=1/
 | #L #K #I #V1 #V2 #d #e #_ #_ #IHLK #e2 #L2 #H #Hdee2
   lapply (transitive_le 1 … Hdee2) // #He2
   lapply (ldrop_inv_ldrop1 … H ?) -H // -He2 #HL2
@@ -85,9 +85,9 @@ theorem ldrop_trans_le: ∀d1,e1,L1,L. ↓[d1, e1] L1 ≡ L →
 [ #d #e #e2 #L2 #H
   >(ldrop_inv_atom1 … H) -L2 /2 width=3/
 | #K #I #V #e2 #L2 #HL2 #H
-  lapply (le_O_to_eq_O … H) -H #H destruct /2 width=3/
+  lapply (le_n_O_to_eq … H) -H #H destruct /2 width=3/
 | #L1 #L2 #I #V #e #_ #IHL12 #e2 #L #HL2 #H
-  lapply (le_O_to_eq_O … H) -H #H destruct
+  lapply (le_n_O_to_eq … H) -H #H destruct
   elim (IHL12 … HL2 ?) -IHL12 -HL2 // #L0 #H #HL0
   lapply (ldrop_inv_refl … H) -H #H destruct /3 width=5/
 | #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #IHL12 #e2 #L #H #He2d
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma
index f58c1906e..30296c685 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma
@@ -303,8 +303,8 @@ lemma lift_split: ∀d1,e2,T1,T2. ↑[d1, e2] T1 ≡ T2 →
 | #i #d1 #e2 #Hid1 #d2 #e1 #Hd12 #_ #_
   lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2 /4 width=3/
 | #i #d1 #e2 #Hid1 #d2 #e1 #_ #Hd21 #He12
-  lapply (transitive_le …(i+e1) Hd21 ?) /2 width=1/ -Hd21 #Hd21
-  <(arith_d1 i e2 e1) // /3 width=3/
+  lapply (transitive_le … (i+e1) Hd21 ?) /2 width=1/ -Hd21 #Hd21
+  >(plus_minus_m_m e2 e1 ?) // /3 width=3/
 | /3 width=3/
 | #I #V1 #V2 #T1 #T2 #d1 #e2 #_ #_ #IHV #IHT #d2 #e1 #Hd12 #Hd21 #He12
   elim (IHV … Hd12 Hd21 He12) -IHV #V0 #HV0a #HV0b
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift.ma
index 2f92251bd..3f5b8ab6a 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift.ma
@@ -50,11 +50,11 @@ theorem lift_div_le: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T →
 | #i #d1 #e1 #Hid1 #d2 #e2 #T2 #Hi #Hd12
   elim (lift_inv_lref2 … Hi) -Hi * #Hid2 #H destruct
   [ -Hd12 lapply (lt_plus_to_lt_l … Hid2) -Hid2 #Hid2 /3 width=3/
-  | -Hid1 lapply (arith1 … Hid2) -Hid2 #Hid2
-    @(ex2_1_intro … #(i - e2))
-    [ >le_plus_minus_comm [ @lift_lref_ge @(transitive_le … Hd12) -Hd12 /2 width=1/ | -Hd12 /2 width=2/ ]
-    | -Hd12 >(plus_minus_m_m i e2) in ⊢ (? ? ? ? %); /2 width=2/ /3 width=1/
-    ]
+  | -Hid1 >plus_plus_comm_23 in Hid2; #H lapply (le_inv_plus_plus_r … H) -H #H
+    elim (le_inv_plus_l … H) -H #Hide2 #He2i
+    lapply (transitive_le … Hd12 Hide2) -Hd12 #Hd12
+    >le_plus_minus_comm // >(plus_minus_m_m i e2) in ⊢ (? ? ? %); // -He2i
+    /4 width=3/
   ]
 | #p #d1 #e1 #d2 #e2 #T2 #Hk #Hd12
   lapply (lift_inv_gref2 … Hk) -Hk #Hk destruct /3 width=3/
@@ -154,8 +154,7 @@ theorem lift_trans_ge: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T →
   lapply (lt_to_le_to_lt … Hid1e Hded) -Hid1e -Hded #Hid2
   lapply (lift_inv_lref1_lt … HX ?) -HX // #HX destruct /3 width=3/
 | #i #d1 #e1 #Hid1 #d2 #e2 #X #HX #_
-  elim (lift_inv_lref1 … HX) -HX * #Hied #HX destruct
-  [ /4 width=3/ | >plus_plus_comm_23 /4 width=3/ ]
+  elim (lift_inv_lref1 … HX) -HX * #Hied #HX destruct /4 width=3/
 | #p #d1 #e1 #d2 #e2 #X #HX #_
   >(lift_inv_gref1 … HX) -HX /2 width=3/
 | #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hded
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps_ldrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps_ldrop.ma
index 7996f53a6..f777d1cd7 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps_ldrop.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps_ldrop.ma
@@ -23,11 +23,11 @@ lemma ltps_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 →
 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H //
 | //
 | normalize #K0 #K1 #I #V0 #V1 #e1 #_ #_ #IHK01 #L2 #e2 #H #He12
-  lapply (plus_le_weak … He12) #He2
+  elim (le_inv_plus_l … He12) #_ #He2
   lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
   lapply (IHK01 … HK0L2 ?) -K0 /2 width=1/
 | #K0 #K1 #I #V0 #V1 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK01 #L2 #e2 #H #Hd1e2
-  lapply (plus_le_weak … Hd1e2) #He2
+  elim (le_inv_plus_l … Hd1e2) #_ #He2
   lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
   lapply (IHK01 … HK0L2 ?) -K0 /2 width=1/
 ]
@@ -40,11 +40,11 @@ lemma ltps_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ≫ L0 →
 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H //
 | //
 | normalize #K1 #K0 #I #V1 #V0 #e1 #_ #_ #IHK10 #L2 #e2 #H #He12
-  lapply (plus_le_weak … He12) #He2
+  elim (le_inv_plus_l … He12) #_ #He2
   lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
   lapply (IHK10 … HK0L2 ?) -K0 /2 width=1/
 | #K0 #K1 #I #V1 #V0 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK10 #L2 #e2 #H #Hd1e2
-  lapply (plus_le_weak … Hd1e2) #He2
+  elim (le_inv_plus_l … Hd1e2) #_ #He2
   lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
   lapply (IHK10 … HK0L2 ?) -IHK10 -HK0L2 /2 width=1/
 ]
@@ -65,7 +65,7 @@ lemma ltps_ldrop_conf_be: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 →
     elim (IHK01 … HK0L2 ? ?) -K0 // /2 width=1/ /3 width=3/
   ]
 | #K0 #K1 #I #V0 #V1 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK01 #L2 #e2 #H #Hd1e2 #He2de1
-  lapply (plus_le_weak … Hd1e2) #He2
+  elim (le_inv_plus_l … Hd1e2) #_ #He2
   <minus_le_minus_minus_comm //
   lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
   elim (IHK01 … HK0L2 ? ?) -K0 /2 width=1/ /3 width=3/
@@ -87,7 +87,7 @@ lemma ltps_ldrop_trans_be: ∀L1,L0,d1,e1. L1 [d1, e1] ≫ L0 →
     elim (IHK10 … HK0L2 ? ?) -K0 // /2 width=1/ /3 width=3/
   ]
 | #K1 #K0 #I #V1 #V0 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK10 #L2 #e2 #H #Hd1e2 #He2de1
-  lapply (plus_le_weak … Hd1e2) #He2
+  elim (le_inv_plus_l … Hd1e2) #_ #He2
   <minus_le_minus_minus_comm //
   lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
   elim (IHK10 … HK0L2 ? ?) -K0 /2 width=1/ /3 width=3/
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps_tps.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps_tps.ma
index c021f5d50..8bf9f197d 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps_tps.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps_tps.ma
@@ -26,7 +26,7 @@ lemma ltps_tps_conf_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫ U2 →
   lapply (transitive_le … Hde1d2 Hdi2) -Hde1d2 #Hde1i2
   lapply (ltps_ldrop_conf_ge … HL01 … HLK0 ?) -L0 // /2 width=4/
 | #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01 #Hde1d2
-  @tps_bind [ /2 width=4/ | @IHTU2 /2 width=4/ ] (**) (* explicit constructor *)
+  @tps_bind [ /2 width=4/ | @IHTU2 -IHTU2 -IHVW2 [3: /2 by ltps_tps1/ |1,2: skip | /2 width=1/ ] ] (**) (* explicit constructor *)
 | /3 width=4/
 ]
 qed.
@@ -40,18 +40,18 @@ lemma ltps_tps_conf: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫ U2 →
 [ /2 width=3/
 | #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL01
   elim (lt_or_ge i2 d1) #Hi2d1
-  [ elim (ltps_ldrop_conf_le … HL01 … HLK0 ?) -L0 /2 width=1/ #X #H #HLK1
+  [ elim (ltps_ldrop_conf_le … HL01 … HLK0 ?) -L0 /2 width=2/ #X #H #HLK1
     elim (ltps_inv_tps11 … H ?) -H /2 width=1/ #K1 #V1 #_ #HV01 #H destruct
     lapply (ldrop_fwd_ldrop2 … HLK1) #H
     elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1
-    lapply (tps_lift_ge … HV01 … H HVW0 HVW1 ?) -V0 -H // >arith_a2 // /3 width=4/
+    lapply (tps_lift_ge … HV01 … H HVW0 HVW1 ?) -V0 -H // >minus_plus <plus_minus_m_m // /3 width=4/
   | elim (lt_or_ge i2 (d1 + e1)) #Hde1i2
-    [ elim (ltps_ldrop_conf_be … HL01 … HLK0 ? ?) -L0 /2 width=1/ #X #H #HLK1
+    [ elim (ltps_ldrop_conf_be … HL01 … HLK0 ? ?) -L0 // /2 width=2/ #X #H #HLK1
       elim (ltps_inv_tps21 … H ?) -H /2 width=1/ #K1 #V1 #_ #HV01 #H destruct
       lapply (ldrop_fwd_ldrop2 … HLK1) #H
       elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1
       lapply (tps_lift_ge … HV01 … H HVW0 HVW1 ?) -V0 -H // normalize #HW01
-      lapply (tps_weak … HW01 d1 e1 ? ?) [2: /2 width=1/ |3: /3 width=4/ ] >arith_i2 //
+      lapply (tps_weak … HW01 d1 e1 ? ?) [2: /2 width=1/ |3: /3 width=4/ ] >minus_plus >commutative_plus /2 width=1/
     | lapply (ltps_ldrop_conf_ge … HL01 … HLK0 ?) -L0 // /3 width=4/
     ]
   ]
@@ -73,7 +73,7 @@ lemma ltps_tps_trans_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫ U2 →
   lapply (transitive_le … Hde1d2 Hdi2) -Hde1d2 #Hde1i2
   lapply (ltps_ldrop_trans_ge … HL10 … HLK0 ?) -L0 // /2 width=4/
 | #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10 #Hde1d2
-  @tps_bind [ /2 width=4/ | @IHTU2 /2 width=4/ ] (**) (* explicit constructor *)
+  @tps_bind [ /2 width=4/ | @IHTU2 -IHTU2 -IHVW2 [3: /2 by ltps_tps1/ |1,2: skip | /2 width=1/ ] ] (**) (* explicit constructor *)
 | /3 width=4/
 ]
 qed.
@@ -87,18 +87,18 @@ lemma ltps_tps_trans: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫ U2 →
 [ /2 width=3/
 | #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL10
   elim (lt_or_ge i2 d1) #Hi2d1
-  [ elim (ltps_ldrop_trans_le … HL10 … HLK0 ?) -HL10 /2 width=1/ #X #H #HLK1
+  [ elim (ltps_ldrop_trans_le … HL10 … HLK0 ?) -HL10 /2 width=2/ #X #H #HLK1
     elim (ltps_inv_tps12 … H ?) -H /2 width=1/ #K1 #V1 #_ #HV01 #H destruct
     lapply (ldrop_fwd_ldrop2 … HLK0) -HLK0 #H
     elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1
-    lapply (tps_lift_ge … HV01 … H HVW1 HVW0 ?) -V0 -H // >arith_a2 // /3 width=4/
+    lapply (tps_lift_ge … HV01 … H HVW1 HVW0 ?) -V0 -H // >minus_plus <plus_minus_m_m /2 width=1/ /3 width=4/
   | elim (lt_or_ge i2 (d1 + e1)) #Hde1i2
-    [ elim (ltps_ldrop_trans_be … HL10 … HLK0 ? ?) -HL10 // /2 width=1/ #X #H #HLK1
+    [ elim (ltps_ldrop_trans_be … HL10 … HLK0 ? ?) -HL10 // /2 width=2/ #X #H #HLK1
       elim (ltps_inv_tps22 … H ?) -H /2 width=1/ #K1 #V1 #_ #HV01 #H destruct
       lapply (ldrop_fwd_ldrop2 … HLK0) -HLK0 #H
       elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1
       lapply (tps_lift_ge … HV01 … H HVW1 HVW0 ?) -V0 -H // normalize #HW01
-      lapply (tps_weak … HW01 d1 e1 ? ?) [2: /3 width=1/ |3: /3 width=4/ ] >arith_i2 //
+      lapply (tps_weak … HW01 d1 e1 ? ?) [2: /3 width=1/ |3: /3 width=4/ ] >minus_plus >commutative_plus /2 width=1/
     | lapply (ltps_ldrop_trans_ge … HL10 … HLK0 ?) -HL10 -HLK0 // /3 width=4/
     ]
   ]
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps.ma
index 762e2a9a0..969e67485 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps.ma
@@ -58,7 +58,7 @@ lemma tps_full: ∀K,V,T1,L,d. ↓[0, d] L ≡ (K. 𝕓{Abbr} V) →
   elim (lt_or_eq_or_gt i d) #Hid /3 width=4/
   destruct
   elim (lift_total V 0 (i+1)) #W #HVW
-  elim (lift_split … HVW i i ? ? ?) // <minus_plus_m_m_comm /3 width=4/
+  elim (lift_split … HVW i i ? ? ?) // /3 width=4/
 | * #I #W1 #U1 #IHW1 #IHU1 #L #d #HLK
   elim (IHW1 … HLK) -IHW1 #W2 #W #HW12 #HW2
   [ elim (IHU1 (L. 𝕓{I} W2) (d+1) ?) -IHU1 /2 width=1/ -HLK /3 width=8/
@@ -86,8 +86,7 @@ lemma tps_weak_top: ∀L,T1,T2,d,e.
 [ //
 | #L #K #V #W #i #d #e #Hdi #_ #HLK #HVW
   lapply (ldrop_fwd_ldrop2_length … HLK) #Hi
-  lapply (le_to_lt_to_lt … Hdi Hi) #Hd
-  lapply (plus_minus_m_m_comm (|L|) d ?) /2 width=1/ /2 width=4/ 
+  lapply (le_to_lt_to_lt … Hdi Hi) /3 width=4/
 | normalize /2 width=1/
 | /2 width=1/
 ]
@@ -107,15 +106,15 @@ lemma tps_split_up: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → ∀i. d ≤ i →
 | #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_comm j d) in ⊢ (% → ?); // -Hdj /3 width=4/
+    >(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_comm … Hjde) in ⊢ (% → ?); -Hjde /4 width=4/
+    >(plus_minus_m_m … Hjde) in ⊢ (% → ?); -Hjde /4 width=4/
   ]
 | #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #i #Hdi #Hide
   elim (IHV12 i ? ?) -IHV12 // #V #HV1 #HV2
   elim (IHT12 (i + 1) ? ?) -IHT12 /2 width=1/
-  -Hdi -Hide >arith_c1 >arith_c1x #T #HT1 #HT2
+  -Hdi -Hide >arith_c1x #T #HT1 #HT2
   lapply (tps_lsubs_conf … HT1 (L. 𝕓{I} V) ?) -HT1 /3 width=5/
 | #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #i #Hdi #Hide
   elim (IHV12 i ? ?) -IHV12 // elim (IHT12 i ? ?) -IHT12 //
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps_lift.ma
index ff42a7ac4..6e3565e73 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps_lift.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps_lift.ma
@@ -52,7 +52,7 @@ lemma tps_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫ T2 →
   lapply (lt_to_le_to_lt … Hidet … Hdetd) -Hdetd #Hid
   lapply (lift_inv_lref1_lt … H … Hid) -H #H destruct
   elim (lift_trans_ge … HVW … HWU2 ?) -W // <minus_plus #W #HVW #HWU2
-  elim (ldrop_trans_le … HLK … HKV ?) -K /2 width=1/ #X #HLK #H
+  elim (ldrop_trans_le … HLK … HKV ?) -K /2 width=2/ #X #HLK #H
   elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K #Y #_ #HVY
   >(lift_mono … HVY … HVW) -Y -HVW #H destruct /2 width=4/
 | #K #I #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #d #e #HLK #H1 #H2 #Hdetd
@@ -78,7 +78,7 @@ lemma tps_lift_be: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫ T2 →
   [ -Hdtd
     lapply (lt_to_le_to_lt … (dt+et+e) Hidet ?) // -Hidet #Hidete
     elim (lift_trans_ge … HVW … HWU2 ?) -W // <minus_plus #W #HVW #HWU2
-    elim (ldrop_trans_le … HLK … HKV ?) -K /2 width=1/ #X #HLK #H
+    elim (ldrop_trans_le … HLK … HKV ?) -K /2 width=2/ #X #HLK #H
     elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K #Y #_ #HVY
     >(lift_mono … HVY … HVW) -V #H destruct /2 width=4/
   | -Hdti
@@ -90,7 +90,7 @@ lemma tps_lift_be: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫ T2 →
   elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1
   elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct
   @tps_bind [ /2 width=6/ | @IHT12 [3,4: // | skip |5,6: /2 width=1/ | /2 width=1/ ] 
-            ] (**) (* /3 width=6/ is too slow, arith3 needed to avoid crash, simplification like tps_lift_le is too slow *)
+            ] (**) (* /3 width=6/ is too slow, simplification like tps_lift_le is too slow *)
 | #K #I #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #d #e #HLK #H1 #H2 #Hdetd
   elim (lift_inv_flat1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1
   elim (lift_inv_flat1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /3 width=6/
@@ -136,7 +136,7 @@ lemma tps_inv_lift1_le: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 →
   lapply (lt_to_le_to_lt … Hidet … Hdetd) -Hdetd #Hid
   lapply (lift_inv_lref2_lt … H … Hid) -H #H destruct
   elim (ldrop_conf_lt … HLK … HLKV ?) -L // #L #U #HKL #_ #HUV
-  elim (lift_trans_le … HUV … HVW ?) -V // >arith_a2 // -Hid /3 width=4/
+  elim (lift_trans_le … HUV … HVW ?) -V // >minus_plus <plus_minus_m_m // -Hid /3 width=4/
 | #L #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 (IHV12 … HLK … HWV1 ?) -V1 // #W2 #HW12 #HWV2
@@ -165,17 +165,18 @@ lemma tps_inv_lift1_be: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 →
   [ -Hdtd -Hidet
     lapply (lt_to_le_to_lt … (dt + (et - e)) Hid ?) [ <le_plus_minus /2 width=1/ ] -Hdedet #Hidete
     elim (ldrop_conf_lt … HLK … HLKV ?) -L // #L #U #HKL #_ #HUV
-    elim (lift_trans_le … HUV … HVW ?) -V // >arith_a2 // -Hid /3 width=4/
+    elim (lift_trans_le … HUV … HVW ?) -V // >minus_plus <plus_minus_m_m // -Hid /3 width=4/
   | -Hdti -Hdedet
     lapply (transitive_le … (i - e) Hdtd ?) /2 width=1/ -Hdtd #Hdtie
-    lapply (plus_le_weak … Hid) #Hei
+    elim (le_inv_plus_l … Hid) #_ #Hei
     lapply (ldrop_conf_ge … HLK … HLKV ?) -L // #HKV
-    elim (lift_split … HVW d (i - e + 1) ? ? ?) -HVW [4: // |2,3: /2 width=1/ ] -Hid >arith_e2 // /4 width=4/
+    elim (lift_split … HVW d (i - e + 1) ? ? ?) -HVW [4: // |3: /2 width=1/ |2: /3 width=1/ ] -Hid
+    #V1 #HV1 >plus_minus // <minus_minus // /2 width=1/ /4 width=4/
   ]
 | #L #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
   elim (IHV12 … HLK … HWV1 ? ?) -V1 // #W2 #HW12 #HWV2
-  elim (IHU12 … HTU1 ? ?) -U1 [5: @ldrop_skip // |2: skip |3: >plus_plus_comm_23 >(plus_plus_comm_23 dt) /2 width=1/ |4: /2 width=1/ ]
+  elim (IHU12 … HTU1 ? ?) -U1 [5: @ldrop_skip // |2: skip |3: >plus_plus_comm_23 >(plus_plus_comm_23 dt) /2 width=1/ |4: /2 width=1/ ] (**) (* 29s without the rewrites *)
   /3 width=5/
 | #L #I #V1 #V2 #U1 #U2 #dt #et #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H #Hdtd #Hdedet
   elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
@@ -197,15 +198,16 @@ lemma tps_inv_lift1_ge: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 →
   ]
 | #L #KV #V #W #i #dt #et #Hdti #Hidet #HLKV #HVW #K #d #e #HLK #T1 #H #Hdedt
   lapply (transitive_le … Hdedt … Hdti) #Hdei
-  lapply (plus_le_weak … Hdedt) -Hdedt #Hedt
-  lapply (plus_le_weak … Hdei) #Hei  
+  elim (le_inv_plus_l … Hdedt) -Hdedt #_ #Hedt
+  elim (le_inv_plus_l … Hdei) #_ #Hei
   lapply (lift_inv_lref2_ge … H … Hdei) -H #H destruct
   lapply (ldrop_conf_ge … HLK … HLKV ?) -L // #HKV
-  elim (lift_split … HVW d (i - e + 1) ? ? ?) -HVW [4: // |2,3: normalize /2 width=1/ ] -Hdei >arith_e2 // #V0 #HV10 #HV02
+  elim (lift_split … HVW d (i - e + 1) ? ? ?) -HVW [4: // |3: /2 width=1/ |2: /3 width=1/ ] -Hdei 
+  #V0 #HV10 >plus_minus // <minus_minus // /2 width=1/ #HV02
   @ex2_1_intro /3 width=4/ (**) (* explicitc constructors *)
 | #L #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
-  lapply (plus_le_weak … Hdetd) #Hedt
+  elim (le_inv_plus_l … Hdetd) #_ #Hedt
   elim (IHV12 … HLK … HWV1 ?) -V1 // #W2 #HW12 #HWV2
   elim (IHU12 … HTU1 ?) -U1 [4: @ldrop_skip // |2: skip |3: /2 width=1/ ]
   <plus_minus // /3 width=5/
@@ -256,7 +258,7 @@ lemma tps_inv_lift1_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 →
                         ∃∃T2. K ⊢ T1 [d, dt + et - (d + e)] ≫ T2 & ↑[d, e] T2 ≡ U2.
 #L #U1 #U2 #dt #et #HU12 #K #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet
 elim (tps_split_up … HU12 (d + e) ? ?) -HU12 // -Hdedet #U #HU1 #HU2
-lapply (tps_weak … HU1 d e ? ?) -HU1 // <plus_minus_m_m_comm // -Hddt -Hdtde #HU1
+lapply (tps_weak … HU1 d e ? ?) -HU1 // [ >commutative_plus /2 width=1/ ] -Hddt -Hdtde #HU1
 lapply (tps_inv_lift1_eq … HU1 … HTU1) -HU1 #HU1 destruct
 elim (tps_inv_lift1_ge … HU2 … HLK … HTU1 ?) -U -L // <minus_plus_m_m /2 width=3/
 qed.
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_lift.ma
index 53c4f0c68..f2c39379f 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_lift.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_lift.ma
@@ -30,7 +30,7 @@ lemma tpss_subst: ∀L,K,V,U1,i,d,e.
   lapply (IHU … HU0) -IHU #H
   lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
   lapply (tps_lift_ge … HU1 … HLK HU0 HU12 ?) -HU1 -HLK -HU0 -HU12 // normalize #HU02
-  lapply (tps_weak … HU02 d e ? ?) -HU02 [ >arith_i2 // | /2 width=1/ | /2 width=3/ ]
+  lapply (tps_weak … HU02 d e ? ?) -HU02 [ >minus_plus >commutative_plus /2 width=1/ | /2 width=1/ | /2 width=3/ ]
 ]
 qed.
 
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_ltps.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_ltps.ma
index 18b181741..f07ee8ee3 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_ltps.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_ltps.ma
@@ -67,7 +67,7 @@ fact ltps_tps_trans_eq_aux: ∀Y1,X2,L1,T2,U2,d,e.
 [ //
 | #L1 #K1 #V1 #W1 #i #d #e #Hdi #Hide #HLK1 #HVW1 #L0 #HL10 #H1 #H2 destruct
   lapply (ldrop_fwd_lw … HLK1) normalize #H1
-  elim (ltps_ldrop_trans_be … HL10 … HLK1 ? ?) -HL10 -HLK1 /2 width=1/ #X #H #HLK0
+  elim (ltps_ldrop_trans_be … HL10 … HLK1 ? ?) -HL10 -HLK1 // /2 width=2/ #X #H #HLK0
   elim (ltps_inv_tps22 … H ?) -H /2 width=1/ #K0 #V0 #HK01 #HV01 #H destruct
   lapply (tps_fwd_tw … HV01) #H2
   lapply (transitive_le (#[K1] + #[V0]) … H1) -H1 /2 width=1/ -H2 #H
@@ -75,11 +75,11 @@ fact ltps_tps_trans_eq_aux: ∀Y1,X2,L1,T2,U2,d,e.
   [1,3: // |2,4: skip | normalize /2 width=1/ | /3 width=6/ ]
 | #L #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #L0 #HL0 #H1 #H2 destruct
   lapply (tps_lsubs_conf … HT12 (L. 𝕓{I} V1) ?) -HT12 /2 width=1/ #HT12
-  lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3,5: normalize // |2,4: skip ] #HV12
+  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_conf … 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,5: normalize // |2,4: skip ]
+  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/
 ]
 qed.
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_tpss.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_tpss.ma
index fc340e1ad..cd7e666b2 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_tpss.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_tpss.ma
@@ -53,7 +53,7 @@ lemma tpss_split_up: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫* T2 →
 [ /2 width=3/
 | #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: <plus_minus_m_m_comm // ]
+  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 *)
 ]
 qed.
@@ -64,7 +64,7 @@ lemma tpss_inv_lift1_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫* U2 →
                          ∃∃T2. K ⊢ T1 [d, dt + et - (d + e)] ≫* T2 & ↑[d, e] T2 ≡ U2.
 #L #U1 #U2 #dt #et #HU12 #K #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet
 elim (tpss_split_up … HU12 (d + e) ? ?) -HU12 // -Hdedet #U #HU1 #HU2
-lapply (tpss_weak … HU1 d e ? ?) -HU1 // <plus_minus_m_m_comm // -Hddt -Hdtde #HU1
+lapply (tpss_weak … HU1 d e ? ?) -HU1 // [ >commutative_plus /2 width=1/ ] -Hddt -Hdtde #HU1
 lapply (tpss_inv_lift1_eq … HU1 … HTU1) -HU1 #HU1 destruct
 elim (tpss_inv_lift1_ge … HU2 … HLK … HTU1 ?) -HU2 -HLK -HTU1 // <minus_plus_m_m /2 width=3/
 qed.
diff --git a/matita/matita/contribs/lambda_delta/Ground_2/arith.ma b/matita/matita/contribs/lambda_delta/Ground_2/arith.ma
index a6ac73c12..5d14a43dd 100644
--- a/matita/matita/contribs/lambda_delta/Ground_2/arith.ma
+++ b/matita/matita/contribs/lambda_delta/Ground_2/arith.ma
@@ -17,43 +17,55 @@ include "Ground_2/star.ma".
 
 (* ARITHMETICAL PROPERTIES **************************************************)
 
-lemma false_lt_to_le: ∀x,y. (x < y → False) → y ≤ x.
-#x #y #H elim (decidable_lt x y) /2 width=1/
-#Hxy elim (H Hxy)
-qed-.
+(* equations ****************************************************************)
 
-axiom eq_nat_dec: ∀n1,n2:nat. Decidable (n1 = n2).
+lemma plus_plus_comm_23: ∀x,y,z. x + y + z = x + z + y.
+// qed.
 
-axiom lt_dec: ∀n1,n2. Decidable (n1 < n2).
+lemma le_plus_minus: ∀m,n,p. p ≤ n → m + n - p = m + (n - p).
+/2 by plus_minus/ qed.
 
-lemma plus_S_eq_O_false: ∀n,m. n + S m = 0 → False.
-#n #m <plus_n_Sm #H destruct
-qed-.
+lemma le_plus_minus_comm: ∀n,m,p. p ≤ m → m + n - p = m - p + n.
+/2 by plus_minus/ qed.
 
-lemma plus_S_le_to_pos: ∀n,m,p. n + S m ≤ p → 0 < p.
-#n #m #p <plus_n_Sm #H @(lt_to_le_to_lt … H) //
+lemma minus_le_minus_minus_comm: ∀b,c,a. c ≤ b → a - (b - c) = a + c - b.
+#b elim b -b
+[ #c #a #H >(le_n_O_to_eq … H) -H //
+| #b #IHb #c elim c -c //
+  #c #_ #a #Hcb
+  lapply (le_S_S_to_le … Hcb) -Hcb #Hcb
+  <plus_n_Sm normalize /2 width=1/
+]
 qed.
 
-lemma minus_le: ∀m,n. m - n ≤ m.
-/2 width=1/ qed.
+lemma minus_minus_comm: ∀a,b,c. a - b - c = a - c - b.
+/3 by monotonic_le_minus_l, le_to_le_to_eq/ qed.
 
-lemma le_O_to_eq_O: ∀n. n ≤ 0 → n = 0.
-/2 width=1/ qed.
+lemma arith_b1: ∀a,b,c1. c1 ≤ b → a - c1 - (b - c1) = a - b.
+#a #b #c1 #H >minus_plus @eq_f2 /2 width=1/
+qed.
 
-lemma lt_to_le: ∀a,b. a < b → a ≤ b.
-/2 width=2/ qed.
+lemma arith_b2: ∀a,b,c1,c2. c1 + c2 ≤ b → a - c1 - c2 - (b - c1 - c2) = a - b.
+#a #b #c1 #c2 #H >minus_plus >minus_plus >minus_plus /2 width=1/
+qed.
 
-lemma lt_refl_false: ∀n. n < n → False.
-#n #H elim (lt_to_not_eq … H) -H /2 width=1/
-qed-.
+lemma arith_c1x: ∀x,a,b,c1. x + c1 + a - (b + c1) = x + a - b.
+/3 by monotonic_le_minus_l, le_to_le_to_eq, le_n/ qed.
 
-lemma lt_zero_false: ∀n. n < 0 → False.
-#n #H elim (lt_to_not_le … H) -H /2 width=1/
-qed-.
+lemma arith_h1: ∀a1,a2,b,c1. c1 ≤ a1 → c1 ≤ b →
+                a1 - c1 + a2 - (b - c1) = a1 + a2 - b.
+#a1 #a2 #b #c1 #H1 #H2 >plus_minus // /2 width=1/
+qed.
+
+(* inversion & forward lemmas ***********************************************)
+
+axiom eq_nat_dec: ∀n1,n2:nat. Decidable (n1 = n2).
+
+axiom lt_dec: ∀n1,n2. Decidable (n1 < n2).
 
 lemma lt_or_ge: ∀m,n. m < n ∨ n ≤ m.
 #m #n elim (decidable_lt m n) /2 width=1/ /3 width=1/
-qed.
+qed-.
 
 lemma lt_or_eq_or_gt: ∀m,n. ∨∨ m < n | n = m | n < m.
 #m elim m -m
@@ -61,13 +73,25 @@ lemma lt_or_eq_or_gt: ∀m,n. ∨∨ m < n | n = m | n < m.
 | #m #IHm * /2 width=1/
   #n elim (IHm n) -IHm #H 
   [ @or3_intro0 | @or3_intro1 destruct | @or3_intro2 ] // /2 width=1/ (**) (* /3 width=1/ is slow *)
-qed.
+qed-.
 
-lemma le_to_lt_or_eq: ∀m,n. m ≤ n → m < n ∨ m = n.
-/2 width=1/ qed. (**) (* REMOVE: this is le_to_or_lt_eq *)
+lemma le_inv_plus_plus_r: ∀x,y,z. x + z ≤ y + z → x ≤ y.
+/2 by le_plus_to_le/ qed-.
 
-lemma plus_le_weak: ∀m,n,p. m + n ≤ p → n ≤ p.
-/2 width=2/ qed.
+lemma le_inv_plus_l: ∀x,y,z. x + y ≤ z → x ≤ z - y ∧ y ≤ z.
+/3 width=2/ qed-.
+
+lemma lt_refl_false: ∀n. n < n → False.
+#n #H elim (lt_to_not_eq … H) -H /2 width=1/
+qed-.
+
+lemma lt_zero_false: ∀n. n < 0 → False.
+#n #H elim (lt_to_not_le … H) -H /2 width=1/
+qed-.
+
+lemma plus_S_eq_O_false: ∀n,m. n + S m = 0 → False.
+#n #m <plus_n_Sm #H destruct
+qed-.
 
 lemma plus_lt_false: ∀m,n. m + n < m → False.
 #m #n #H1 lapply (le_plus_n_r n m) #H2
@@ -75,118 +99,103 @@ lapply (le_to_lt_to_lt … H2 H1) -H2 -H1 #H
 elim (lt_refl_false … H)
 qed-.
 
+lemma false_lt_to_le: ∀x,y. (x < y → False) → y ≤ x.
+#x #y #H elim (decidable_lt x y) /2 width=1/
+#Hxy elim (H Hxy)
+qed-.
+
 lemma le_fwd_plus_plus_ge: ∀m1,m2. m2 ≤ m1 → ∀n1,n2. m1 + n1 ≤ m2 + n2 → n1 ≤ n2.
 #m1 #m2 #H elim H -m1
 [ /2 width=2/
-| #m1 #_ #IHm1 #n1 #n2 #H @IHm1 /2 width=1/
+| #m1 #_ #IHm1 #n1 #n2 #H @IHm1 /2 width=3/
 ]
-qed.
+qed-.
+
+(* backward lemmas **********************************************************)
 
 lemma monotonic_lt_minus_l: ∀p,q,n. n ≤ q → q < p → q - n < p - n.
 #p #q #n #H1 #H2
 @lt_plus_to_minus_r <plus_minus_m_m //.
 qed.
 
-lemma plus_le_minus: ∀a,b,c. a + b ≤ c → a ≤ c - b.
-/2 width=1/ qed.
-
-lemma lt_plus_minus: ∀i,u,d. u ≤ i → i < d + u → i - u < d.
-/2 width=1/ qed.
+(* unstable *****************************************************************)
 
-lemma plus_plus_comm_23: ∀m,n,p. m + n + p = m + p + n.
-// qed.
+lemma arith2: ∀j,i,e,d. d + e ≤ i → d ≤ i - e + j.
+#j #i #e #d #H lapply (le_plus_to_minus_r … H) -H /2 width=3/
+qed.
 
-lemma le_plus_minus_comm: ∀n,m,p. p ≤ m → m + n - p = m - p + n.
-#n #m #p #lepm @plus_to_minus <associative_plus
->(commutative_plus p) <plus_minus_m_m //
+lemma arith5: ∀a,b1,b2,c1. c1 ≤ b1 → c1 ≤ a → a < b1 + b2 → a - c1 < b1 - c1 + b2.
+#a #b1 #b2 #c1 #H1 #H2 #H3
+>plus_minus // @monotonic_lt_minus_l //
 qed.
 
-lemma minus_le_minus_minus_comm: ∀b,c,a. c ≤ b → a - (b - c) = a + c - b.
-#b elim b -b
-[ #c #a #H >(le_O_to_eq_O … H) -H //
-| #b #IHb #c elim c -c //
-  #c #_ #a #Hcb
-  lapply (le_S_S_to_le … Hcb) -Hcb #Hcb
-  <plus_n_Sm normalize /2 width=1/
-]
+lemma arith10: ∀a,b,c,d,e. a ≤ b → c + (a - d - e) ≤ c + (b - d - e).
+#a #b #c #d #e #H
+>minus_plus >minus_plus @monotonic_le_plus_r @monotonic_le_minus_l //
 qed.
 
+(* remove *******************************************************************)
+(*
 lemma minus_plus_comm: ∀a,b,c. a - b - c = a - (c + b).
 // qed.
 
-lemma minus_minus_comm: ∀a,b,c. a - b - c = a - c - b.
-/3 width=1/ qed.
+lemma plus_S_le_to_pos: ∀n,m,p. n + S m ≤ p → 0 < p.
+/2 by ltn_to_ltO/ qed.
 
-lemma le_plus_minus: ∀a,b,c. c ≤ b → a + b - c = a + (b - c).
-/2 width=1/ qed.
+lemma minus_le: ∀m,n. m - n ≤ m.
+/2 by monotonic_le_minus_l/ qed.
 
-lemma plus_minus_m_m_comm: ∀n,m. m ≤ n → n = m + (n - m).
-/2 width=1/ qed.
+lemma le_O_to_eq_O: ∀n. n ≤ 0 → n = 0.
+/2 by le_n_O_to_eq/ qed.
 
-lemma minus_plus_m_m_comm: ∀n,m. n = (m + n) - m.
-/2 width=1/ qed.
+lemma lt_to_le: ∀a,b. a < b → a ≤ b.
+/2 by le_plus_b/ qed.
 
-lemma arith_a2: ∀a,c1,c2. c1 + c2 ≤ a → a - c1 - c2 + (c1 + c2) = a.
-/2 width=1/ qed.
+lemma le_to_lt_or_eq: ∀m,n. m ≤ n → m < n ∨ m = n.
+/2 by le_to_or_lt_eq/ qed.
 
-lemma arith_b1: ∀a,b,c1. c1 ≤ b → a - c1 - (b - c1) = a - b.
-#a #b #c1 #H >minus_plus @eq_f2 /2 width=1/
-qed.
+lemma plus_le_weak: ∀m,n,p. m + n ≤ p → n ≤ p.
+/2 by le_plus_b/ qed.
 
-lemma arith_b2: ∀a,b,c1,c2. c1 + c2 ≤ b → a - c1 - c2 - (b - c1 - c2) = a - b.
-#a #b #c1 #c2 #H >minus_plus >minus_plus >minus_plus /2 width=1/
-qed.
+lemma plus_le_minus: ∀a,b,c. a + b ≤ c → a ≤ c - b.
+/2 by le_plus_to_minus_r/ qed.
+
+lemma lt_plus_minus: ∀i,u,d. u ≤ i → i < d + u → i - u < d.
+/2 by monotonic_lt_minus_l/ qed.
+
+lemma arith_a2: ∀a,c1,c2. c1 + c2 ≤ a → a - c1 - c2 + (c1 + c2) = a.
+/2 by plus_minus/ qed.
 
 lemma arith_c1: ∀a,b,c1. a + c1 - (b + c1) = a - b.
 // qed.
 
-lemma arith_c1x: ∀x,a,b,c1. x + c1 + a - (b + c1) = x + a - b.
-#x #a #b #c1 >plus_plus_comm_23 //
-qed.
-
 lemma arith_d1: ∀a,b,c1. c1 ≤ b → a + c1 + (b - c1) = a + b.
-/2 width=1/ qed.
+/2 by plus_minus/ qed.
 
 lemma arith_e2: ∀a,c1,c2. a ≤ c1 → c1 + c2 - (c1 - a + c2) = a.
-/3 width=1/ qed.
+/2 by minus_le_minus_minus_comm/ qed.
 
 lemma arith_f1: ∀a,b,c1. a + b ≤ c1 → c1 - (c1 - a - b) = a + b.
-#a #b #c1 #H >minus_plus <minus_minus //
+/2 by minus_le_minus_minus_comm/
 qed.
 
 lemma arith_g1: ∀a,b,c1. c1 ≤ b → a - (b - c1) - c1 = a - b.
-/2 width=1/ qed.
-
-lemma arith_h1: ∀a1,a2,b,c1. c1 ≤ a1 → c1 ≤ b →
-                a1 - c1 + a2 - (b - c1) = a1 + a2 - b.
-#a1 #a2 #b #c1 #H1 #H2 <le_plus_minus_comm /2 width=1/
-qed.
+/2 by arith_b1/ qed.
 
 lemma arith_i2: ∀a,c1,c2. c1 + c2 ≤ a → c1 + c2 + (a - c1 - c2) = a.
-/2 width=1/ qed.
+/2 by plus_minus_m_m/ qed.
 
 lemma arith_z1: ∀a,b,c1. a + c1 - b - c1 = a - b.
 // qed.
 
-(* unstable *****************************************************************)
-
 lemma arith1: ∀n,h,m,p. n + h + m ≤ p + h → n + m ≤ p.
-/2 width=2/ qed.
-
-lemma arith2: ∀j,i,e,d. d + e ≤ i → d ≤ i - e + j.
-#j #i #e #d #H lapply (plus_le_minus … H) -H /2 width=3/
-qed.
+/2 by le_plus_to_le/ qed.
 
 lemma arith3: ∀a1,a2,b,c1. a1 + a2 ≤ b → a1 + c1 + a2 ≤ b + c1.
-/2 width=1/ qed.
+/2 by le_minus_to_plus/ qed.
 
 lemma arith4: ∀h,d,e1,e2. d ≤ e1 + e2 → d + h ≤ e1 + h + e2.
-/2 width=1/ qed.
-
-lemma arith5: ∀a,b1,b2,c1. c1 ≤ b1 → c1 ≤ a → a < b1 + b2 → a - c1 < b1 - c1 + b2.
-#a #b1 #b2 #c1 #H1 #H2 #H3
-<le_plus_minus_comm // @monotonic_lt_minus_l //
-qed.
+/2 by arith3/ qed.
 
 lemma arith8: ∀a,b. a < a + b + 1.
 // qed.
@@ -194,7 +203,7 @@ lemma arith8: ∀a,b. a < a + b + 1.
 lemma arith9: ∀a,b,c. c < a + (b + c + 1) + 1.
 // qed.
 
-lemma arith10: ∀a,b,c,d,e. a ≤ b → c + (a - d - e) ≤ c + (b - d - e).
-#a #b #c #d #e #H
->minus_plus >minus_plus @monotonic_le_plus_r @monotonic_le_minus_l //
-qed.
+(* backward form of le_inv_plus_l *)
+lemma P2: ∀x,y,z. x ≤ z - y → y ≤ z → x + y ≤ z.
+/2 by le_minus_to_plus_r/ qed.
+*)
diff --git a/matita/matita/contribs/lambda_delta/Ground_2/notation.ma b/matita/matita/contribs/lambda_delta/Ground_2/notation.ma
index 65cb0a029..45109878f 100644
--- a/matita/matita/contribs/lambda_delta/Ground_2/notation.ma
+++ b/matita/matita/contribs/lambda_delta/Ground_2/notation.ma
@@ -14,18 +14,12 @@
 
 (* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
 
-(* Subsets ******************************************************************)
-
-notation "hvbox( T ϵ break R )"
-   non associative with precedence 45
-   for @{ 'InSubset $T $R }.
-
 (* Lists ********************************************************************)
 
 notation "hvbox( hd break :: tl )"
   right associative with precedence 47
   for @{'Cons $hd $tl}.
 
-notation "hvbox( l1 break @ l2)"
+notation "hvbox( l1 break @ l2 )"
   right associative with precedence 47
   for @{'Append $l1 $l2 }.
diff --git a/matita/matita/contribs/lambda_delta/Ground_2/star.ma b/matita/matita/contribs/lambda_delta/Ground_2/star.ma
index ee6a901e8..56181da2f 100644
--- a/matita/matita/contribs/lambda_delta/Ground_2/star.ma
+++ b/matita/matita/contribs/lambda_delta/Ground_2/star.ma
@@ -15,22 +15,19 @@
 include "basics/star.ma".
 include "Ground_2/xoa_props.ma".
 
-(* PROPERTIES of RELATIONS **************************************************)
+(* PROPERTIES OF RELATIONS **************************************************)
 
-definition predicate: Type[0] → Type[0] ≝ λA. A → Prop.
+definition Decidable: Prop → Prop ≝ λR. R ∨ (R → False).
 
-definition Decidable: Prop → Prop ≝
-   λR. R ∨ (R → False). 
+definition confluent2: ∀A. ∀R1,R2: relation A. Prop ≝ λA,R1,R2.
+                       ∀a0,a1. R1 a0 a1 → ∀a2. R2 a0 a2 →
+                       ∃∃a. R2 a1 a & R1 a2 a.
 
-definition confluent: ∀A. ∀R1,R2: relation A. Prop ≝ λA,R1,R2.
-                      ∀a0,a1. R1 a0 a1 → ∀a2. R2 a0 a2 →
-                      ∃∃a. R2 a1 a & R1 a2 a.
+definition transitive2: ∀A. ∀R1,R2: relation A. Prop ≝ λA,R1,R2.
+                        ∀a1,a0. R1 a1 a0 → ∀a2. R2 a0 a2 →
+                        ∃∃a. R2 a1 a & R1 a a2.
 
-definition transitive: ∀A. ∀R1,R2: relation A. Prop ≝ λA,R1,R2.
-                       ∀a1,a0. R1 a1 a0 → ∀a2. R2 a0 a2 →
-                       ∃∃a. R2 a1 a & R1 a a2.
-
-lemma TC_strip1: ∀A,R1,R2. confluent A R1 R2 →
+lemma TC_strip1: ∀A,R1,R2. confluent2 A R1 R2 →
                  ∀a0,a1. TC … R1 a0 a1 → ∀a2. R2 a0 a2 →
                  ∃∃a. R2 a1 a & TC … R1 a2 a.
 #A #R1 #R2 #HR12 #a0 #a1 #H elim H -a1
@@ -42,7 +39,7 @@ lemma TC_strip1: ∀A,R1,R2. confluent A R1 R2 →
 ]
 qed.
 
-lemma TC_strip2: ∀A,R1,R2. confluent A R1 R2 →
+lemma TC_strip2: ∀A,R1,R2. confluent2 A R1 R2 →
                  ∀a0,a2. TC … R2 a0 a2 → ∀a1. R1 a0 a1 →
                  ∃∃a. TC … R2 a1 a & R1 a2 a.
 #A #R1 #R2 #HR12 #a0 #a2 #H elim H -a2
@@ -54,8 +51,8 @@ lemma TC_strip2: ∀A,R1,R2. confluent A R1 R2 →
 ]
 qed.
 
-lemma TC_confluent: ∀A,R1,R2.
-                    confluent A R1 R2 → confluent A (TC … R1) (TC … R2).
+lemma TC_confluent2: ∀A,R1,R2.
+                     confluent2 A R1 R2 → confluent2 A (TC … R1) (TC … R2).
 #A #R1 #R2 #HR12 #a0 #a1 #H elim H -a1
 [ #a1 #Ha01 #a2 #Ha02
   elim (TC_strip2 … HR12 … Ha02 … Ha01) -HR12 -a0 /3 width=3/
@@ -65,11 +62,7 @@ lemma TC_confluent: ∀A,R1,R2.
 ]
 qed.
 
-lemma TC_strap: ∀A. ∀R:relation A. ∀a1,a,a2.
-                R a1 a → TC … R a a2 → TC … R a1 a2.
-/3 width=3/ qed.
-
-lemma TC_strap1: ∀A,R1,R2. transitive A R1 R2 →
+lemma TC_strap1: ∀A,R1,R2. transitive2 A R1 R2 →
                  ∀a1,a0. TC … R1 a1 a0 → ∀a2. R2 a0 a2 →
                  ∃∃a. R2 a1 a & TC … R1 a a2.
 #A #R1 #R2 #HR12 #a1 #a0 #H elim H -a0
@@ -81,7 +74,7 @@ lemma TC_strap1: ∀A,R1,R2. transitive A R1 R2 →
 ]
 qed.
 
-lemma TC_strap2: ∀A,R1,R2. transitive A R1 R2 →
+lemma TC_strap2: ∀A,R1,R2. transitive2 A R1 R2 →
                  ∀a0,a2. TC … R2 a0 a2 → ∀a1. R1 a1 a0 →
                  ∃∃a. TC … R2 a1 a & R1 a a2.
 #A #R1 #R2 #HR12 #a0 #a2 #H elim H -a2
@@ -93,8 +86,8 @@ lemma TC_strap2: ∀A,R1,R2. transitive A R1 R2 →
 ]
 qed.
 
-lemma TC_transitive: ∀A,R1,R2.
-                     transitive A R1 R2 → transitive A (TC … R1) (TC … R2).
+lemma TC_transitive2: ∀A,R1,R2.
+                      transitive2 A R1 R2 → transitive2 A (TC … R1) (TC … R2).
 #A #R1 #R2 #HR12 #a1 #a0 #H elim H -a0
 [ #a0 #Ha10 #a2 #Ha02
   elim (TC_strap2 … HR12 … Ha02 … Ha10) -HR12 -a0 /3 width=3/
@@ -104,15 +97,6 @@ lemma TC_transitive: ∀A,R1,R2.
 ]
 qed.
 
-lemma TC_reflexive: ∀A,R. reflexive A R → reflexive A (TC … R).
-/2 width=1/ qed.
-
-lemma TC_star_ind: ∀A,R. reflexive A R → ∀a1. ∀P:predicate A.
-                   P a1 → (∀a,a2. TC … R a1 a → R a a2 → P a → P a2) →
-                   ∀a2. TC … R a1 a2 → P a2.
-#A #R #H #a1 #P #Ha1 #IHa1 #a2 #Ha12 elim Ha12 -a2 /3 width=4/
-qed.
-
 definition NF: ∀A. relation A → relation A → predicate A ≝
    λA,R,S,a1. ∀a2. R a1 a2 → S a1 a2.